diff --git a/.github/workflows/agda-proof-policy.yml b/.github/workflows/agda-proof-policy.yml
index 1cfb9be..e2f9fd6 100644
--- a/.github/workflows/agda-proof-policy.yml
+++ b/.github/workflows/agda-proof-policy.yml
@@ -125,8 +125,8 @@ jobs:
           git init -q "$r"
           git -C "$r" remote add origin https://github.com/metadatastician/standards.git
           git -C "$r" config core.sparseCheckout true
-          printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout"
-          git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4
+          printf '1-formats/deed/tools/\nscripts/check-proof-receipt.sh\nscripts/proof-inputs-sha256.sh\n' > "$r/.git/info/sparse-checkout"
+          git -C "$r" fetch -q --depth 1 origin e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d
           git -C "$r" checkout -q FETCH_HEAD
 
       - name: Golden path (just check), then its controls
@@ -134,6 +134,9 @@ jobs:
         env:
           MATHESIS_STANDARDS: ${{ runner.temp }}/receipt-reader
         run: |
+          # The receipt's git checks (PROOF-POLICY §8.5.3) need origin/main with its
+          # history: the checkout is shallow.
+          git fetch -q --no-tags --unshallow origin +refs/heads/main:refs/remotes/origin/main
           guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- sh -euc '
             just --version
             bun --version
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index a3ff99d..a3ae611 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -31,7 +31,7 @@ jobs:
       contents: read
       security-events: write
     env:
-      HYPATIA_SHA: 'd73f76b5cb7a35e1aa1024c916aee7cb4f9b141e'
+      HYPATIA_SHA: '6693f9aed8e4383f78a3d01b600b32663bf7a45c'
     steps:
       - name: Checkout repository
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
@@ -53,7 +53,7 @@ jobs:
             ~/hypatia
             ~/.hex
             ~/.mix
-          key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-d73f76b5cb7a35e1aa1024c916aee7cb4f9b141e
+          key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-6693f9aed8e4383f78a3d01b600b32663bf7a45c
 
       - name: Build pinned Hypatia scanner
         run: |
diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml
index db5f05e..241c96c 100644
--- a/.github/workflows/proven-tests.yml
+++ b/.github/workflows/proven-tests.yml
@@ -56,8 +56,8 @@ jobs:
           git init -q "$r"
           git -C "$r" remote add origin https://github.com/metadatastician/standards.git
           git -C "$r" config core.sparseCheckout true
-          printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout"
-          git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4
+          printf '1-formats/deed/tools/\nscripts/check-proof-receipt.sh\nscripts/proof-inputs-sha256.sh\n' > "$r/.git/info/sparse-checkout"
+          git -C "$r" fetch -q --depth 1 origin e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d
           git -C "$r" checkout -q FETCH_HEAD
           for f in verification/receipts/*_praxis.deed; do
             bun "$r/1-formats/deed/tools/deed_lint.js" --proof-receipt-json "$f"
diff --git a/Justfile b/Justfile
index 141e7d1..b9034c1 100644
--- a/Justfile
+++ b/Justfile
@@ -707,7 +707,7 @@ uncloak:
 # The Mathesis golden path (re-anchoring plan WO 2.5). CI runs it in the pinned
 # Guix (agda-proof-policy.yml). A stale view or a failing proof fails.
 # Golden path: every generated view matches its data, every gated proof checks
-check: check-views site-check check-proofs
+check: check-views site-check check-proofs receipt-check
 
 # Needs bun, network for the receipts, and MATHESIS_STANDARDS (see `registry`).
 # Views current: catalogue, census tests, atlas, claims registry, bridges and
@@ -772,6 +772,14 @@ registry-check:
     bun scripts/registry/theory-ledger.mjs verify
     bun test tests/registry/
 
+# The git checks of PROOF-POLICY §8.5.3 on the receipt of Mathesis: its
+# :source-commit is on origin/main, each current receipt's inputs manifest holds
+# at its commit, and each echo's witness holds. The shared checker of the pinned
+# standards commit runs them (MATHESIS_STANDARDS, as above). Needs origin/main
+# with its history.
+receipt-check:
+    bun scripts/registry/claims-registry.mjs receipt
+
 # Append each change of the theory shelf to docs/theory/ledger.jsonl, the only
 # way the ledger changes (needs MATHESIS_STANDARDS, as above). A note tells the
 # story: just theory-ledger "THY-2 admitted after its Lean leg landed"
diff --git a/build/manifest.scm b/build/manifest.scm
index 34259e6..3a2303d 100644
--- a/build/manifest.scm
+++ b/build/manifest.scm
@@ -13,6 +13,9 @@
 (specifications->manifest
  (list "git" "bash" "coreutils" "nss-certs" "just" "mise"
        "shellcheck" "chez-scheme" "gmp" "gcc-toolchain" "zig"
+       ;; jq: the shared git checker of proof receipts (PROOF-POLICY §8.5.3) reads
+       ;; the reader's JSON with it.
+       "jq"
        ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)).
        ;; No agda-stdlib: its Guix package does not build, and no proof here
        ;; imports it (owner ruling 2026-11-10).
diff --git a/docs/atlas/claims/claims.jsonl b/docs/atlas/claims/claims.jsonl
index ac21f92..adcbd1e 100644
--- a/docs/atlas/claims/claims.jsonl
+++ b/docs/atlas/claims/claims.jsonl
@@ -1,12 +1,12 @@
-{"agda":{"module":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference","names":["eval-low"]},"claim":"N-2","id":"hyperpolymath/secret-types#N-2","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Public expressions read the same in low-equivalent stores","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference","names":["confine"]},"claim":"N-3","id":"hyperpolymath/secret-types#N-3","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Confinement: under a secret program counter the public variable is unchanged, loops included","status_doc":"PROOF-STATUS.adoc"}
-{"agda":null,"claim":"N-4","id":"hyperpolymath/secret-types#N-4","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks","status_doc":"PROOF-STATUS.adoc"}
-{"agda":null,"claim":"N-5","id":"hyperpolymath/secret-types#N-5","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another","status_doc":"PROOF-STATUS.adoc"}
-{"agda":null,"claim":"N-6","id":"hyperpolymath/secret-types#N-6","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate)","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference.Generic","names":["tini"]},"claim":"N-7","id":"hyperpolymath/secret-types#N-7","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Countermodels","names":["NoUpper₁.refutes","NoUpper₂.refutes","NoDownClosure.refutes","NoTrans.refutes"]},"claim":"N-8","id":"hyperpolymath/secret-types#N-8","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference.OutcomeVisibility","names":["termination-sensitive-fails"]},"claim":"N-9","id":"hyperpolymath/secret-types#N-9","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference","names":["eval-low"]},"claim":"N-2","id":"hyperpolymath/secret-types#N-2","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Public expressions read the same in low-equivalent stores","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference","names":["confine"]},"claim":"N-3","id":"hyperpolymath/secret-types#N-3","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Confinement: under a secret program counter the public variable is unchanged, loops included","status_doc":"PROOF-STATUS.adoc"}
+{"agda":null,"claim":"N-4","id":"hyperpolymath/secret-types#N-4","kind":"demonstration","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks","status_doc":"PROOF-STATUS.adoc"}
+{"agda":null,"claim":"N-5","id":"hyperpolymath/secret-types#N-5","kind":"demonstration","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another","status_doc":"PROOF-STATUS.adoc"}
+{"agda":null,"claim":"N-6","id":"hyperpolymath/secret-types#N-6","kind":"demonstration","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate)","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference.Generic","names":["tini"]},"claim":"N-7","id":"hyperpolymath/secret-types#N-7","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Countermodels","names":["NoUpper₁.refutes","NoUpper₂.refutes","NoDownClosure.refutes","NoTrans.refutes"]},"claim":"N-8","id":"hyperpolymath/secret-types#N-8","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference.OutcomeVisibility","names":["termination-sensitive-fails"]},"claim":"N-9","id":"hyperpolymath/secret-types#N-9","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules","status_doc":"PROOF-STATUS.adoc"}
 {"agda":{"module":"Lintel.Lattice","names":["⊑-refl","⊑-trans","⊑-antisym","⊔-upper₁","⊔-upper₂","⊔-least","⊓-lower₁","⊓-lower₂","⊓-greatest","anyone-least","no-one-greatest","no-one-⋢-anyone","_⊑?_"]},"claim":"L-1","id":"metadatastician/lintel#L-1","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"A lattice, not just a poset: ⊑ is a decidable partial order, ⊔ and ⊓ are least upper and greatest lower bounds, anyone is least and no-one greatest","status_doc":"README.adoc"}
 {"agda":{"module":"Lintel.Lattice","names":["⊑-readers","readers-⊑","observes-flow","flow-observes"]},"claim":"L-2","id":"metadatastician/lintel#L-2","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"⊑ is reverse inclusion of reader sets; a role sees a label exactly when the label may flow to that role's observer level","status_doc":"README.adoc"}
 {"agda":{"module":"Lintel.Instance","names":["reader-sets"]},"claim":"L-3","id":"metadatastician/lintel#L-3","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"The laws secret-types' generic TINI needs hold here, packed as an instance of its Lattice record","status_doc":"README.adoc"}
diff --git a/docs/atlas/generated/registry.adoc b/docs/atlas/generated/registry.adoc
index b5904f6..8d796c6 100644
--- a/docs/atlas/generated/registry.adoc
+++ b/docs/atlas/generated/registry.adoc
@@ -5,36 +5,36 @@
 
 Each row is a claim in its home repository at a pinned commit. The grade is
 *derived* here from that repository's receipt by the canon reader of
-PROOF-POLICY §8.5.1 (`metadatastician/standards` at `be39f900665f`), never
+PROOF-POLICY §8.5.1 (`metadatastician/standards` at `e5a39d7e5c66`), never
 assigned (§8.5). A grade is not a discharge (§8.4): `PWG-3` theorems still
 owe their Rocq and Lean legs. Status of this slice: accepted in
 link:../../decisions/0004-claims-registry.adoc[ADR 0004], ratified by the owner.
 
-Census: 1 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 12 `ungraded`, of 13 theorems. 5 demonstrations and assumptions are listed and not graded.
+Census: 6 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 7 `ungraded`, of 13 theorems. 5 demonstrations and assumptions are listed and not graded.
 
 [cols="2,1,1,4,3",options="header"]
 |===
 |Claim |Kind |PWG |Statement (home repository's wording) |Why not higher
 
-|https://github.com/hyperpolymath/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2`; the receipt describes `336768958d01` |theorem |`PWG-1` |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. (`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`) |—
+|https://github.com/hyperpolymath/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2` |theorem |`ungraded` |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. (`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`) |the canon reader refuses the receipt: a receipt of the agda leg of claim "THY-1" is current and is missing :inputs-sha256 (§8.5.1)
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-1] at `eee4e4038503` |theorem |`ungraded` |TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent (`SecretTypes.Noninterference`: `tini`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-1] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent (`SecretTypes.Noninterference`: `tini`) |—
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-2] at `eee4e4038503` |theorem |`ungraded` |Public expressions read the same in low-equivalent stores (`SecretTypes.Noninterference`: `eval-low`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-2] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |Public expressions read the same in low-equivalent stores (`SecretTypes.Noninterference`: `eval-low`) |—
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-3] at `eee4e4038503` |theorem |`ungraded` |Confinement: under a secret program counter the public variable is unchanged, loops included (`SecretTypes.Noninterference`: `confine`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-3] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |Confinement: under a secret program counter the public variable is unchanged, loops included (`SecretTypes.Noninterference`: `confine`) |—
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-4] at `eee4e4038503` |demonstration |`ungraded` |The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks |demonstration, not a theorem (§8.1)
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-4] at `4ed067220f13` |demonstration |`ungraded` |The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks |demonstration, not a theorem (§8.1)
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-5] at `eee4e4038503` |demonstration |`ungraded` |Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another |demonstration, not a theorem (§8.1)
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-5] at `4ed067220f13` |demonstration |`ungraded` |Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another |demonstration, not a theorem (§8.1)
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-6] at `eee4e4038503` |demonstration |`ungraded` |Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate) |demonstration, not a theorem (§8.1)
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-6] at `4ed067220f13` |demonstration |`ungraded` |Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate) |demonstration, not a theorem (§8.1)
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-7] at `eee4e4038503` |theorem |`ungraded` |TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it (`SecretTypes.Noninterference.Generic`: `tini`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-7] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it (`SecretTypes.Noninterference.Generic`: `tini`) |—
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-8] at `eee4e4038503` |theorem |`ungraded` |Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers (`SecretTypes.Countermodels`: `NoUpper₁.refutes`, `NoUpper₂.refutes`, `NoDownClosure.refutes`, `NoTrans.refutes`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-8] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers (`SecretTypes.Countermodels`: `NoUpper₁.refutes`, `NoUpper₂.refutes`, `NoDownClosure.refutes`, `NoTrans.refutes`) |—
 
-|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-9] at `eee4e4038503` |theorem |`ungraded` |If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules (`SecretTypes.Noninterference.OutcomeVisibility`: `termination-sensitive-fails`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt
+|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-9] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules (`SecretTypes.Noninterference.OutcomeVisibility`: `termination-sensitive-fails`) |—
 
 |https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#A-1] at `a0f2bae9cac0` |assumption |`ungraded` |Non-collusion: no party holds both the proxy and the target role (the gap is proved: collusion-gap) |assumption, not a theorem (§8.1)
 
diff --git a/docs/decisions/0004-claims-registry.adoc b/docs/decisions/0004-claims-registry.adoc
index a0bc3b1..70614a7 100644
--- a/docs/decisions/0004-claims-registry.adoc
+++ b/docs/decisions/0004-claims-registry.adoc
@@ -92,6 +92,15 @@ if its sha256 differs from the pinned digest, and derives:
   `ungraded`;
 . otherwise the grade that the reader derives for the claim, from `PWG-3` to
   `PWG-1` (§8.2).
+. a `PWG-1` stays only when the git checks of §8.5.3 hold (amendment
+  2026-11-13): the shared checker of the pinned standards commit
+  (`scripts/check-proof-receipt.sh`, pinned by digest with the digest script
+  that it calls, `CHECKER` in `scripts/registry/claims-registry.mjs`) runs
+  against a clone of the home repository that holds its pull-request heads.
+  It checks that the receipt's `:source-commit` is on the default branch, that
+  each current receipt's inputs manifest holds at its commit, and that each
+  echo's witness holds at both ends. If a check fails or cannot run, the
+  registry catalogues `PWG-2ii` and records why (§8.5.2).
 
 Until this amendment the registry carried its own copy of the §8.2 rules, read
 only the Agda side, and never derived `PWG-1`.
diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc
index edf291a..104efd4 100644
--- a/docs/status/PROOF-NEEDS.adoc
+++ b/docs/status/PROOF-NEEDS.adoc
@@ -42,7 +42,7 @@ missing input is missing, in every period after it too, and never zero. A
 verdict is "no" on a known breach and otherwise missing when any value it
 depends on is missing; it is never "yes" then
 |Agda, re-checked in Rocq and Lean
-|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2)
 |`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean`
 
 |APP-2
@@ -50,7 +50,7 @@ depends on is missing; it is never "yes" then
 plus, summed over the periods, receipts minus payments; when a value is
 missing, both sides are missing
 |Agda, re-checked in Rocq and Lean
-|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2)
 |`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`); Rocq and Lean: `cash_identity`
 
 |APP-3
@@ -58,14 +58,14 @@ missing, both sides are missing
 keeps every closing balance at or above its floor, and no smaller
 non-negative amount does
 |Agda, re-checked in Rocq and Lean
-|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2)
 |`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`); Rocq and Lean: `gap_sound`, `gap_least`
 
 |APP-4
 |Status never upgrades: the evidence status of an output is never stronger
 than the weakest status of the inputs that it depends on
 |Agda, re-checked in Rocq and Lean
-|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2)
+|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2)
 |`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean`
 |===
 
@@ -84,7 +84,8 @@ the integer instance of the worked examples is one. The Rocq and Lean legs
 restate the same definitions and re-prove every theorem, the integer laws
 included. Every module is gated: no postulate in an Agda import cone, every
 Rocq theorem closed under the global context, and no axiom in any Lean
-theorem. No receipt records these legs yet, so no grade is derived.
+theorem. The receipt `verification/receipts/theory_praxis.deed` records the
+three legs of each, and the canon reader derives `PWG-1` for each (2026-11-13).
 
 No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed
 declares neither capability.
diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc
index 411ff8e..4e4ade1 100644
--- a/docs/status/PROOF-STATUS.adoc
+++ b/docs/status/PROOF-STATUS.adoc
@@ -26,7 +26,7 @@ reader of PROOF-POLICY §8.5.1.
 |APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2)
 |Proved in Agda, Rocq and Lean
 |-
-|The record below. No receipt yet, so no grade is derived
+|The record below. The receipt derives `PWG-1` (2026-11-13)
 |===
 
 *Overall*: 5 of 6 obligations are proved in all three provers; THY-1 alone has
@@ -83,10 +83,13 @@ missing crate as missing from every build.
   monotonicity step.
 * Axioms: none.
 * Receipt state: superseded on 2026-11-10 by the CI receipt below.
-* CI receipt (current): Agda 2.7.0.1 in the pinned Guix (`8edb9da`), same
-  invocation, at commit `336768958d01`, run 42896264290. The file SHA-256 is
-  unchanged, and the log reports no postulate in the cone (`Agda.Primitive`,
-  `FeatureReachability`).
+* CI receipt (superseded on 2026-11-13): Agda 2.7.0.1 in the pinned Guix
+  (`8edb9da`), same invocation, at commit `336768958d01`, run 42896264290.
+  The file SHA-256 is unchanged, and the log reports no postulate in the cone
+  (`Agda.Primitive`, `FeatureReachability`).
+* CI receipt (current, 2026-11-13): the same, at main `034f215`, run
+  43498592499. It records the inputs manifest and the axioms (none) that
+  PROOF-POLICY §8.5.1 now requires (standards `e5a39d7`).
 
 |Rocq leg
 |`PROVEN`, route `re-proved`, correspondence `RECONCILED`. Receipt:
@@ -194,7 +197,7 @@ same reader derives
 |`pwg`
 |`1` (since 2026-11-10): `PWG-2ii`, and every counted witness has a current
 receipt from one headless, isolated, pinned CI run on the exact source commit
-`336768958d01` (PROOF-POLICY §8.2). The grade holds while those receipts stay
+(PROOF-POLICY §8.2): `336768958d01` until 2026-11-13, `034f215` since. The grade holds while those receipts stay
 current: a later commit that breaks a leg, or a run that cannot be repeated,
 drops it (§8.4). Before 2026-11-10 it was `2ii`, because each receipt came
 from a local run.
@@ -261,9 +264,14 @@ is `cash_identity`, and so on). The differences are encoding only:
 Residual assumptions: none in any leg.
 
 |Machine receipt (§8.5.1)
-|None yet. The receipt `verification/receipts/theory_praxis.deed` records
-THY-1 only. Adding APP-1 to APP-4 needs receipts from a CI run on the merged
-commit, so no grade is derived for them yet.
+|`verification/receipts/theory_praxis.deed`, with THY-1. The current receipts
+come from CI run 43498592499 on main `034f215` (Agda 2.7.0.1, Rocq 8.18.0,
+Lean 4.29.0, pinned Guix `8edb9da`). Each records the inputs manifest of its
+prover and no axiom. The canon reader at standards `e5a39d7` derives `PWG-1`
+for each of APP-1 to APP-4, and the shared git checker (`just receipt-check`)
+passes. The Rocq and Lean legs are `RECONCILED` by the comparison above, done
+by reading. The trusted base gains `Char` and `String`, the postulates that
+`Applied/IntLaws` reaches through `Agda.Builtin.Int`.
 |===
 
 == Verification commands
@@ -284,6 +292,14 @@ bash tests/proofs/gate_controls_test.sh agda
 |===
 |Date |Change
 
+|2026-11-13
+|The receipt is written again under PROOF-POLICY §8.5.1 at standards
+`e5a39d7`: each current receipt records its inputs manifest and its axioms.
+THY-1 is earned again, and APP-1 to APP-4 are added, from CI run 43498592499
+on main `034f215`. The reader derives `PWG-1` for all five. The claims
+registry shows THY-1 as `ungraded` until its claim pin moves to the new
+receipt (the next change).
+
 |2026-11-10
 |THY-1 receipts earned again at Agda 2.7.0.1 and Lean 4.29.0 in the pinned
 Guix shell; the receipt derives `PWG-1`.
diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc
index c6f9c5d..39b3fda 100644
--- a/docs/status/ROADMAP.adoc
+++ b/docs/status/ROADMAP.adoc
@@ -220,6 +220,25 @@ One pull request that changes census rows is open at a time (atlas README,
   the owner's act.
 * Finding: the `intend` contract still marks stage 3 `in_progress` and
   stage 4 `declared`; a contract edit needs owner review.
+* Receipts under the new PROOF-POLICY §8.5.1 to §8.5.3 (owner rulings
+  2026-11-13; standards PRs 1534 and 1545, merged at `e5a39d7`): every current
+  receipt records its inputs manifest, its inputs digest and its axioms; an
+  `(echo …)` record carries a receipt across a squash or rebase; the home gate
+  and consumers run the shared git checker.
+** First change: the Mathesis receipt is written again from CI run
+   43498592499 on main `034f215`. It adds APP-1 to APP-4 and earns THY-1
+   again; the reader derives `PWG-1` for all five, and `just receipt-check`
+   (the home gate, in `just check`) passes. The registry pins the new reader
+   and catalogues a `PWG-1` only when the git checks hold. Until the next
+   change, the registry shows THY-1 as `ungraded`, because its claim pin names
+   the old receipt; the theory ledger records this.
+** The same change pins the nine secret-types claims at its main `4ed0672`
+   (re-anchoring plan WO 5.1). Its receipt names `292d566`, with the echo
+   `7dfeab2` to `292d566` for the squash merge of its pull request 40. The
+   reader derives `PWG-1` for N-1, N-2, N-3, N-7, N-8 and N-9, and the
+   registry's git checks hold, so the registry catalogues six `PWG-1`.
+** Next change: the claim pins of THY-1 and APP-1 to APP-4 (applied shelf, a
+   new `shelf` field).
 
 [[stages]]
 == Stages
diff --git a/docs/theory/generated/index.adoc b/docs/theory/generated/index.adoc
index 552f85a..cb2cd98 100644
--- a/docs/theory/generated/index.adoc
+++ b/docs/theory/generated/index.adoc
@@ -13,6 +13,6 @@ Theorems: 1.
 |===
 |Theorem |Statement |PWG |Source and receipt |Dependant
 
-|THY-1 |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. |`PWG-1` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `9aa1662da5b2` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build.
+|THY-1 |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. |`ungraded` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `9aa1662da5b2` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build.
 
 |===
diff --git a/docs/theory/ledger.jsonl b/docs/theory/ledger.jsonl
index 93f31e3..1a76a90 100644
--- a/docs/theory/ledger.jsonl
+++ b/docs/theory/ledger.jsonl
@@ -1 +1,2 @@
 {"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","date":"2026-11-11","event":"admitted","id":"hyperpolymath/mathesis#THY-1","note":"The ledger starts here, on 2026-11-11. THY-1 was proved in Agda on 2026-11-09 and re-proved in Rocq and Lean; it derived PWG-2ii until the CI receipts of run 42896264290 gave PWG-1 on 2026-11-10. Transport from Agda was blocked, because the Lambdapi exports to Rocq and Lean drop rewrite rules. Earlier history is in git and docs/status/PROOF-STATUS.adoc.","pwg":"PWG-1","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":1}
+{"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","changes":["pwg"],"date":"2026-11-13","event":"changed","id":"hyperpolymath/mathesis#THY-1","note":"The reader pin moved to standards e5a39d7, which requires an inputs manifest, the axioms and the inputs digest on every current receipt. The receipt that THY-1's claim pin names predates them, so the reader refuses it. The Mathesis receipt is regenerated in the same change, and the next change moves THY-1's pin to it.","pwg":"ungraded","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":2}
diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs
index c3801a7..78dfd32 100644
--- a/scripts/registry/claims-registry.mjs
+++ b/scripts/registry/claims-registry.mjs
@@ -22,7 +22,10 @@
 // the reader at READER.commit; the reader's sha256 must equal READER.sha256.
 // --receipts-dir DIR reads receipts from DIR/<owner>__<repo>@<commit>/<path>
 // instead of fetching them (the tests use it; CI fetches).
-import {readFile, writeFile, mkdir} from 'node:fs/promises';
+import {readFile, writeFile, mkdir, mkdtemp, rm} from 'node:fs/promises';
+import {existsSync} from 'node:fs';
+import {spawnSync} from 'node:child_process';
+import {tmpdir} from 'node:os';
 import {createHash} from 'node:crypto';
 import {fileURLToPath, pathToFileURL} from 'node:url';
 import path from 'node:path';
@@ -60,9 +63,19 @@ const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']);
 // that is not this file is refused, so a grade never comes from an unpinned rule.
 export const READER = {
   repository: 'metadatastician/standards',
-  commit: 'be39f900665fb7c042c05d1165da018adc1860f4',
+  commit: 'e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d',
   path: '1-formats/deed/tools/deed_lint.js',
-  sha256: 'f7e2b91905f0d99e5cabab59385073afb695be8b9f2d0591257a6a6fd62e25e3',
+  sha256: '37ff85be499b35dd9d74399e05d9ae1e57ccf095362c355f93e04b3bbf4c9491',
+};
+
+// The git checks of PROOF-POLICY §8.5.3, from the same standards commit as the
+// reader. A PWG-1 is catalogued only when the checker passes against a clone of
+// the home repository; the checker calls the digest script, so both are pinned.
+export const CHECKER = {
+  path: 'scripts/check-proof-receipt.sh',
+  sha256: '831f5a43c906c3edc8cfa68ab5fe13c37e7a41b35e40068481d988d887f4bd3f',
+  digest: 'scripts/proof-inputs-sha256.sh',
+  digestSha256: 'dfc6dde01a3a79df638eebe4cad0eae584d8f17280077e149174c0667e9508f4',
 };
 
 // ── Validation of the registry rows ──────────────────────────────────────────
@@ -155,30 +168,116 @@ async function loadReceipt(row, receiptsDir) {
   return text;
 }
 
-// Derive every row, reading each distinct receipt once. A receipt that the
-// reader refuses gives `ungraded` with the reader's reason; a receipt that
-// cannot be fetched or fails its digest stops the run.
-export async function deriveAll(rows, receiptsDir, readProofReceipt) {
-  const cache = new Map();
-  const out = [];
-  for (const row of rows) {
-    let read = null;
-    if (row.receipt !== null) {
-      const key = `${row.repo}@${row.source_commit}/${row.receipt.path}`;
-      if (!cache.has(key)) {
-        const text = await loadReceipt(row, receiptsDir);
-        try {
-          cache.set(key, {record: readProofReceipt(text, path.basename(row.receipt.path))});
-        } catch (e) {
-          if (!['LintError', 'ProofReceiptError'].includes(e?.name)) throw e;
-          cache.set(key, {refusal: String(e)});
-        }
-      }
-      read = cache.get(key);
+// ── The git checks of PROOF-POLICY §8.5.3 ────────────────────────────────────
+
+// A consumer catalogues a PWG-1 only when the git checks hold against the home
+// repository; otherwise it catalogues the grade without PWG-1 (PWG-2ii, §8.5.2)
+// and records why. `check` is {ok, reason}.
+export function withGitCheck(d, check) {
+  if (d.pwg !== 'PWG-1' || check.ok) return d;
+  return {...d, pwg: 'PWG-2ii', reasons: [...d.reasons, `§8.5.3 git checks: ${check.reason}; catalogued without PWG-1`]};
+}
+
+// A program in an absolute directory of PATH, run by its absolute path, so that no
+// relative PATH entry can pick the program.
+export function findTool(name, env = process.env) {
+  for (const d of (env.PATH || '').split(path.delimiter)) {
+    if (path.isAbsolute(d) && existsSync(path.join(d, name))) return path.join(d, name);
+  }
+  throw new Error(`${name} not found in an absolute directory of PATH`);
+}
+
+// A program that cannot be found or launched gives a failed result (status null),
+// so the git check reports it instead of stopping the derivation.
+const run = (cmd, args) => {
+  try {
+    const r = spawnSync(findTool(cmd), args, {encoding: 'utf8'});
+    return r.error ? {status: null, stdout: '', stderr: String(r.error.message)} : r;
+  } catch (e) {
+    return {status: null, stdout: '', stderr: e.message};
+  }
+};
+
+// The path of the pinned checker, after the digest checks of both pinned
+// scripts and of the canon reader that the checker runs, in the standards
+// checkout. The `receipt` home gate runs the checker without loadReader().
+export async function checkerScript(standardsDir = process.env.MATHESIS_STANDARDS) {
+  const pinned = async (rel, sha) => {
+    const file = path.resolve(standardsDir, rel);
+    const digest = createHash('sha256').update(await readFile(file)).digest('hex');
+    if (digest !== sha) throw new Error(`${file} is not the pinned file (sha256 ${digest}, pinned ${sha} at ${READER.commit})`);
+    return file;
+  };
+  await pinned(READER.path, READER.sha256);
+  await pinned(CHECKER.digest, CHECKER.digestSha256);
+  return pinned(CHECKER.path, CHECKER.sha256);
+}
+
+// The shared checker of the standards checkout, after the digest checks of both
+// pinned scripts. It returns (row, text) => {ok, reason}, cloning each home
+// repository once, with the pull-request heads that a squashed echo source needs.
+export async function gitChecker(standardsDir = process.env.MATHESIS_STANDARDS) {
+  const script = await checkerScript(standardsDir);
+  const work = await mkdtemp(path.join(tmpdir(), 'mathesis-git-'));
+  const clones = new Map();
+  const clone = repo => {
+    if (!clones.has(repo)) {
+      const dir = path.join(work, repo.replace('/', '__'));
+      const steps = [
+        ['git', ['clone', '-q', '--filter=blob:none', '--no-checkout', `https://github.com/${repo}`, dir]],
+        ['git', ['-C', dir, 'fetch', '-q', 'origin', '+refs/pull/*/head:refs/pull/*/head']],
+      ];
+      const failed = steps.map(([c, a]) => run(c, a)).find(r => r.status !== 0);
+      const head = failed ? null : run('git', ['-C', dir, 'symbolic-ref', '--short', 'refs/remotes/origin/HEAD']);
+      clones.set(repo, failed || head.status !== 0
+        ? {reason: `could not clone ${repo}: ${(failed || head).stderr.trim().split('\n').pop()}`}
+        : {dir, branch: head.stdout.trim()});
     }
-    out.push({row, ...derive(row, read)});
+    return clones.get(repo);
+  };
+  const check = async (row, text) => {
+    const c = clone(row.repo);
+    if (!c.dir) return {ok: false, reason: c.reason};
+    const file = path.join(await mkdtemp(path.join(work, 'r-')), path.basename(row.receipt.path));
+    await writeFile(file, text);
+    const r = run('bash', [script, '--branch', c.branch, file, c.dir]);
+    if (r.status === 0) return {ok: true};
+    const why = `${r.stdout}${r.stderr}`.trim().split('\n').filter(l => !l.startsWith('ok ')).slice(-2).join('; ');
+    return {ok: false, reason: `check-proof-receipt.sh exit ${r.status}: ${why}`};
+  };
+  // The clones and receipt copies live in `work` only; remove it when done.
+  check.cleanup = () => rm(work, {recursive: true, force: true});
+  return check;
+}
+
+// The reader's record of one receipt text: {record, text} or {refusal}.
+function readReceipt(text, row, readProofReceipt) {
+  try {
+    return {record: readProofReceipt(text, path.basename(row.receipt.path)), text};
+  } catch (e) {
+    if (!['LintError', 'ProofReceiptError'].includes(e?.name)) throw e;
+    return {refusal: String(e)};
   }
-  return out;
+}
+
+// The pinned digest is part of the key, so each row is checked against its own pin.
+const receiptKey = row =>
+  row.receipt === null ? null : `${row.repo}@${row.source_commit}/${row.receipt.path}#${row.receipt.sha256}`;
+
+// Derive every row, reading each distinct receipt once. A receipt that the
+// reader refuses gives `ungraded` with the reader's reason; a receipt that
+// cannot be fetched or fails its digest stops the run. Each receipt that gives
+// a PWG-1 goes once through `gitCheck` (§8.5.3); with none, no PWG-1 is
+// catalogued.
+export async function deriveAll(rows, receiptsDir, readProofReceipt, gitCheck = null) {
+  const once = list => [...new Map(list.map(row => [receiptKey(row), row]))];
+  const reads = new Map(await Promise.all(once(rows.filter(receiptKey)).map(async ([key, row]) =>
+    [key, readReceipt(await loadReceipt(row, receiptsDir), row, readProofReceipt)])));
+  const derived = rows.map(row => ({row, ...derive(row, reads.get(receiptKey(row)) ?? null)}));
+  const graded = derived.filter(d => d.pwg === 'PWG-1').map(d => d.row);
+  const checks = new Map(await Promise.all(once(graded).map(async ([key, row]) =>
+    [key, gitCheck ? await gitCheck(row, reads.get(key).text) : {ok: false, reason: 'no git check ran'}])));
+  return derived.map(d => (d.pwg === 'PWG-1' ? withGitCheck(d, checks.get(receiptKey(d.row))) : d));
 }
 
 // ── Rendering ────────────────────────────────────────────────────────────────
@@ -230,8 +329,15 @@ export function render(derived) {
 
 async function main() {
   const [cmd, ...args] = process.argv.slice(2);
+  if (cmd === 'receipt') {
+    // The home gate (§8.5.3): the git checks on the receipt of Mathesis itself,
+    // against this clone. origin/main needs its history (CI fetches it).
+    const receipt = path.join(root, 'verification/receipts/theory_praxis.deed');
+    const r = spawnSync(findTool('bash'), [await checkerScript(), '--branch', 'origin/main', receipt, root], {stdio: 'inherit'});
+    process.exit(r.status ?? 2);
+  }
   if (!['build', 'check', 'ledger'].includes(cmd)) {
-    console.error('usage: claims-registry.mjs build|check|ledger [--receipts-dir DIR] [--note TEXT]');
+    console.error('usage: claims-registry.mjs build|check|ledger|receipt [--receipts-dir DIR] [--note TEXT]');
     process.exit(2);
   }
   const i = args.indexOf('--receipts-dir');
@@ -240,7 +346,13 @@ async function main() {
   const rows = validate(await readJsonl(claimsFile), inventory);
   const bridges = validateBridges(await readJsonl(bridgesFile), inventory);
   const admissions = validateAdmissions(await readJsonl(admissionsFile), rows, inventory);
-  const derived = await deriveAll(rows, receiptsDir, await loadReader());
+  const gitCheck = receiptsDir ? null : await gitChecker();
+  let derived;
+  try {
+    derived = await deriveAll(rows, receiptsDir, await loadReader(), gitCheck);
+  } finally {
+    await gitCheck?.cleanup();
+  }
   const ledger = validateLedger(await readJsonl(ledgerFile));
   const current = snapshot(rows, admissions, new Map(derived.map(d => [d.row.id, d.pwg])));
   if (cmd === 'ledger') {
diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs
index 92b515d..27b12b6 100644
--- a/tests/registry/claims-registry.test.mjs
+++ b/tests/registry/claims-registry.test.mjs
@@ -9,7 +9,7 @@ import {readFileSync, mkdtempSync, mkdirSync, writeFileSync, copyFileSync} from
 import {createHash} from 'node:crypto';
 import {tmpdir} from 'node:os';
 import path from 'node:path';
-import {validate, loadReader, derive, deriveAll, render, READER} from '../../scripts/registry/claims-registry.mjs';
+import {validate, loadReader, derive, deriveAll, withGitCheck, findTool, gitChecker, checkerScript, render, READER, CHECKER} from '../../scripts/registry/claims-registry.mjs';
 import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs';
 
 const rows = parseJsonl(readFileSync(new URL('../../docs/atlas/claims/claims.jsonl', import.meta.url), 'utf8'));
@@ -28,8 +28,15 @@ beforeAll(async () => { readProofReceipt = await loadReader(); });
 // that leg's current receipt.
 const fixture = ({repo = 'o/r', pwg = 'PWG-3', invocation = 'agda --safe --without-K --cubical-compatible M.agda',
   rocq = null, lean = null, rocqAt = commit, leanAt = commit} = {}) => {
-  const run = (prover, at, inv) =>
-    `      (receipt :run "ci" :commit "${at}" :checker "${prover}" :invocation "${inv}" :state current))\n`;
+  // Each current receipt lists its inputs (standards e5a39d7): one manifest line,
+  // the digest of that manifest, and an empty axioms clause.
+  const run = (prover, at, inv) => {
+    const line = `${'c'.repeat(64)}  ${prover}/M\n`;
+    const digest = createHash('sha256').update(line).digest('hex');
+    return `      (receipt :run "ci" :commit "${at}" :checker "${prover}" :invocation "${inv}"\n` +
+      `               :inputs-sha256 "${digest}" :state current (axioms)\n` +
+      `               (inputs-manifest (file :path "${prover}/M" :sha256 "${'c'.repeat(64)}"))))\n`;
+  };
   const leg = (prover, state, at) => state === null ? '' :
     `    (leg :prover ${prover} :route re-proved :token proven :state ${state}\n` + run(prover, at, `${prover} M`);
   return ';; SPDX-License-Identifier: CC-BY-SA-4.0\n(praxis-deed\n  :schema-version "1.0.0"\n' +
@@ -108,6 +115,9 @@ test('deriveAll reads each receipt once, and refuses a receipt that does not mat
   const good = {...theorem, receipt: {path: 'r_praxis.deed', sha256: createHash('sha256').update(text).digest('hex')}};
   expect((await deriveAll([good], dir, readProofReceipt))[0].pwg).toBe('PWG-3');
   await expect(deriveAll([{...good, receipt: {path: 'r_praxis.deed', sha256: 'b'.repeat(64)}}], dir, readProofReceipt)).rejects.toThrow(/digest mismatch/);
+  // Each row is checked against its own pin: a second row with a wrong digest for
+  // the same receipt is not hidden behind the first.
+  await expect(deriveAll([good, {...good, id: 'o/r#T-1b', receipt: {path: 'r_praxis.deed', sha256: 'b'.repeat(64)}}], dir, readProofReceipt)).rejects.toThrow(/digest mismatch/);
 });
 
 test('the view is a census with its denominator, never a percentage, and is deterministic', () => {
@@ -126,3 +136,55 @@ test('a row names the commit that its receipt describes when it differs from the
   expect(v).toContain(`at \`${at.slice(0, 12)}\`; the receipt describes \`${commit.slice(0, 12)}\``);
   expect(render([{row: theorem, pwg: 'PWG-1', reasons: [], evidence: commit}])).not.toContain('the receipt describes');
 });
+
+test('a PWG-1 is catalogued only when the git checks of §8.5.3 hold', async () => {
+  const one = derive(theorem, read(fixture({pwg: 'PWG-1', rocq: 'RECONCILED', lean: 'RECONCILED'})));
+  expect(withGitCheck(one, {ok: true})).toEqual(one);
+  const capped = withGitCheck(one, {ok: false, reason: 'the source commit is not on origin/main'});
+  expect(capped.pwg).toBe('PWG-2ii');
+  expect(capped.reasons.join()).toContain('§8.5.3 git checks: the source commit is not on origin/main; catalogued without PWG-1');
+  const three = derive(theorem, read(fixture()));
+  expect(withGitCheck(three, {ok: false, reason: 'x'})).toEqual(three);
+  // deriveAll runs the check once per receipt, and with no check it catalogues no PWG-1.
+  const dir = mkdtempSync(path.join(tmpdir(), 'registry-'));
+  const text = fixture({pwg: 'PWG-1', rocq: 'RECONCILED', lean: 'RECONCILED'});
+  mkdirSync(path.join(dir, `o__r@${commit}`), {recursive: true});
+  writeFileSync(path.join(dir, `o__r@${commit}`, 'r_praxis.deed'), text);
+  const row = {...theorem, receipt: {path: 'r_praxis.deed', sha256: createHash('sha256').update(text).digest('hex')}};
+  let calls = 0;
+  const ok = async () => { calls += 1; return {ok: true}; };
+  const both = await deriveAll([row, {...row, id: 'o/r#T-1b'}], dir, readProofReceipt, ok);
+  expect(both.map(d => d.pwg)).toEqual(['PWG-1', 'PWG-1']);
+  expect(calls).toBe(1);
+  expect((await deriveAll([row], dir, readProofReceipt))[0].pwg).toBe('PWG-2ii');
+});
+
+test('git and bash run only from an absolute directory of PATH', () => {
+  expect(path.isAbsolute(findTool('bash'))).toBe(true);
+  expect(() => findTool('bash', {PATH: 'relative/bin'})).toThrow(/not found in an absolute directory/);
+});
+
+test('a git check that cannot run gives a failed result, not a crash', async () => {
+  const check = await gitChecker();
+  const saved = process.env.PATH;
+  process.env.PATH = '';
+  try {
+    const r = await check({...theorem, receipt: {path: 'r_praxis.deed', sha256: 'a'.repeat(64)}}, fixture());
+    expect(r.ok).toBe(false);
+    expect(r.reason).toMatch(/could not clone o\/r: git not found in an absolute directory of PATH/);
+  } finally {
+    process.env.PATH = saved;
+    await check.cleanup();
+  }
+});
+
+test('the checker runs only beside the pinned canon reader', async () => {
+  const std = mkdtempSync(path.join(tmpdir(), 'mathesis-std-'));
+  for (const rel of [READER.path, CHECKER.path, CHECKER.digest]) {
+    mkdirSync(path.dirname(path.join(std, rel)), {recursive: true});
+    copyFileSync(path.join(process.env.MATHESIS_STANDARDS, rel), path.join(std, rel));
+  }
+  expect(await checkerScript(std)).toBe(path.resolve(std, CHECKER.path));
+  writeFileSync(path.join(std, READER.path), '// changed\n', {flag: 'a'});
+  await expect(checkerScript(std)).rejects.toThrow(/is not the pinned file/);
+});
diff --git a/verification/receipts/theory_praxis.deed b/verification/receipts/theory_praxis.deed
index b336890..64ec114 100644
--- a/verification/receipts/theory_praxis.deed
+++ b/verification/receipts/theory_praxis.deed
@@ -1,35 +1,61 @@
 ;; SPDX-License-Identifier: CC-BY-SA-4.0
 ;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
-;; The proof receipt of Mathesis (PROOF-POLICY §8.5.1), written from the THY-1
-;; record in docs/status/PROOF-STATUS.adoc (re-anchoring plan WO 1.5). The
-;; current receipts come from one CI run of the proof lanes in the pinned Guix
-;; (WO 1.4, Guix 8edb9da). Its log records, for each witness, the checker and
-;; its version, the invocation, the SHA-256 of the file, the result and the
-;; axioms reported. The local runs of 2026-11-09 stay as superseded receipts.
-;; The reader in standards 1-formats/deed/tools/deed_lint.js derives the grade:
+;; The proof receipt of Mathesis (PROOF-POLICY §8.5.1, standards e5a39d7),
+;; written from the records of THY-1 and APP-1 to APP-4 in
+;; docs/status/PROOF-STATUS.adoc. The current receipts come from one CI run of
+;; the proof lanes in the pinned Guix (Guix 8edb9da) on main 034f215: run
+;; 43498592499. Its log records, for each gated module, the checker and its
+;; version, the SHA-256 of the file, the result and the axioms reported (none).
+;; Each current receipt carries the inputs manifest of its prover: the union of
+;; the first-party files that the graded roots read, from
+;;   standards scripts/proof-inputs-sha256.sh --manifest 034f215 PATH...
+;; One manifest per prover, because §8.5.1 allows one digest for one commit and
+;; one prover. Earlier receipts stay as superseded receipts, each with a reason.
+;; The reader derives the grade, and the shared git checker does the §8.5.3
+;; checks (just receipt-check):
 ;;   bun deed_lint.js --proof-receipt-json verification/receipts/theory_praxis.deed
-;; The trusted base is the Agda.Primitive block of the import cone that
-;; agda --dependency-graph reports for FeatureReachability; Agda 2.6.3 and
-;; 2.7.0.1 postulate the same four names there (checked 2026-11-10).
+;;   check-proof-receipt.sh --branch origin/main verification/receipts/theory_praxis.deed .
+;; The trusted base is each prover-supplied postulate that the Agda import
+;; cones reach (agda --dependency-graph): the four of Agda.Primitive, and Char
+;; and String, which Applied/IntLaws reaches through Agda.Builtin.Int. Agda
+;; 2.7.0.1 postulates these six (its lib/prim sources, read 2026-11-13).
 (praxis-deed
   :schema-version "1.0.0"
   :canonical-name "mathesis-theory-receipt"
   :beholding-chora #u5"estate/chora"
   :profile proof-receipt
   :repository "hyperpolymath/mathesis"
-  :source-commit "336768958d01257caae14cb81fb54197c2617d97"
+  :source-commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
   (trusted-base
     (primitive :prover agda :module "Agda.Primitive" :name "Level" :binding "BUILTIN LEVEL")
     (primitive :prover agda :module "Agda.Primitive" :name "lzero" :binding "BUILTIN LEVELZERO")
     (primitive :prover agda :module "Agda.Primitive" :name "lsuc" :binding "BUILTIN LEVELSUC")
-    (primitive :prover agda :module "Agda.Primitive" :name "_⊔_" :binding "BUILTIN LEVELMAX"))
+    (primitive :prover agda :module "Agda.Primitive" :name "_⊔_" :binding "BUILTIN LEVELMAX")
+    (primitive :prover agda :module "Agda.Builtin.Char" :name "Char" :binding "BUILTIN CHAR")
+    (primitive :prover agda :module "Agda.Builtin.String" :name "String" :binding "BUILTIN STRING"))
   (claim :id "THY-1" :pwg PWG-1 :foundation-diverse #f
     (leg :prover agda :route source :token proven :state AGDA-VERIFIED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "agda 2.7.0.1 (Guix 8edb9da)"
+               :invocation "agda --safe --without-K --cubical-compatible FeatureReachability.agda"
+               :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12")
+                 (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56")
+                 (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb")
+                 (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959")
+                 (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9")
+                 (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97")
+                 (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564")))
       (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/42896264290/job/130110238086"
                :commit "336768958d01257caae14cb81fb54197c2617d97"
                :checker "agda 2.7.0.1 (Guix 8edb9da)"
                :invocation "agda --safe --without-K --cubical-compatible FeatureReachability.agda"
-               :state current)
+               :state superseded
+               :reason "replaced by the CI receipt of run 43498592499 on 034f215, which records the inputs digest and the axioms (PROOF-POLICY 8.5.1, standards d9b03a3)")
       (receipt :run "local run, 2026-11-09"
                :commit "f68b78d6ceb8d3c83f96f5ab8e57779442a8834f"
                :checker "agda 2.6.3 (Ubuntu 24.04 agda package)"
@@ -37,11 +63,22 @@
                :state superseded
                :reason "replaced by the CI receipt in the pinned Guix, Agda 2.7.0.1"))
     (leg :prover rocq :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "coqc 8.18.0 (Guix 8edb9da)"
+               :invocation "coqc FeatureReachability.v"
+               :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260")
+                 (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1")))
       (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/42896264290/job/130110238086"
                :commit "336768958d01257caae14cb81fb54197c2617d97"
                :checker "coqc 8.18.0 (Guix 8edb9da)"
                :invocation "coqc FeatureReachability.v"
-               :state current)
+               :state superseded
+               :reason "replaced by the CI receipt of run 43498592499 on 034f215, which records the inputs digest and the axioms (PROOF-POLICY 8.5.1, standards d9b03a3)")
       (receipt :run "local run, 2026-11-09"
                :commit "f1be654e69b23873ea40651cb40e0e095ac53680"
                :checker "coqc 8.18.0 (Ubuntu 24.04 coq package)"
@@ -49,14 +86,186 @@
                :state superseded
                :reason "replaced by the CI receipt in the pinned Guix"))
     (leg :prover lean :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "lean 4.29.0 (Guix 8edb9da)"
+               :invocation "lean FeatureReachability.lean"
+               :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10")
+                 (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a")
+                 (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2")))
       (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/42896264290/job/130110238086"
                :commit "336768958d01257caae14cb81fb54197c2617d97"
                :checker "lean 4.29.0 (Guix 8edb9da)"
                :invocation "lean FeatureReachability.lean"
-               :state current)
+               :state superseded
+               :reason "replaced by the CI receipt of run 43498592499 on 034f215, which records the inputs digest and the axioms (PROOF-POLICY 8.5.1, standards d9b03a3)")
       (receipt :run "local run, 2026-11-09"
                :commit "f1be654e69b23873ea40651cb40e0e095ac53680"
                :checker "lean 4.15.0 (11651562caae, release archive)"
                :invocation "lean FeatureReachability.lean"
                :state superseded
-               :reason "replaced by the CI receipt in the pinned Guix, Lean 4.29.0"))))
+               :reason "replaced by the CI receipt in the pinned Guix, Lean 4.29.0")))
+  (claim :id "APP-1" :pwg PWG-1 :foundation-diverse #f
+    (leg :prover agda :route source :token proven :state AGDA-VERIFIED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "agda 2.7.0.1 (Guix 8edb9da)"
+               :invocation "agda --safe --without-K --cubical-compatible Applied/Missing.agda"
+               :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12")
+                 (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56")
+                 (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb")
+                 (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959")
+                 (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9")
+                 (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97")
+                 (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564"))))
+    (leg :prover rocq :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "coqc 8.18.0 (Guix 8edb9da)"
+               :invocation "coqc Cohort.v"
+               :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260")
+                 (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1"))))
+    (leg :prover lean :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "lean 4.29.0 (Guix 8edb9da)"
+               :invocation "lean Cohort.lean"
+               :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10")
+                 (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a")
+                 (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2")))))
+  (claim :id "APP-2" :pwg PWG-1 :foundation-diverse #f
+    (leg :prover agda :route source :token proven :state AGDA-VERIFIED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "agda 2.7.0.1 (Guix 8edb9da)"
+               :invocation "agda --safe --without-K --cubical-compatible Applied/IntLaws.agda"
+               :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12")
+                 (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56")
+                 (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb")
+                 (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959")
+                 (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9")
+                 (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97")
+                 (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564"))))
+    (leg :prover rocq :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "coqc 8.18.0 (Guix 8edb9da)"
+               :invocation "coqc Cohort.v"
+               :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260")
+                 (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1"))))
+    (leg :prover lean :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "lean 4.29.0 (Guix 8edb9da)"
+               :invocation "lean Cohort.lean"
+               :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10")
+                 (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a")
+                 (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2")))))
+  (claim :id "APP-3" :pwg PWG-1 :foundation-diverse #f
+    (leg :prover agda :route source :token proven :state AGDA-VERIFIED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "agda 2.7.0.1 (Guix 8edb9da)"
+               :invocation "agda --safe --without-K --cubical-compatible Applied/IntLaws.agda"
+               :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12")
+                 (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56")
+                 (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb")
+                 (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959")
+                 (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9")
+                 (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97")
+                 (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564"))))
+    (leg :prover rocq :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "coqc 8.18.0 (Guix 8edb9da)"
+               :invocation "coqc Cohort.v"
+               :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260")
+                 (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1"))))
+    (leg :prover lean :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "lean 4.29.0 (Guix 8edb9da)"
+               :invocation "lean Cohort.lean"
+               :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10")
+                 (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a")
+                 (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2")))))
+  (claim :id "APP-4" :pwg PWG-1 :foundation-diverse #f
+    (leg :prover agda :route source :token proven :state AGDA-VERIFIED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "agda 2.7.0.1 (Guix 8edb9da)"
+               :invocation "agda --safe --without-K --cubical-compatible Applied/Missing.agda"
+               :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12")
+                 (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56")
+                 (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb")
+                 (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959")
+                 (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9")
+                 (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97")
+                 (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564"))))
+    (leg :prover rocq :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "coqc 8.18.0 (Guix 8edb9da)"
+               :invocation "coqc Cohort.v"
+               :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260")
+                 (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1"))))
+    (leg :prover lean :route re-proved :token proven :state RECONCILED
+      (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520"
+               :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c"
+               :checker "lean 4.29.0 (Guix 8edb9da)"
+               :invocation "lean Cohort.lean"
+               :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1"
+               :state current
+               (axioms)
+               (inputs-manifest
+                 (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10")
+                 (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a")
+                 (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2"))))))