docs(proofs): record the CI receipts of THY-1; it derives PWG-1 (WO 1.4)

docs/status/PROOF-STATUS.adoc

@@ -116,7 +116,11 @@ missing crate as missing from every build.
   claim, a non-terminating definition, and a `reach-mono` that skips the
   monotonicity step.
 * Axioms: none.
-* Receipt state: current. It is a local run; no CI receipt yet.
+* 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`).
 
 |Rocq leg
 |`PROVEN`, route `re-proved`, correspondence `RECONCILED`. Receipt:
@@ -132,7 +136,11 @@ missing crate as missing from every build.
   for `absent_under_all_features`, `reach_mono` and `edge_mono`.
 * Negative controls: a planted false lemma is rejected. A planted
   `Admitted` compiles, and `Print Assumptions` reports it as an axiom.
-* Receipt state: current. It is a local run; no CI lane runs Rocq here.
+* Receipt state: superseded on 2026-11-10 by the CI receipt below.
+* CI receipt (current): Rocq 8.18.0 in the pinned Guix (`8edb9da`), same
+  invocation, at commit `336768958d01`, run 42896264290. The file SHA-256 is
+  unchanged, and `Print Assumptions` reports `absent_under_all_features`
+  closed under the global context.
 
 |Lean leg
 |`PROVEN`, route `re-proved`, correspondence `RECONCILED`. Receipt:
@@ -153,7 +161,10 @@ missing crate as missing from every build.
 * Negative controls: a planted false lemma and a non-terminating
   definition are rejected. A planted `sorry` compiles with a warning, and
   `#print axioms` reports `sorryAx`.
-* Receipt state: current. It is a local run; no CI lane runs Lean here.
+* Receipt state: superseded on 2026-11-10 by the CI receipt below.
+* CI receipt (current): Lean 4.29.0 in the pinned Guix (`8edb9da`), same
+  invocation, at commit `336768958d01`, run 42896264290. The file SHA-256 is
+  unchanged, and no declared theorem depends on an axiom.
 
 |Why neither leg is transported
 |Lambdapi's Rocq and Lean exports translate before elaboration and drop
@@ -208,13 +219,16 @@ Residual assumptions: none in any leg.
 
 |Machine receipt (§8.5.1)
 |`verification/receipts/theory_praxis.deed`. The canon reader
-(`deed_lint.js --proof-receipt-json`) derives `PWG-2ii` from it, the grade
+(`deed_lint.js --proof-receipt-json`) derives `PWG-1` from it, the grade
 below, and CI runs that reader on each change.
 
 |`pwg`
-|`2ii`: the Agda leg checks, and both recheck legs count (kernel-checked
-and `RECONCILED`). It is not `PWG-1`, because no leg has a per-commit CI
-receipt.
+|`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
+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.
 
 |`foundation_diverse`
 |`false`

docs/status/ROADMAP.adoc

@@ -23,18 +23,23 @@ Initial development phase.
   in a dependency graph is monotone under additive features. It backs the
   `--all-features` rule in the standards upstream dependency watch.
   Re-proved in Rocq (`verification/proofs/coq/`) and Lean
-  (`verification/proofs/lean4/`), both `RECONCILED`: `PWG-2ii`, recorded
-  in `docs/status/PROOF-STATUS.adoc`. Transport was not possible because
+  (`verification/proofs/lean4/`), both `RECONCILED`: `PWG-1` since 2026-11-10 (`PWG-2ii` before),
+  recorded in `docs/status/PROOF-STATUS.adoc`. Transport was not possible because
   Lambdapi's Rocq and Lean exports drop rewrite rules.
-* Proof lanes (2026-11-10, re-anchoring plan WO 1.4, ruling D-8 (a)): CI is
-  wired to check Agda, Rocq and Lean inside the pinned Guix shell
+* Proof lanes (2026-11-10, re-anchoring plan WO 1.4, ruling D-8 (a)): CI
+  checks Agda, Rocq and Lean inside the pinned Guix shell
   (`build/channels.scm`, `build/manifest.scm`) on every commit, with no path
   filter, and asserts each version: Agda 2.7.0.1, Rocq 8.18.0, Lean 4.29.0.
   The THY-1 record names Agda 2.6.3 and Lean 4.15.0, so those two receipts
   are earned again at the new versions; Rocq stays at 8.18.0. The first
-  lane runs were still going when this was written; their receipts are
-  recorded only after they pass.
-* Two findings on the way. The `agda-stdlib` 2.3 package of the pinned Guix
+  green run on `main` (run 42896264290, commit `336768958d01`) earned them:
+  each witness passed with an unchanged file digest and a clean axiom
+  report, so the receipt derives `PWG-1`. The toolchain step takes 22 to 35
+  minutes per run, because Guix builds some of its own modules at the pin.
+* Three findings on the way. The Guix `agda` 2.7.0.1 package ships without
+  the interfaces of its primitive modules in a read-only store, so the gate
+  gives Agda a writable copy of its data directory (`Agda_datadir`); that
+  defect belongs to Guix. The `agda-stdlib` 2.3 package of the pinned Guix
   does not build (it fails on the Guix build farm in every build since
   2026-10-18), so `Properties.agda` now uses `Agda.Builtin` only. At the old
   pin `ae77aeb` Guix had no substitute for itself, so the pin moved to

verification/receipts/theory_praxis.deed

@@ -1,41 +1,62 @@
 ;; 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). Every
-;; receipt below is a local run, because no CI lane has given one yet: the run
-;; field says so instead of naming a run that does not exist. The reader in
-;; standards 1-formats/deed/tools/deed_lint.js derives the grade:
+;; 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:
 ;;   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 (2026-11-10).
+;; 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).
 (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 "f1be654e69b23873ea40651cb40e0e095ac53680"
+  :source-commit "336768958d01257caae14cb81fb54197c2617d97"
   (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"))
-  (claim :id "THY-1" :pwg PWG-2ii :foundation-diverse #f
+  (claim :id "THY-1" :pwg PWG-1 :foundation-diverse #f
     (leg :prover agda :route source :token proven :state AGDA-VERIFIED
-      (receipt :run "local run, 2026-11-09; no CI receipt yet"
+      (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)
+      (receipt :run "local run, 2026-11-09"
                :commit "f68b78d6ceb8d3c83f96f5ab8e57779442a8834f"
                :checker "agda 2.6.3 (Ubuntu 24.04 agda package)"
                :invocation "agda --safe --without-K --cubical-compatible FeatureReachability.agda"
-               :state current))
+               :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 "local run, 2026-11-09; no CI lane runs Rocq yet"
+      (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)
+      (receipt :run "local run, 2026-11-09"
                :commit "f1be654e69b23873ea40651cb40e0e095ac53680"
                :checker "coqc 8.18.0 (Ubuntu 24.04 coq package)"
                :invocation "coqc FeatureReachability.v"
-               :state current))
+               :state superseded
+               :reason "replaced by the CI receipt in the pinned Guix"))
     (leg :prover lean :route re-proved :token proven :state RECONCILED
-      (receipt :run "local run, 2026-11-09; no CI lane runs Lean yet"
+      (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)
+      (receipt :run "local run, 2026-11-09"
                :commit "f1be654e69b23873ea40651cb40e0e095ac53680"
                :checker "lean 4.15.0 (11651562caae, release archive)"
                :invocation "lean FeatureReachability.lean"
-               :state current))))
+               :state superseded
+               :reason "replaced by the CI receipt in the pinned Guix, Lean 4.29.0"))))