hyperpolymath · Nov 10, 2026 · Nov 10, 2026
@@ -11,7 +11,7 @@ Proofs stay in their home repositories. mathesis points at them. Later it
 will also hold the Agda sources for theory that has no other natural home.
 
 The rules for where a proof *should* live are not here: they are
-https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot for Rust, SPARK for Ada,
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot with Pearlite contracts, and Verus, for Rust; SPARK for Ada;
 Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked
 in Rocq and Lean). The working method is the proof-craft skill.
 

@@ -1210,89 +1210,99 @@ three different practices (<<centre>>).
 
 [appendix]
 [[triage]]
-== Provisional triage of the open pull requests
+== Triage of the open pull requests (ruled 2026-11-10)
 
-The table comes from commit subjects and file lists at 2026-11-10. Each row
-needs a full read of the diff (<<wo-0-1>>). Each pull request conflicts with
-`main`.
+The implementation session read each full diff on 2026-11-10 and put each
+row to the owner, who approved every row (ruling D-6 (a)). Each pull request
+conflicted with `main`. The kept parts land in four landing pull requests from
+one branch: A (scanner fixes, hyperpolymath/mathesis#51), B (one refresh tool,
+#52), C (frame, #53) and D (documents, the pull request that adds this table).
+Each original closes with a pointer to its landing pull request. No other
+branch is written.
 
 [cols="1,4,4",options="header"]
 |===
-|PR |Content that `main` does not have |Provisional disposition
+|PR |What `main` lacked |Ruled disposition
 
 |16
-|An audit report of the ECHIDNA proof route. The record of ruling D-10.
-|Keep both as documents. Drop the row changes.
+|An audit report of the ECHIDNA proof route, with ruling D-10.
+|Report lands in D. Rows and the script change are dropped. Closed.
 
 |17
-|Nothing found. The status-document fix and the canon 2.1.5 pin are on
-`main`.
-|Close as superseded.
+|Only its CI step: `main` did not run the census tests.
+|CI step lands in A. Closed.
 
 |20
-|Template boilerplate matched by blob, first implementation.
-|Choose one of 20 and 26.
+|Template boilerplate by blob, first design, with a test.
+|Test lands in A, adapted to the design of 26. Its refresh script is dropped.
+Closed.
 
 |22
-|Tests for status-document choice. The trope-checker grades, typed into the
-register.
-|Keep the tests. Move the grades to the registry (<<wo-2-4>>).
+|Order-independent status tests, two trope-checker register rows, a prose
+grade census.
+|Tests and rows land in D. The prose grade census is dropped: the registry
+derives grades (<<wo-2-4>>). Closed.
 
 |24
-|A partial refresh that records provenance. A finding: one occupancy proof
-fails under its pinned Lean.
-|Keep the provenance design for <<wo-2-1>>. Keep the finding.
+|Reconnaissance rows for nine repositories and the occupancy finding; a
+second refresh mode and a provenance file.
+|Rows and finding land in D, without its januskey rows (superseded by CI
+rows). The mode and the file are dropped for <<wo-2-1>>. Closed.
 
 |25
-|A fix that keeps rows when the template list is empty.
-|Check `main` for the same fix. Then close or rebase that part.
+|A fix: on `main` an empty template list dropped every row.
+|Fix and test land in A. Closed.
 
 |26
-|Template boilerplate matched by path and blob, second implementation.
-|Choose one of 20 and 26.
+|Template boilerplate by (path, blob), second design.
+|The design lands in A. Closed.
 
 |27
-|A scanner that skips comments and strings. Idris2 signatures without
-clauses, reported as axiom candidates.
-|Keep the scanner changes. Send them to the scanner's source.
+|A scanner that blanks comments and strings; Idris2 signatures without
+clauses as axiom candidates.
+|Lands in A. The change goes to the proof-craft source. Closed.
 
 |31
-|The census sees proofs written in Rust (Creusot, Pearlite, Verus).
-|Keep. PROOF-POLICY §1.2 makes this necessary.
+|The census sees Rust proofs (Creusot, Pearlite, Verus); nested status
+documents rank last.
+|Lands in A. Closed.
 
 |34
-|Verus rules.
-|Fold into 31. Close the remainder.
+|One Verus rule; a proof-burrower register row; the Rust wording; an
+ECHIDNA relabel.
+|Rule in A; row and wording in D. The relabel waits: the receipt it cites is
+not on the `main` of echidna. Closed.
 
 |36
-|25 repositories that the frame lacks. A derived row count.
-|Keep both. Drop the rerun data.
+|A derived row count; the atlas rebuilt with each census.
+|Lands in C. The frame was already on `main`. Closed.
 
 |39
-|The owner's proofs in one fork, with the fork listed.
-|Keep the fork listing. Take the row from the next census.
+|A third-party upstream added to `repos.json` by hand.
+|Closed. `main` lists the fork; a sync of the fork gives the row.
 
 |40
-|A census rerun.
-|Close as superseded by the next single run.
+|Nothing: a census rerun.
+|Closed.
 
 |41
-|A row refresh tool with atomic publication and tests.
-|Choose one refresh tool among `main`, 24, 41 and 42.
+|A public-only check; a repository-map fix; a snapshot step.
+|Check and fix land in B. The snapshot step is dropped: it needs
+`mv --exchange`, which ubuntu-24.04 does not have. Closed.
 
 |42
-|Wording that says the catalogue has no grades.
-|Keep the wording. See 41.
+|A sentence that the catalogue carries no grades.
+|Lands in B. Closed.
 
 |44
-|Ada counted as SPARK only where the code opts in.
-|Keep the scanner change. Drop the row changes.
+|Ada counted as SPARK only where it opts in; the template owns its files.
+|Lands in A. Closed.
 
 |45
-|Nothing found beyond a rerun.
-|Close as superseded.
+|Nothing: status-document order and a rerun.
+|Closed.
 |===
 
 `scripts/census/proof-holes.sh` is a copy of the scanner from the proof-craft
-skill. Pull requests 27, 31, 34 and 44 change the copy. The same change must
-reach the source, or the two will differ.
+skill. Landing change A changes the copy. The same change must reach the
+source, or the two will differ.
@@ -0,0 +1,101 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= The echidna proof route: theorems, receipts and grades (2026-11-09)
+:toc:
+
+This is a dated, source-anchored record of the proofs the echidna proof route
+rests on. It is *not* a claims registry: the atlas README leaves that design
+open. Each theorem lives in its home repository, which owns its statement,
+receipts and status (PROOF-POLICY §2.2, §8.5). This page points at them. The
+Proof Witness Grades (PWG) below are derived from those receipts, not
+assigned here.
+
+An agent drafted this record and the statement comparison it cites. Neither
+has been reviewed by the owner yet, so neither counts as independent
+corroboration.
+
+The plan these rows come from is
+https://github.com/metadatastician/standards/blob/main/docs/ULTRAPLAN-ECHIDNA-PROOF-ROUTE-2026-11-04.adoc[the echidna proof-route ultraplan]
+(ladder rows in brackets; v0.2.4 is metadatastician/standards#1434).
+
+== Theory theorems
+
+Census: 4 theory theorems in this route. `PWG-1`: 0. `PWG-2ii`: 0.
+`PWG-2i`: 0. `PWG-3`: 1. `ungraded`: 3, all planned with no Agda source yet.
+
+[cols="2,2,3,2,3",options="header"]
+|===
+|Theorem |Home |Legs: §5 token, §2.2 state |Derived PWG |Receipts
+
+|Receipt boundary, T-RECEIPT: a warrant token does not give its claim
+without a soundness map; no unconditional reflection exists (feeds rows 4-5)
+|hyperpolymath/echidnabot, `docs/PROOF-STATUS.adoc`
+|Agda `proven`. Lean `proven`, re-proved, `BRIDGE-PENDING`. Rocq `proven`,
+re-proved, `BRIDGE-PENDING`. No axioms in any leg.
+|`PWG-3`. It would become `PWG-2ii` once the drafted statement comparison is
+reviewed and both legs are `RECONCILED`.
+|Agda 2.8.0.2 (§2.1 profile), Lean 4.35.0, Coq 8.18.0, at echidnabot
+`1443adfabb98a9e0daea562bc8dbe764442c14cc`; agent session. The per-commit
+CI job is hyperpolymath/echidnabot#195.
+
+|Token order and weakest-step meet; level monotonicity (row 2)
+|hyperpolymath/mathesis (owner ruling D-10, 2026-11-09); no Agda source yet
+|`open`
+|`ungraded`
+|None
+
+|Retraction never raises a level; name-wise retraction kills exactly its
+dependents (row 7)
+|hyperpolymath/residual-evidence-types (Agda source of `Revision.agda`)
+|`open` for the stated theorem
+|`ungraded`
+|None for this statement. The Idris2 transcription is below.
+
+|Status fold is a join on the token lattice (row 12)
+|hyperpolymath/mathesis (owner ruling D-10, 2026-11-09); no Agda source yet
+|`open`
+|`ungraded`
+|None
+|===
+
+== Engineering proofs (not graded, PROOF-POLICY §8.1)
+
+[cols="2,2,2,3",options="header"]
+|===
+|Proof |Home |Token |Receipt
+
+|`Verdict.idr`: `Sound` only from a confirming prover re-check; level
+"sound" only with a witness
+|hyperpolymath/hypatia, `verification/PROOF-STATUS.adoc`
+|`proven` (Idris2); correspondence with epistemic-types `Warrant.agda` is
+`argued`
+|Idris2 v0.7.0, `verify-proofs.yml` run 42559874988 at
+`c639c465e9bbbd01522f1eae12ac98a071afac13`, with accept and reject fixtures
+
+|`Retraction.idr`: retraction as a thinning; a finding survives through a
+token
+|hyperpolymath/hypatia
+|`proven` (Idris2); correspondence with residual-evidence-types is `argued`.
+It retracts one occurrence by position, while the runtime retracts by name
+(ladder row 7).
+|Same run
+
+|echidnabot GraphQL gate, E-AUTH-SCOPE, E-AUTH-ROLE, E-AUTH-GUARD,
+E-RATE-BOUND (row 15)
+|hyperpolymath/echidnabot, `docs/PROOF-STATUS.adoc`
+|`open` under Creusot/Pearlite and Verus (§1.2)
+|Tests only, which are not proof receipts
+|===
+
+== Census corrections made with this record
+
+* The catalogue rows for echidnabot and hypatia were refreshed from a census
+  of those two repositories on 2026-11-09. echidnabot now shows its Agda,
+  Lean and Rocq theory files.
+* `scripts/census/build-rows.sh` chose whichever status document sorted
+  first, so hypatia was listed under `docs/proof-debt.adoc`. It now prefers
+  a `PROOF-STATUS` file, then `PROOF-NEEDS`, then `proof-debt`, so hypatia's
+  CI-checked `verification/PROOF-STATUS.adoc` is the one shown. Other rows
+  pick up this rule at the next full census.
+* echidnabot's class is still the heuristic `theory`, from its file counts.
+  Most of its proof files are prover fixtures (PROOF-POLICY §3); one
+  theorem is real theory.
@@ -116,6 +116,14 @@ grade field.
 |Mathesis |Manifest-driven per-prover gate and proof inventory; historical Agda manifest only attested `--safe` |Run full-mode check and attach genuine run receipt; only then advance status
 |ECHIDNA |Dogfood Agda corpus and meta-checker CI have separate commands; MetaChecker contains at least one stale 'funext' exception comment |Enforce uniform invocation and audit all imports/assumptions before marking Agda verified
 |januskey |Four theory roots (`Reversibility`, `TransactionAtomicity`, `SingleActiveLog`, `Epistemic`) checked in CI under the canonical flags plus `--no-libraries --ignore-interfaces --double-check`, Agda 2.6.4.3, sibling `resource-algebra` pinned by commit; the gate scans the import cone for postulates and refuses seven expected-rejection fixtures. T-1 is re-proved in core Rocq and Lean with its statement comparison recorded |Recheck the four remaining `PWG-3` rows (G-1, T-2, T-3, E-1m) in Rocq and Lean. The Rust TransactionManager refines the abstract log only by transcription (januskey T-10, OPEN)
+|echo-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible` (stdlib v2.3 `8326c74`, absolute-zero `f486c29`): all five non-cubical entrypoints pass; the `All` cone is 125 local modules with no escape. Recipes pass no `--cubical-compatible`; file pragmas carry it in 131 of 137 files. `EchoImageFactorizationPropCubical` is checked in full Cubical through its pragma. No Rocq or Lean leg |Put the canonical flags in recipes and CI; give the cubical island a reviewed profile; record receipts in the home `PROOF-STATUS` for the eligible theorems (`Echo-comp-iso`, `cancel-iso`, `Echo-comp-pent-Σ-assoc`, `echo↔fib`, `A↔ΣEcho`, `echo-pullback-univ`, `GCLaws`, `no-section-of-collapsing-map`)
+|secret-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible` (builtins only): `SecretTypes.All` passes; 2/2 rejection fixtures refused. Its own `-W error` fails under the canonical flags unless `-W noUnsupportedIndexedMatch` is added. Rocq and Lean files present are RSR template files |Adopt the canonical flags; re-run at the pinned Agda 2.6.4.3; record receipts for N-1, N-2, N-3, N-7, N-8
+|epistemic-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`: all 22 `src` modules and `CanonicalEcho` pass; 13/13 rejection fixtures refused |Re-run at the pinned Agda 2.6.4.3; record receipts; refresh the stale module counts in `PROOF-STATUS`
+|residual-evidence-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`: `All`, both comparisons and `Correspondence` pass; 9/9 rejection fixtures refused |Re-run at the pinned Agda 2.6.4.3; record receipts for the Core, Context and Composition laws
+|choreographic-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`: both roots pass with all `src` modules in cone; 5/5 rejection fixtures refused. The MaxPlus rows are said to equal tropical-types' Lean instance; that is not proved |Re-run at the pinned Agda 2.6.4.3; record receipts; state the MaxPlus correspondence as `BRIDGE-PENDING`
+|occupancy-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible` (resource-algebra `0b338c9`): passes; 2/2 rejection fixtures refused. The Agda check is not called by any workflow, recipe or script. Under its pinned Lean 4.15.0, `StackcertCore.lean` does not compile (type errors in the proof of `cert_sound`) |Wire the Agda check first; move R-6 to TESTED; repair `stackcert` under Lean 4.15.0 or retract the README claim that it compiles
+|absolute-zero |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`, stdlib 1.7.3 (its CI) and 2.3 (what echo-types consumes): the four modules pass. Most CNO lemmas are vacuous; `cno-composition` and OND1–OND5 carry content. The archived Lean uses Mathlib |Grade only `cno-composition` and OND1–OND5; record the stdlib pin; mark the archived Coq and Lean sections as archived
+|affinescript |No Agda source for any theory theorem. Coq 8.18: all 20 `formal/` files build and all 137 assertions are closed under the global context; several hold by definition. Idris2 0.7.0: the Solo core proves progress and preservation. The 23 staged files under `proposals/` pass the canonical flags but are unwired |Owner chooses the Agda home (AffineScript completion plan, question 17); port `QttSemiring` first; compare the Rocq statements and record the bridge. The repo's proof ledger is in `docs/EXPLAINME.adoc`
 |===
 
 Existing proof statuses in these repos are historical evidence, not
@@ -138,6 +146,15 @@ full-mode runs or cross-prover reconciliations were observed during
 this policy edit**. CI must supply the evidence before any result
 is relabelled.
 
+On 2026-11-09 the rows for echo-types, secret-types, epistemic-types,
+residual-evidence-types, choreographic-types, occupancy-types, absolute-zero and
+affinescript were added from local runs (hyperpolymath/mathesis#24, landed
+2026-11-10; its januskey rows are not carried, because the januskey rows above
+come from CI). Those runs are
+reconnaissance: they used Agda 2.6.3, while four of these repositories pin
+2.6.4.3, and they are not receipts recorded in the home repositories. So no
+of those rows moved past `AGDA-PENDING`, and no grade is derived.
+
 == Register format (initially not reconciled)
 
 First populated rows (2026-11-09): the squeakwell recovery ladder, from
@@ -170,6 +187,17 @@ not hand-edited here.
 |januskey |T-2 `lifecycle-preserves-good` |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING
 |januskey |T-3 `at-most-one-active` |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING
 |januskey |E-1m epistemic model (`Epistemic.agda`) |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING
+|echo-types |Composition and fibration headlines (`All` cone) |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
+|secret-types |TINI and countermodels (N-1, N-2, N-3, N-7, N-8) |AGDA-PENDING |NOT-INVENTORIED (template files only) |BRIDGE-PENDING
+|epistemic-types |Ordered-group and Kripke rows |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
+|residual-evidence-types |Core, Context and Composition laws |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING
+|choreographic-types |K, W, T, Y, A, B and E rows |AGDA-PENDING |MaxPlus said to match a tropical-types Lean instance; not audited |BRIDGE-PENDING
+|occupancy-types |R-1, R-3, R-4 |AGDA-PENDING (unwired) |Lean `stackcert` fails to compile at its 4.15.0 pin |BRIDGE-PENDING
+|absolute-zero |`cno-composition`, OND1–OND5 |AGDA-PENDING |Archived; the Lean uses Mathlib |BRIDGE-PENDING
+|affinescript |QTT semiring laws, STLC and records progress and preservation, Solo core |INVENTORIED (no Agda source) |COQ-CHECKED (Coq 8.18, 2026-11-09); Lean none; Solo core in Idris2 |BRIDGE-PENDING
+|trope-checker |Theorem B, Targets 1–4 |AGDA-VERIFIED: `proofs.yml` run 42623339243 at `c0eb4f1`, log `PASS: All.agda + Smoke.agda typecheck (--safe --without-K --cubical-compatible)`, Agda 2.7.0.1 + stdlib v2.0 pinned by SHA-256 |Rocq: none exists (ADR 0005 D5 removed the template). Lean: states no part of Theorem B |BRIDGE-PENDING (no leg to bridge to)
+|trope-checker |O1-carrier atom factorisation, tropical factorisations, grade-algebra boundary |No Agda source states them |LEAN-CHECKED (kernel-accepted; `[propext]` for `GradeR.atom_factorization`). Rocq: none. The whole Lean package imports Mathlib, which PROOF-POLICY §2 forbids for a recheck leg |BRIDGE-PENDING
+|proof-burrower |`Burrow/Trust.agda`, `Burrow/Ledger.agda` (DOM-1, DOM-2) |AGDA-PENDING (a 2026-11-09 re-check passed under the policy flags; no receipt is committed in that repository and no CI job runs it) |NOT-INVENTORIED |BRIDGE-PENDING
 |===
 
 The januskey rows are evidence-backed, not a todo. januskey owns these theorems