feat(atlas): bridge candidates and their generated view; the register becomes a pointer (WO 2.4)

.github/workflows/proven-tests.yml

@@ -80,7 +80,7 @@ jobs:
           MATHESIS_STANDARDS: ${{ runner.temp }}/receipt-reader
         run: |
           bun scripts/registry/claims-registry.mjs check
-          bun test tests/registry/claims-registry.test.mjs
+          bun test tests/registry/
       - name: Install verified Nickel 1.18.0 (K9 L2 semantics)
         run: |
           set -euo pipefail

Justfile

@@ -766,4 +766,4 @@ registry:
 # Fail if the committed registry view is stale (needs MATHESIS_STANDARDS, as above)
 registry-check:
     bun scripts/registry/claims-registry.mjs check
-    bun test tests/registry/claims-registry.test.mjs
+    bun test tests/registry/

docs/atlas/README.adoc

@@ -9,7 +9,7 @@ or reclassifies the source census. Each row names the commit that the census rea
 source. A–Z means repository-name order, not a claim
 that these are all the mathematical concepts relevant to the estate.
 
-The views are the catalogue (split by census class), A–Z repositories, owner/organisation grouping and the claims registry. The separate class view was removed on 2026-11-10 (WO 2.3): it repeated the catalogue with fewer columns. `index.json` is machine-readable. The CLI
+The views are the catalogue (split by census class), A–Z repositories, owner/organisation grouping, the claims registry and the bridge candidates (`generated/bridges.adoc`, from `claims/bridges.jsonl`). The separate class view was removed on 2026-11-10 (WO 2.3): it repeated the catalogue with fewer columns. `index.json` is machine-readable. The CLI
 supports source discovery and a bounded context pack suitable for agents.
 
 Run with Bun: `bun scripts/atlas/census-atlas.mjs build`, `check`,

docs/atlas/claims/bridges.jsonl

@@ -0,0 +1,2 @@
+{"basis":"read","endpoints":[{"name":"MaxPlus rows","repository":"hyperpolymath/choreographic-types","state":"AGDA-PENDING","system":"agda"},{"name":"MaxPlus instance","repository":"hyperpolymath/tropical-types","state":"NOT-INVENTORIED","system":"lean"}],"id":"choreographic-maxplus-tropical","note":"choreographic-types says the rows equal the tropical-types Lean instance; that is not proved, and the Lean side is not audited","proposed_by":"agent","relation":"unassessed","reviewed_by":null,"source":"reconciliation register of 2026-11-09 (choreographic-types row)","stage":"candidate","state":"BRIDGE-PENDING","subject":"The MaxPlus rows of choreographic-types and the MaxPlus instance of tropical-types"}
+{"basis":"read","endpoints":[{"name":"EchoPartialSection.agda","repository":"hyperpolymath/echo-types","state":"AGDA-VERIFIED","system":"agda"},{"name":"formal/Recovery.v","repository":"hyperpolymath/verisimdb","state":"COQ-CHECKED","system":"rocq"}],"id":"squeakwell-r3-r9-merge-laws","note":"the register read the relation as a refinement: Agda states the laws pointwise, Rocq as function equalities under funext (functional_extensionality_dep whitelisted); no checked translation. The Agda state comes from a local run of 2026-11-09 (Agda 2.7.0.1), not from a home receipt","proposed_by":"agent","relation":"unassessed","reviewed_by":null,"source":"hyperpolymath/squeakwell PROOF-STATUS.adoc, read for the reconciliation register of 2026-11-09","stage":"candidate","state":"BRIDGE-PENDING","subject":"squeakwell recovery ladder R3 and R9: guarded fill inflationary and not monotone; resolve-parametric merge commutative, associative and idempotent"}

docs/atlas/generated/bridges.adoc

@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// GENERATED by scripts/registry/claims-registry.mjs from docs/atlas/claims/bridges.jsonl;
+// do not hand-edit.
+= Bridges
+
+A bridge relates two artefacts in two repositories (PROOF-POLICY §2.2). Each
+row below is a *candidate*: Mathesis has read that the relation may hold, and
+nothing more. A candidate is not evidence, and it gives no grade. Its relation
+stays `unassessed` until a person reviews a comparison that a home repository
+holds. The full record, with the commit, path and blob digest at each end, comes
+with re-anchoring plan WO 5.2.
+
+Candidates: 2.
+
+[cols="2,4,4,1,1,3",options="header"]
+|===
+|Bridge |Subject |Endpoints (§2.2 state) |Relation |State |Source; note
+
+|`choreographic-maxplus-tropical` |The MaxPlus rows of choreographic-types and the MaxPlus instance of tropical-types |https://github.com/hyperpolymath/choreographic-types[hyperpolymath/choreographic-types] agda `MaxPlus rows` (AGDA-PENDING) +
+https://github.com/hyperpolymath/tropical-types[hyperpolymath/tropical-types] lean `MaxPlus instance` (NOT-INVENTORIED) |`unassessed` |`BRIDGE-PENDING` |reconciliation register of 2026-11-09 (choreographic-types row); choreographic-types says the rows equal the tropical-types Lean instance; that is not proved, and the Lean side is not audited
+
+|`squeakwell-r3-r9-merge-laws` |squeakwell recovery ladder R3 and R9: guarded fill inflationary and not monotone; resolve-parametric merge commutative, associative and idempotent |https://github.com/hyperpolymath/echo-types[hyperpolymath/echo-types] agda `EchoPartialSection.agda` (AGDA-VERIFIED) +
+https://github.com/hyperpolymath/verisimdb[hyperpolymath/verisimdb] rocq `formal/Recovery.v` (COQ-CHECKED) |`unassessed` |`BRIDGE-PENDING` |hyperpolymath/squeakwell PROOF-STATUS.adoc, read for the reconciliation register of 2026-11-09; the register read the relation as a refinement: Agda states the laws pointwise, Rocq as function equalities under funext (functional_extensionality_dep whitelisted); no checked translation. The Agda state comes from a local run of 2026-11-09 (Agda 2.7.0.1), not from a home receipt
+
+|===

docs/reports/audit/echidna-proof-route-2026-11-09.adoc

@@ -13,6 +13,14 @@ 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.
 
+NOTE: 2026-11-10 (re-anchoring plan WO 2.4): the grades below are an agent's
+reading of the receipts on 2026-11-09. No machine derived them. The canon
+reader of PROOF-POLICY §8.5.1 is now the only source of a grade in Mathesis,
+and the claims registry
+(link:../../atlas/generated/registry.adoc[`docs/atlas/generated/registry.adoc`])
+pins no echidna claim yet. Read these grades as history, not as a current
+record.
+
 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).