diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index b145f55..7b33ae9 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -26,3 +26,45 @@ jobs:
           cargo test --locked --test protocol_contract
           cargo test --locked --bin echidnabot clone_contract_tests
           cargo test --locked --lib git_process_tests
+
+  theory:
+    # Receipt-boundary theory (docs/PROOF-STATUS.adoc T-RECEIPT): the Agda
+    # source and its Lean and Rocq re-proofs, each checked by its own kernel
+    # at this commit. Toolchains come from pinned upstream release archives,
+    # not the Guix manifest: this is the recorded PROOF-POLICY §6 deviation
+    # D-THEORY-TOOLS in docs/PROOF-STATUS.adoc. Each archive is verified by
+    # digest, and each script fails if the version it observes differs.
+    name: Theory proofs (Agda, Lean, Rocq)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    env:
+      AGDA_URL: https://github.com/agda/agda/releases/download/v2.8.0.2/Agda-v2.8.0.2-linux.tar.xz
+      AGDA_SHA256: 2bcf24bb561b1be859bba841e5d67962d1616b3251bc147f878e4f60a2fbd9f7
+      LEAN_URL: https://releases.lean-lang.org/lean4/v4.35.0/lean-4.35.0-linux.tar.zst
+      LEAN_SHA256: 7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d
+    steps:
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install Agda 2.8.0.2 (digest-verified release)
+        run: |
+          mkdir -p "$RUNNER_TEMP/agda"
+          curl --proto "=https" --tlsv1.2 -fsSL -o "$RUNNER_TEMP/agda.tar.xz" "$AGDA_URL"
+          echo "$AGDA_SHA256  $RUNNER_TEMP/agda.tar.xz" | sha256sum -c -
+          tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP/agda"
+          echo "$RUNNER_TEMP/agda" >> "$GITHUB_PATH"
+      - name: Install Lean 4.35.0 (digest-verified release)
+        run: |
+          mkdir -p "$RUNNER_TEMP/lean"
+          curl --proto "=https" --tlsv1.2 -fsSL -o "$RUNNER_TEMP/lean.tar.zst" "$LEAN_URL"
+          echo "$LEAN_SHA256  $RUNNER_TEMP/lean.tar.zst" | sha256sum -c -
+          tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean" --strip-components=1
+          echo "$RUNNER_TEMP/lean/bin" >> "$GITHUB_PATH"
+      - name: Install Coq 8.18.0 (Ubuntu 24.04 archive)
+        run: |
+          sudo apt-get update -q
+          sudo apt-get install -y -q coq
+      - name: Agda source (strict profile)
+        run: ./scripts/check-agda-proofs.sh
+      - name: Lean and Rocq recheck legs (with negative controls)
+        run: ./scripts/check-theory-rechecks.sh
diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
index fd85057..8fd5d7e 100644
--- a/docs/PROOF-STATUS.adoc
+++ b/docs/PROOF-STATUS.adoc
@@ -4,18 +4,25 @@
 
 == Evidence rules
 
-Updated 2026-11-01 on `arena/68c18146-echidnabot`, based on
-`ab26bd54c8bdc04da8cc48c0778a25eb774be268`. New files are working-tree
-candidates, not committed or checked proof receipts. No Grade 3 attainment
-is claimed. `open` means not checked/done, `argued` means an explicit
-assumption, and `tested-only` requires an actual observed bounded check.
-ConfidenceLevel::Level3 is a runtime heuristic, NOT Mathesis Grade 3.
+First written 2026-11-01 on `arena/68c18146-echidnabot`, based on
+`ab26bd54c8bdc04da8cc48c0778a25eb774be268`. Updated 2026-11-09 with the
+first kernel receipts for the receipt-boundary theory, taken at
+`1443adfabb98a9e0daea562bc8dbe764442c14cc` (<<receipts>>), and with the
+GraphQL authorisation obligations from #192 (<<rust-auth>>).
+
+Tokens are the closed vocabulary of PROOF-POLICY §5: `proven`,
+`proven-with-postulates`, `tested-only`, `argued`, `open`. A theory theorem
+also carries a Proof Witness Grade (PWG, PROOF-POLICY §8) and, per leg, a
+§2.2 correspondence state. The three are separate fields. A PWG is derived
+from the receipts below, never asserted. `ConfidenceLevel::Level3` is a
+runtime heuristic and is not a PWG.
 
 Policies and pinned references are in
 link:ESTATE-ROUTING-AUDIT.adoc[the routing audit]. Theory requires strict
 Agda checks, with separately recorded Rocq/Lean statement correspondence and
-kernel results. Rust behaviour requires Creusot on actual first-party code;
-a mathematical model does not establish runtime refinement.
+kernel results. Rust behaviour is verified with Creusot (Pearlite contracts)
+and Verus on the actual first-party code (PROOF-POLICY §1.2); a mathematical
+model does not establish runtime refinement.
 
 == Local obligation ledger
 
@@ -25,22 +32,32 @@ a mathematical model does not establish runtime refinement.
 |T-RECEIPT
 |A general evidence token does not imply its claim;
 `proofs/agda/ReceiptBoundary.agda`
-|open
-|AGDA-PENDING. `no-unconditional-reflection` constructs a contradiction
-from unconditional reflection by instantiating Claim with Empty and evidence
-with Unit. `receive-with-soundness` requires an explicit evidence-to-claim
-function. This is new local theory, informed by epistemic-types, NOT a port
-of that library or proof of the Rust parser. No external library or postulate.
-|T-RECEIPT-ROCQ / T-RECEIPT-LEAN
-|Same statements, quantification, evidence packaging and assumptions as
-T-RECEIPT
-|open
-|Independent re-proof source candidates now exist under
-`proofs/theory/{rocq,lean}/ReceiptBoundary.*`, without libraries, axioms or
-admitted obligations. Neither was compiled; no transport or checked
-correspondence exists. A Prop-only reformulation of Set-level quantification
-is not silently interchangeable. The candidates deliberately use Rocq Set
-and Lean Type rather than silently shrinking the claims to Prop.
+|proven
+|AGDA-VERIFIED (<<receipts>>, R-AGDA). `no-unconditional-reflection`
+constructs a contradiction from unconditional reflection by instantiating
+Claim with Empty and evidence with Unit. `receive-with-soundness` requires
+an explicit evidence-to-claim function. This is new local theory, informed
+by epistemic-types, NOT a port of that library or proof of the Rust parser.
+Import cone: this module alone, no libraries, no postulates. PWG: `PWG-3`,
+derived; it owes both recheck legs until they count (§8.4).
+|T-RECEIPT-LEAN
+|A Lean restatement of T-RECEIPT, intended to match it; the match is not
+yet confirmed (`BRIDGE-PENDING`). `proofs/theory/lean/ReceiptBoundary.lean`
+|proven
+|Route `re-proved`; transport was tried and failed (<<transport>>).
+LEAN-CHECKED, no axioms (<<receipts>>, R-LEAN).
+§2.2 state `BRIDGE-PENDING`: the statement comparison in
+<<correspondence>> is agent-drafted and awaits owner review. Until then the
+leg does not count towards a PWG.
+|T-RECEIPT-ROCQ
+|A Rocq restatement of T-RECEIPT, intended to match it; the match is not
+yet confirmed (`BRIDGE-PENDING`). `proofs/theory/rocq/ReceiptBoundary.v`
+|proven
+|Route `re-proved`; transport was tried and failed (<<transport>>).
+COQ-CHECKED, closed under the global context
+(<<receipts>>, R-ROCQ). §2.2 state `BRIDGE-PENDING`, as for the Lean leg.
+The leg was checked with Coq 8.18.0, not a Rocq 9 release; the file uses
+only the prelude (`Empty_set`, `unit`).
 |E-ADAPTER
 |`VeriSimEchidnaAdapter::prove` validates the gateway payload and propagates
 failure without calling a direct client
@@ -85,10 +102,12 @@ is out of scope does NOT make that scaffolding verified.
   because there was no Agda record. It is not witness transport. Rocq/Lean
   Prop and Agda Set differ; correspondence is limited to propositional
   identity and remains `open` until checked and justified explicitly.
-  All three current executions are unavailable in this sandbox.
+  The Agda file checks under the strict profile (<<receipts>>, R-AGDA); the
+  Rocq and Lean fixtures are prover test material (PROOF-POLICY §3), not
+  recheck legs.
 * `proofs/coq/admitted_stub.v` and `proofs/lean/sorry_stub.lean` are negative
   fixtures, not candidate proofs. Their escape hatches must stay intact.
-  They are excluded from Grade 3 counts, not repaired into passing fixtures.
+  They are excluded from PWG counts, not repaired into passing fixtures.
 * JSON files under `proofs/test_fixtures` are webhook/prover inputs, not proofs.
 
 === ABI scaffold debt (not verified)
@@ -121,49 +140,223 @@ or layout contracts are invented in this patch.
 * Any future claim of theorem truth needs the relevant prover kernel/checker
   boundary and assumptions, separately from receipt transport.
 
-== Toolchain acquisition attempt
-
-Published stable releases observed through GitHub's release API on 2026-11-01:
-Rust 1.99.1; Agda 2.8.0.2; Creusot 0.14.0; Idris2 0.8.0;
-Lean 4.35.0; Rocq 9.3.0; Cubicle 1.2.0. None was installed or run.
-Creusot 0.14.0 itself pins `nightly-2026-08-03` with rustc-dev and llvm-tools;
-it cannot simply be built against latest stable Rust. Its INSTALL requires
-Cargo, opam/OCaml, Why3/Why3find and solver acquisition.
-
-Actual network observations:
-
-* `static.rust-lang.org` and `deb.debian.org`: TLS connection failed;
-  Debian HTTP also returned an empty reply.
-* The Agda Linux release asset was requested through api.github.com;
-  its redirect to `release-assets.githubusercontent.com` failed TLS.
-* The sandbox permits GitHub source/API and npm/PyPI registries, not the
-  distribution/package hosts needed by the normal installers. Unrelated npm
-  packages named agda/rustup are not substituted for trusted toolchains.
-
-Required environment help: provision verified toolchains through the session
-setup, or allow the official distribution and package hosts (including release
-assets and the dependencies required by opam). Cubical Agda is a mode of Agda,
-not the separate Cubicle model checker. Full Cubical is not the canonical
-proof profile and needs a separately reviewed exception where necessary.
-The existing Rust pin is preserved until an actual tested toolchain update;
-this is an unmet latest-stable target, not a completed upgrade.
+
+[[receipts]]
+== Kernel receipts (2026-11-09, agent session)
+
+Taken at `1443adfabb98a9e0daea562bc8dbe764442c14cc` with the scripts below.
+These are session receipts, not per-commit CI receipts: the `theory` job in
+`.github/workflows/proof-safety.yml` repeats them on every pull request and
+push to `main`, and its run is the receipt `PWG-1` would need (§8.2).
+
+[cols="1,2,3,2",options="header"]
+|===
+|ID |Checker |Invocation and input digest |Observed result, axioms
+
+|R-AGDA
+|Agda 2.8.0.2, official Linux release (archive sha256
+`2bcf24bb561b1be859bba841e5d67962d1616b3251bc147f878e4f60a2fbd9f7`)
+|`./scripts/check-agda-proofs.sh`: `agda --safe --without-K
+--cubical-compatible --exact-split --no-sized-types --no-guardedness
+--no-libraries --no-default-libraries --ignore-interfaces`.
+`ReceiptBoundary.agda` sha256
+`276ee4b56a9c2c7e7d8878162090785119bbbb141c359afc6d3352b0100c9014`;
+`FixtureIdentity.agda` sha256
+`9c7b80b13f3507fc54f08b93e17190fc081c4cee00db0dd63d70c154746a91fb`
+|Both modules accepted, exit 0. `--safe` refuses `postulate`; no library is
+in the import cone. Negative controls: a planted `postulate` and a false
+reflection proof were both refused (exit 42).
+
+|R-LEAN
+|Lean 4.35.0, commit `eb6cafb7290e8bd5f2937522d8d804f58f02bafc` (release
+archive sha256
+`7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d`)
+|`./scripts/check-theory-rechecks.sh`: `lean -o` compiles the file as a
+module; a query file the script writes runs `#print axioms` on the three
+named theorems. Source sha256
+`00ea31f061473e4ad48d06904c18d302c30d5b1443d6dd71afb863c8e328858f`
+|Accepted, exit 0. None of the three theorems depends on any axiom.
+Negative control: a planted `axiom` is reported and refused.
+
+|R-ROCQ
+|The Coq Proof Assistant 8.18.0 (OCaml 4.14.1), Ubuntu 24.04 `coq`
+package `8.18.0+dfsg-1build2`
+|`./scripts/check-theory-rechecks.sh`: `coqc -q -Q . Recheck` compiles the
+file as a module; one query file per theorem, written by the script, runs
+`Print Assumptions` on it. Source sha256
+`ca65d1dd2c87cee49a10d26c0466b3ba812d183c71d44e965b9d14e99bf3e66d`
+|Accepted, exit 0. `Print Assumptions`: all three closed under the global
+context. Negative control: a planted `Admitted` is reported and refused.
+|===
+
+[[correspondence]]
+== Statement correspondence for T-RECEIPT (agent-drafted, awaiting review)
+
+Both recheck legs are re-proofs, not transports (§2). The comparison below
+was made by reading the three files side by side. It was drafted by an agent
+and is not yet reviewed, so each leg stays `BRIDGE-PENDING` and does not
+count towards a PWG (§2.2, §8.2). On owner review it becomes `RECONCILED`,
+and the PWG derived from these receipts would then be `PWG-2ii`.
+
+[cols="2,2,2,2",options="header"]
+|===
+|Item |Agda |Lean 4 |Rocq
+
+|Small universe of claims and evidence
+|`Set` (`--without-K`)
+|`Type` (Type 0)
+|`Set` (predicative)
+
+|Warrant record and its universe
+|`Warrant Claim : Set₁`, fields `Evidence : Set`, `evidence : Evidence`
+|`ReceiptWarrant Claim : Type 1`, same fields
+|`ReceiptWarrant Claim : Type`, fields `evidence_type : Set`,
+`evidence_token`
+
+|Soundness structure
+|`SoundWarrant w : Set`, field `sound : Evidence w → Claim`
+|`SoundReceiptWarrant w`, same field
+|`SoundReceiptWarrant w : Type`, same field
+
+|Empty and unit
+|local `Empty` (no constructors), local `Unit`
+|core `Empty`, core `Unit` (`PUnit.{1}`)
+|prelude `Empty_set`, `unit`
+
+|`receive-with-soundness`
+|`(w : Warrant Claim) → SoundWarrant w → Claim`
+|same quantification
+|same quantification
+
+|`no-unconditional-reflection`
+|`((Claim : Set) → Warrant Claim → Claim) → Empty`
+|same, over `Type`
+|same, over `Set`
+
+|`no-soundness-for-empty-token`
+|`SoundWarrant empty-claim-token → Empty`
+|same
+|same
+|===
+
+Residual assumptions: none in any leg (no postulates, axioms or admitted
+obligations). The match is between small predicative universes; none of the
+three statements is about `Prop`, and none is moved there.
+
+[[transport]]
+=== Why both legs are re-proved: the Dedukti transport attempt (2026-11-09)
+
+PROOF-POLICY §2 asks for transport through Dedukti first. It was tried for
+T-RECEIPT in an agent session and failed at both steps, so both legs fall
+back to re-proof (§2, "Re-proof as fallback").
+
+. *Agda to Dedukti.* Agda2Dedukti at `c7c7d671` (the only Agda-to-Dedukti
+  translator; it builds against a Deducteam fork of Agda reporting 2.6.3)
+  translates its own test files (`dependantRecord`, `box`), and Dedukti 2.7
+  accepts them. It does not translate `ReceiptBoundary.agda`:
+  * the fork rejects `--cubical-compatible`; a copy differing only by that
+    flag was used;
+  * on that copy the translator stops with an internal Agda error
+    (`__IMPOSSIBLE__`, `Agda/TypeChecking/Sort.hs:216`), in both its plain
+    and eta modes. Minimal modules isolate the trigger: a parameterised
+    record in `Set₁`, which is how `Warrant` is declared;
+  * a variant with `Warrant` as a `data` type (checked by Agda 2.8.0.2, so
+    a different source, not T-RECEIPT) fails differently: "Expected a
+    unrestricted argument, but found an erased argument".
+. *Dedukti to Rocq and Lean.* Even a translated term would have no route
+  out. Lambdapi 4.0.0 (2026-11-05) adds a Lean exporter beside its Rocq
+  one, but both drop rewrite rules ("Command not translated") and turn
+  the theory's symbols into axioms. Agda's Dedukti encoding is built on
+  rewrite rules. On a five-line rewrite theory both exports fail to
+  type-check: with the rule gone, the proof term no longer has its stated
+  type.
+
+The statement comparison above is therefore by reading, and the legs stay
+`BRIDGE-PENDING` until the owner reviews it. Retry the transport when
+Agda2Dedukti tracks a current Agda or Lambdapi exports rewrite theories.
+
+[[rust-auth]]
+== GraphQL authorisation obligations (#192)
+
+#192 added bearer authentication and per-field authorisation. Under
+PROOF-POLICY §1.2 its behaviour is verified with Creusot (Pearlite contracts)
+and Verus on the shipped functions. No verifier was run on it; it is covered
+by unit, contract and smoke tests only, which are not proof receipts. Each
+row is `open` until a verifier discharges it.
+
+[cols="1,3,2,2",options="header"]
+|===
+|ID |Entrypoint and specification |Verifiers and assumptions |Status and next action
+
+|E-AUTH-SCOPE
+|`RepoScope::allows` (`src/api/auth.rs`): true iff the slug is `owner/name`
+with one `/`, both parts non-empty, and some pattern is that exact slug or
+`owner/*` for that owner. No pattern admits every owner.
+|Creusot/Pearlite and Verus. Assumes `str` equality, `split_once` and
+`contains` behave as std documents (trusted extern specs).
+|`open`. Tests: `scope_matches_exact_and_owner_wildcard_only`. Next: Pearlite
+contract on a byte-slice core of the matcher.
+
+|E-AUTH-ROLE
+|`ApiCredentials::authenticate`: the admin credential maps to `Admin`, the
+route credential to `Route(scope)`, anything else to `None`; credentials
+are trimmed on storage and on presentation alike.
+|Creusot/Pearlite and Verus. `constant_time_eq`
+(`src/trust/solver_integrity.rs`) is assumed to equal byte equality; its
+timing property is outside both verifiers.
+|`open`. Tests: `authenticate_maps_each_credential_to_its_role`,
+`stored_credentials_are_trimmed_like_presented_ones`.
+
+|E-AUTH-GUARD
+|`admin_only`, `route_or_admin`, `check_repo_scope`: with no principal every
+guarded field is refused; `Route` reaches only `submitProofObligation`, and
+only in scope.
+|Creusot/Pearlite and Verus on the guard functions. async-graphql guard
+dispatch is a trusted boundary (third party, §1.1).
+|`open`. Tests: `schema_executed_without_a_principal_refuses_the_guarded_fields`,
+`route_credential_cannot_reach_administrative_fields`.
+
+|E-RATE-BOUND
+|`WebhookRateLimiter::check_ip` (`src/api/rate_limit.rs`): at most `limit`
+admissions per peer per window; the peer map is swept when it reaches
+`max(4096, 2 × size after the last sweep)`, and a sweep never drops a peer
+with a request inside the window.
+|Creusot/Pearlite and Verus. `Instant` monotonicity and `HashMap` behaviour
+are trusted std boundaries.
+|`open`. Tests: `idle_peers_are_swept_once_the_map_is_large`,
+`active_peers_survive_a_sweep_and_stay_limited`.
+|===
+
+[[deviations]]
+== Toolchain deviations (PROOF-POLICY §6)
+
+`D-THEORY-TOOLS`, state `open`. The `theory` job in
+`.github/workflows/proof-safety.yml` installs its checkers outside a Guix
+manifest or container, because this repository has neither:
+
+* Agda 2.8.0.2 from the official GitHub release archive, digest above;
+* Lean 4.35.0 from `releases.lean-lang.org`, digest above;
+* Coq from the Ubuntu 24.04 archive. Nothing pins the package version;
+  `scripts/check-theory-rechecks.sh` requires 8.18.0 and fails otherwise.
+
+Each script asserts the version it observes and fails on a mismatch. The
+deviation closes when a Guix manifest or a proof-toolchain container provides
+the same versions.
 
 == Reproduction and completion criteria
 
-`./scripts/check-agda-proofs.sh` requires exactly Agda 2.8.0.2, ignores stale
-interfaces, uses no external libraries, and runs the strict policy flags.
-It prints source hashes, base revision and invocations. Capture the output
-and record the observed result here; do not edit statuses based on expected
-success. Its missing-tool failure was observed in this session (exit 127).
-This is evidence that absence is not silently skipped, not a proof execution.
-
-`cargo test --locked dispatcher::verisim_echidna` and the existing protocol
-suites remain unrun. Creusot, Idris2 and independent theory rechecks also
-remain unrun. CI wiring for the new theory gate and its real positive/negative
-controls is still open; a local check command is not an installed CI gate.
-
-Completion requires: actual checker receipts; backend protocol agreement;
-production routing and provenance migration; implementation/interface proofs;
-matched theory rechecks; preserved fixture detection; and regression tests.
-This session has NOT completed old/new proof updating or the original routing
-work. Documentation and unverified source candidates are partial progress only.
+`./scripts/check-agda-proofs.sh` requires Agda 2.8.0.2 (first line of
+`agda --version`; the official binary prints build flags after it), ignores
+stale interfaces, uses no external libraries, and runs the strict policy
+flags. `./scripts/check-theory-rechecks.sh` requires Lean at the version in
+`proofs/theory/lean/lean-toolchain` and Coq 8.18.0, runs each leg's negative
+control first, and fails unless every axiom report is clean. Both print
+source hashes, base revision and invocations. Record the observed result
+here; do not edit statuses on expected success.
+
+Still open: `cargo test --locked dispatcher::verisim_echidna`; Creusot and
+Verus on any Rust obligation; Idris2 for I-GATEWAY; owner review of the
+T-RECEIPT correspondence; and a Rocq 9 recheck if the estate pins one.
+Completion requires backend protocol agreement, production routing and
+provenance migration, implementation and interface proofs, and preserved
+fixture detection.
diff --git a/scripts/check-agda-proofs.sh b/scripts/check-agda-proofs.sh
index 4ea20c0..d1f9670 100755
--- a/scripts/check-agda-proofs.sh
+++ b/scripts/check-agda-proofs.sh
@@ -9,7 +9,7 @@ if ! command -v agda >/dev/null; then
     echo 'OPEN: Agda 2.8.0.2 is required; no proof was checked.' >&2
     exit 127
 fi
-actual=$(agda --version)
+actual=$(agda --version | head -n 1)
 if [[ "$actual" != "$expected" ]]; then
     printf 'OPEN: expected %s, observed %s. Review the pin explicitly.\n' "$expected" "$actual" >&2
     exit 1
diff --git a/scripts/check-theory-rechecks.sh b/scripts/check-theory-rechecks.sh
new file mode 100755
index 0000000..8b438a8
--- /dev/null
+++ b/scripts/check-theory-rechecks.sh
@@ -0,0 +1,121 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Recheck legs of the receipt-boundary theory (PROOF-POLICY §2): Lean and Rocq.
+# Each leg is an independent re-proof, not a transport of the Agda term. This
+# script checks that each target kernel accepts its file and that each named
+# theorem below depends on no axioms; the statement correspondence is recorded
+# separately in docs/PROOF-STATUS.adoc.
+#
+# The axiom queries are not taken from the proof file. Each leg compiles the
+# file as a module, then asks about a fixed list of names from a query file
+# this script writes. What the proof file prints, or leaves unqueried, cannot
+# change the verdict. Both legs first run a negative control (a planted axiom,
+# a planted Admitted) that must compile, be reported, and still be refused.
+set -euo pipefail
+cd "$(dirname "${BASH_SOURCE[0]}")/.."
+
+# The theorems the T-RECEIPT-LEAN and T-RECEIPT-ROCQ rows claim. Keep these
+# in step with docs/PROOF-STATUS.adoc.
+lean_names=(
+    EchidnabotReceiptBoundary.receiveWithSoundness
+    EchidnabotReceiptBoundary.noUnconditionalReflection
+    EchidnabotReceiptBoundary.noSoundnessForEmptyToken
+)
+rocq_names=(receive_with_soundness no_unconditional_reflection no_soundness_for_empty_token)
+
+lean_expected="version $(sed -n 's|^leanprover/lean4:v||p' proofs/theory/lean/lean-toolchain)"
+rocq_expected='The Coq Proof Assistant, version 8.18.0'
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+
+require() {
+    local tool=$1
+    if ! command -v "$tool" >/dev/null; then
+        echo "OPEN: $tool is required; no proof was checked." >&2
+        exit 127
+    fi
+}
+
+# lean_leg FILE NAME...: Lean compiles FILE as a module, and a separate query
+# file reports each NAME as depending on no axioms. Prints the query output.
+lean_leg() {
+    local file=$1 dir mod out name
+    shift
+    dir=$(mktemp -d -p "$work")
+    mod=$(basename "$file" .lean)
+    cp "$file" "$dir/$mod.lean"
+    (cd "$dir" && lean -o "$mod.olean" "$mod.lean" >/dev/null 2>&1) || { echo "lean rejected $file" >&2; return 1; }
+    { printf 'import %s\n' "$mod"; printf '#print axioms %s\n' "$@"; } >"$dir/Query.lean"
+    out=$(cd "$dir" && LEAN_PATH="$dir" lean Query.lean 2>&1) || { printf '%s\n' "$out"; return 1; }
+    printf '%s\n' "$out"
+    if grep -q 'depends on axioms' <<<"$out"; then return 1; fi
+    for name in "$@"; do
+        grep -qxF "'$name' does not depend on any axioms" <<<"$out" || return 1
+    done
+}
+
+# rocq_leg FILE NAME...: coqc compiles FILE as a module, and one query file
+# per NAME reports it closed under the global context. Prints the output.
+rocq_leg() {
+    local file=$1 dir mod out name
+    shift
+    dir=$(mktemp -d -p "$work")
+    mod=$(basename "$file" .v)
+    cp "$file" "$dir/$mod.v"
+    (cd "$dir" && coqc -q -Q . Recheck "$mod.v" >/dev/null 2>&1) || { echo "coqc rejected $file" >&2; return 1; }
+    for name in "$@"; do
+        printf 'From Recheck Require %s.\nPrint Assumptions Recheck.%s.%s.\n' "$mod" "$mod" "$name" >"$dir/Query.v"
+        out=$(cd "$dir" && coqc -q -Q . Recheck Query.v 2>&1) || { printf '%s\n' "$out"; return 1; }
+        printf '%s: %s\n' "$name" "$out"
+        [[ "$out" == 'Closed under the global context' ]] || return 1
+    done
+}
+
+# control LEG FILE NAME REPORT: LEG must refuse FILE, and its query output must
+# contain REPORT, so the refusal is the axiom check and not a compile error.
+control() {
+    local leg=$1 file=$2 name=$3 report=$4 out
+    if out=$("$leg" "$file" "$name" 2>&1); then
+        echo "FAIL: $leg accepted control $(basename "$file")." >&2
+        exit 1
+    fi
+    if ! grep -q -- "$report" <<<"$out"; then
+        printf '%s\n' "$out" >&2
+        echo "FAIL: control $(basename "$file") was refused without reporting its planted axiom." >&2
+        exit 1
+    fi
+}
+
+printf 'Base commit (not a clean-tree claim): %s\n' "$(git rev-parse HEAD)"
+
+require lean
+lean_actual=$(lean --version | head -n 1)
+if [[ "$lean_actual" != *"$lean_expected,"* ]]; then
+    printf 'OPEN: expected Lean %s, observed %s.\n' "$lean_expected" "$lean_actual" >&2
+    exit 1
+fi
+printf 'Tool: %s\n' "$lean_actual"
+printf 'axiom planted : False\ntheorem uses : False := planted\n' >"$work/Planted.lean"
+control lean_leg "$work/Planted.lean" uses "'uses' depends on axioms: \[planted\]"
+sha256sum proofs/theory/lean/ReceiptBoundary.lean
+printf 'Invocation: lean -o ReceiptBoundary.olean ReceiptBoundary.lean, then #print axioms for:'
+printf ' %s' "${lean_names[@]}"
+printf '\n'
+lean_leg proofs/theory/lean/ReceiptBoundary.lean "${lean_names[@]}"
+
+require coqc
+rocq_actual=$(coqc --version | head -n 1)
+if [[ "$rocq_actual" != "$rocq_expected" ]]; then
+    printf 'OPEN: expected %s, observed %s.\n' "$rocq_expected" "$rocq_actual" >&2
+    exit 1
+fi
+printf 'Tool: %s\n' "$rocq_actual"
+printf 'Lemma planted : False.\nAdmitted.\n' >"$work/Planted.v"
+control rocq_leg "$work/Planted.v" planted '^Planted.planted : False'
+sha256sum proofs/theory/rocq/ReceiptBoundary.v
+printf 'Invocation: coqc -q -Q . Recheck ReceiptBoundary.v, then Print Assumptions for:'
+printf ' %s' "${rocq_names[@]}"
+printf '\n'
+rocq_leg proofs/theory/rocq/ReceiptBoundary.v "${rocq_names[@]}"
+
+printf '%s\n' 'LEAN-CHECKED and COQ-CHECKED for these source hashes only; statement correspondence is recorded in docs/PROOF-STATUS.adoc.'