proofs: write the receipt under the new PROOF-POLICY 8.5 and add APP-1 to APP-4

.github/workflows/agda-proof-policy.yml

@@ -125,15 +125,18 @@ 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
         if: ${{ !cancelled() && steps.toolchain.outcome == 'success' }}
         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

.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"

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"

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).

docs/atlas/generated/registry.adoc

@@ -5,18 +5,18 @@
 
 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: 0 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 13 `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
 

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`.

docs/status/PROOF-NEEDS.adoc

@@ -42,30 +42,30 @@ 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
 |Cash identity: the closing cash of the last period equals the opening cash
 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
 |The funding gap is sound and least: adding the gap to the opening cash
 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.

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`.

docs/status/ROADMAP.adoc

@@ -220,6 +220,21 @@ 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.
+** Next change: the claim pins of THY-1 and APP-1 to APP-4 (applied shelf, a
+   new `shelf` field), and of secret-types at the commit that holds its
+   manifest receipt (re-anchoring plan WO 5.1).
 
 [[stages]]
 == Stages

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.
 
 |===

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}