From 2ea061ef5c69499f175ca544d268dde1cd6ef504 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 11 Nov 2026 01:12:06 +0000 Subject: [PATCH] feat(atlas): bridge candidates and their generated view (WO 2.4) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The hand-written reconciliation register leaves Mathesis (owner rulings 2026-11-10: one bridge file with a stage; the other rows point to their home repositories). - docs/atlas/claims/bridges.jsonl holds every bridge record, with a `stage`. The two cross-repository rows of the register are candidates: the squeakwell R3/R9 merge laws (echo-types Agda, verisimdb Rocq) and the choreographic-types MaxPlus rows (choreographic-types, tropical-types). An unreviewed agent proposal has relation `unassessed`. A record holds no token and no grade. - scripts/registry/bridges.mjs validates the records (closed schema, §2.2 states, public repositories, two endpoints in two repositories) and renders docs/atlas/generated/bridges.adoc; claims-registry.mjs builds and checks it with the registry view. The `recorded` stage comes with WO 5.2. - docs/status/CROSS-PROVER-RECONCILIATION.adoc becomes a pointer file: the policy is PROOF-POLICY §2.1, §2.2 and §8; grades are in the registry; bridges are in the bridge view; the other rows belong to their homes. - No canon-readable receipt exists in the homes of the other rows (the reader refuses the secret-types and lintel receipts), so no new claim pin. - The echidna route audit of 2026-11-09 gets a note: its grades are an agent's reading, not derived. Check: no grade is typed by hand outside Mathesis's own home record of THY-1 (PROOF-POLICY §8.5) and that dated, annotated audit report. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- .github/workflows/proven-tests.yml | 2 +- Justfile | 2 +- docs/atlas/README.adoc | 2 +- docs/atlas/claims/bridges.jsonl | 2 + docs/atlas/generated/bridges.adoc | 25 ++ .../audit/echidna-proof-route-2026-11-09.adoc | 8 + docs/status/CROSS-PROVER-RECONCILIATION.adoc | 274 ++++-------------- scripts/registry/bridges.mjs | 98 +++++++ scripts/registry/claims-registry.mjs | 21 +- tests/registry/bridges.test.mjs | 56 ++++ 10 files changed, 258 insertions(+), 232 deletions(-) create mode 100644 docs/atlas/claims/bridges.jsonl create mode 100644 docs/atlas/generated/bridges.adoc create mode 100644 scripts/registry/bridges.mjs create mode 100644 tests/registry/bridges.test.mjs diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index 1e9b1b9..db5f05e 100644 --- a/.github/workflows/proven-tests.yml +++ b/.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 diff --git a/Justfile b/Justfile index 87dc1bc..9d08c6a 100644 --- a/Justfile +++ b/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/ diff --git a/docs/atlas/README.adoc b/docs/atlas/README.adoc index c0c4f4e..68bd9f5 100644 --- a/docs/atlas/README.adoc +++ b/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`, diff --git a/docs/atlas/claims/bridges.jsonl b/docs/atlas/claims/bridges.jsonl new file mode 100644 index 0000000..3472ac4 --- /dev/null +++ b/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"} diff --git a/docs/atlas/generated/bridges.adoc b/docs/atlas/generated/bridges.adoc new file mode 100644 index 0000000..7773f6e --- /dev/null +++ b/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 + +|=== diff --git a/docs/reports/audit/echidna-proof-route-2026-11-09.adoc b/docs/reports/audit/echidna-proof-route-2026-11-09.adoc index 4ae39e8..0a082ff 100644 --- a/docs/reports/audit/echidna-proof-route-2026-11-09.adoc +++ b/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). diff --git a/docs/status/CROSS-PROVER-RECONCILIATION.adoc b/docs/status/CROSS-PROVER-RECONCILIATION.adoc index 9fe0156..46593f0 100644 --- a/docs/status/CROSS-PROVER-RECONCILIATION.adoc +++ b/docs/status/CROSS-PROVER-RECONCILIATION.adoc @@ -1,223 +1,53 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= Cross-prover proof reconciliation — working policy -:revdate: 2026-11-09 -:toc: -:sectnums: - -== Scope and authority - -This is a *research and verification policy*, not a claim that proofs across -languages have already been reconciled. Mathesis indexes proof evidence and -relationships; it does not become the authoritative proof kernel for its -independent source repositories. ECHIDNA is the intended longer-term -reconciliation automation, not an already complete cross-prover translator. - -Maintain a source theorem's statement, premises, universe/type discipline, -prover version, module, revision and proof assumptions before porting it. -Preserve existing Idris2, Coq and Lean gates during migration. If a proof -cannot be translated faithfully, create an independent Agda proof of an -explicitly compared statement. An Agda proof of a *weaker* proposition never -silently replaces the original theorem. - -== Canonical Agda gate - -Use the documented Agda CLI spelling, with capital K: - -[source,shell] ----- -agda --safe --without-K --cubical-compatible ----- - -Agda's manual specifies `--without-K`; `--cubical-compatible` implies -it but does **not** activate full `--cubical` support. This policy -requires all three flags explicitly at checked entrypoints and CI. -File-level OPTIONS pragmas may reinforce but not replace the command. -Pin/record a compatible Agda and standard-library pair for each corpus. -Imported libraries must satisfy the applicable safe / without-K / -cubical-compatible compatibility requirements. Do not bypass a failing -import with `--allow-unsolved-metas`, `--type-in-type`, `postulate` -or unsafe compiler switches. - -A module dependent on genuinely full Cubical Agda must be recorded -as an explicit proof-profile exception for review; do not claim it -passed the default profile. A failed migration remains *unreconciled*, -rather than being hidden, skipped or relabelled `PROVEN`. - -In this repo `scripts/check-proofs.sh agda` is the manifest-coverage -hard gate; `just proof-check-agda` invokes it. Its command is the -canonical source for local and CI checks. - -== Independent Coq and Lean inspection - -Coq and Lean independently check statements or explicitly specified -witness translations where there is a trustworthy conversion. Neither -kernel automatically verifies arbitrary Agda terms, and equal theorem -names do not establish semantic agreement. - -For every claimed cross-prover correspondence, record: - -* a stable theorem identifier and owning repository; -* the exact *proposition and premises* in each prover (including any - translation of equality, quotients, guardedness, universe levels, - modalities, partiality and effects); -* the revision, prover version, library dependencies, build command - and observed CI/runner result for each; -* whether the relation is `same-statement`, `refinement`, - `conditional-transport`, `countermodel` or `unassessed`; -* the *bridge justification* (theorem, checked translation or - explicit semantic comparison) plus any unproved side conditions; -* whether the result is model-level only, runtime-refined or - externally warranted. A type-checked proof is not independent - evidence about physical reality. - -The strongest possible status requires both a justified correspondence -and independently verified targets; two successful local builds alone -do not satisfy it. - -== Status vocabulary (never collapse) - -[cols="2,4",options="header"] -|=== -|Status |Meaning -|NOT-INVENTORIED |The theorem and exact statement have not been recovered -|INVENTORIED |Original claim, source and dependencies located, without fresh compilation evidence -|AGDA-PENDING |Translation/reproof proposed; full Agda command has not succeeded -|AGDA-VERIFIED |Exact Agda artefact checked with the policy flags at a recorded revision -|COQ-CHECKED |Corresponding Coq module checked, but cross-prover equivalence NOT implied -|LEAN-CHECKED |Corresponding Lean module checked, but cross-prover equivalence NOT implied -|BRIDGE-PENDING |Both sides may compile, but proposition correspondence or side conditions are unproved -|RECONCILED |All stated targets checked and the declared correspondence obligation discharged -|COUNTEREXAMPLE |A soundly evidenced mismatch, inconsistency or refuting instance -|QUARANTINED |Known failure kept visible with issue, reason and a recheck path -|=== - -A proof can have multiple statuses: a successful independent proof is -not inherently a verified Agda–Lean–Coq bridge. Use separate fields -when publishing a machine-readable register. - -These statuses are *correspondence states*. A theorem's *Proof Witness -Grade* (`PWG-3`, `PWG-2i`, `PWG-2ii`, `PWG-1`) is a separate field, derived -from these states and the kernel receipts. Its rules are in -https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc#proof-witness-grades[PROOF-POLICY §8]. -A recheck leg raises the grade only once it is `RECONCILED`. A -`COQ-CHECKED`, `LEAN-CHECKED` or `BRIDGE-PENDING` leg does not raise it. -Never write a grade into a status field, and never write a status into the -grade field. - -== Source-anchored first reconciliation targets - -[cols="2,3,3",options="header"] -|=== -|Owner |Already checked in reconnaissance |Next task, not an established result -|VCL-UT |The current proof corpus is Idris2; VCL-UT has distinct safety, transition and epistemic obligations |Inventory exact Idris propositions and port/reprove the smallest soundness lemma before any claim of 3-prover agreement -|Kategoria |The alpha route includes Idris2 parametric polymorphism demos; multiple type mechanisms are independently scoped |Choose the concrete theorem and theory; do not translate a feature checklist into a purported theorem -|nextgen-typing / Echo |Agda `Verification.agda` imports Echo; historical modules use `--safe --without-K` |Recheck compatible Echo and stdlib under all three policy flags; record mismatches -|trope-checker / invariant-path |Graded-loss algebra and evidence/sortal distinctions carry independent open obligations |Compare exact theorem claims, not an assumed type–trope identity or triangulation -|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 -automatic proof of compliance with the new mode. Do not make all -repos depend on Mathesis or ECHIDNA to build their local proofs. - -== Graduation / rollout - -. Update direct Agda entrypoints and CI commands *in each owning repo*. -. Recheck first-party modules and all imported dependencies under the - new invocation. Record errors without weakening the gate. -. Inventory a theorem and obtain a full-mode Agda receipt. -. Reprove or inspect the corresponding proposition in Lean and Coq. -. Prove/validate the bridge (or label it `BRIDGE-PENDING`). -. Add the receipt and unresolved proof assumptions to the registry. -. Only later automate the reconciliation with ECHIDNA. - -The central register below is currently a *todo list*: **no new -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 -https://github.com/hyperpolymath/squeakwell[squeakwell] `PROOF-STATUS.adoc` -(which holds the per-rung receipts: Coq 8.18.0, Agda 2.7.0.1 with pinned -libraries, Lean 4.35.0). Statuses below are *correspondence states*; the Agda -and Coq legs were checked in one local session and the owning repositories' -CI must confirm them on merge (verisimdb#350, tropical-types#67, the echo-types -PR). None of these rows is RECONCILED: the Agda↔Rocq relation for the merge -laws is a refinement (pointwise vs. function equality), not same-statement. -The catalogue in `docs/catalogue/` is census-generated from `main` and will -pick up the new files when the census is rerun after those PRs merge; it is -not hand-edited here. - - -[cols="2,2,2,2,3",options="header"] -|=== -|Owner |Candidate |Agda |Coq / Lean |Correspondence -|Mathesis |Properties example |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING -|VCL-UT |L0–L10 / transition corpus |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING -|Kategoria |Selected typed mechanism theorem (TBD) |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING -|ECHIDNA |Meta-checker / dogfood Agda |AGDA-PENDING |Existing separate prover corpora; theorem matches not audited |BRIDGE-PENDING -|nextgen-typing |EchoTyping / Verification |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING -|squeakwell (R3, R9 merge laws) |Partial sections: guarded fill inflationary / not monotone; resolve-parametric merge comm/assoc/idem |AGDA-VERIFIED (echo-types `EchoPartialSection.agda`, Agda 2.7.0.1, pinned stdlib/absolute-zero, 2026-11-09 local run) |COQ-CHECKED (verisimdb `formal/Recovery.v`, Coq 8.18.0; `functional_extensionality_dep` whitelisted) |BRIDGE-PENDING — refinement: Agda states the laws pointwise, Rocq as function equalities under funext; no checked translation yet -|squeakwell (R8 narrowing) |Fibre of a pairing = intersection of fibres; `narrow-shrinks` on `FiberSize-fin` |AGDA-VERIFIED (echo-types `EchoFibreIntersection.agda`, same run) |NOT-INVENTORIED (no Rocq/Lean statement) |n/a — single-prover theorem -|squeakwell (R10 progress / termination) |Lexicographic progress on the (missing-count, conflict-count) pair; nine-round fixpoint; `winner_some`, `conflict_refl` explicit |AGDA-PENDING (not stated; needs the finite octad) |COQ-CHECKED (`Recovery.v`: `step_progress`, `iter_9_fixpoint`) |BRIDGE-PENDING -|squeakwell (R5–R7 tropical) |`weightedResidueMeasure`; hub ceiling under `OneTop` (refuted at MaxPlus); `reachGrade` monotone in matrix and observed set |AGDA-PENDING (not stated) |LEAN-CHECKED (tropical-types `Resource/HubCeiling.lean`, Lean 4.35.0; axioms propext/Quot.sound only) |BRIDGE-PENDING -|januskey |G-1 Reversibility (Loss grade algebra) |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING -|januskey |T-1 `rollback-restores` |AGDA-VERIFIED |COQ-CHECKED, LEAN-CHECKED (both re-proved; Rocq 8.18, Lean 4.35, no Mathlib) |RECONCILED -|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 -and records them in `PROOF-NEEDS.adoc` §Proof Witness Grades and -`docs/theory/PROOF-GRADES.adoc` (leg records per PROOF-POLICY §8.5). Derived -from those records and their receipts, its census is `PWG-2ii` 1 (T-1) and -`PWG-3` 4 (G-1, T-2, T-3, E-1m), of 5; none rests on an axiom. The `PWG-3` -receipt is the `agda-proofs.yml` run on januskey `main`: the first to carry the -import cone and the postulate scan is -https://github.com/hyperpolymath/januskey/actions/runs/42633520061[run 42633520061] -at `05ade7862f7f95d618c53bef73a82e71c1700925` (Agda 2.6.4.3, `--safe ---without-K --cubical-compatible`, `resource-algebra` pinned at -`cf9235c532712a783a404c359a1055f40134794a`). T-1's Rocq and Lean legs were -re-proved by hand, because Agda2Dedukti cannot read Agda 2.6.4.3 modules. -januskey records their statement comparison, and checks them in the same -workflow's "Rocq and Lean recheck legs" job. This register catalogues -januskey's grades and assigns none. - -References: -https://agda.readthedocs.io/en/v2.7.0.1/language/cubical-compatible.html[Agda cubical-compatible]; -https://github.com/hyperpolymath/vcl-ut[owned VCL-UT gate]; -https://github.com/hyperpolymath/kategoria[Kategoria]; -https://github.com/hyperpolymath/echidna[ECHIDNA]. += Cross-prover reconciliation (pointer) +:revdate: 2026-11-10 + +This file was the hand-written reconciliation register of Mathesis. On +2026-11-10 (re-anchoring plan WO 2.4) its parts moved to the places that own +them. The file stays at this path because other repositories cite it. The +last version of the register is in the history of this file. + +== Where each part is now + +The policy:: +The canonical Agda invocation is PROOF-POLICY §2.1. The correspondence +evidence for Lean and Rocq, and the status vocabulary (`NOT-INVENTORIED` to +`QUARANTINED`), are PROOF-POLICY §2.2. Proof Witness Grades are PROOF-POLICY +§8. See +https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[metadatastician/standards `3-practice/PROOF-POLICY.adoc`]. +A correspondence state is not a grade, and a grade is not a correspondence +state. + +Grades:: +Mathesis types no grade by hand. The claims registry derives each grade from +the home repository's receipt with the canon reader of PROOF-POLICY §8.5.1: +link:../atlas/generated/registry.adoc[`docs/atlas/generated/registry.adoc`], +from the pins in `docs/atlas/claims/claims.jsonl`. The Mathesis row of the old +register is now the claim `hyperpolymath/mathesis#THY-1` there. + +Bridges:: +A relation between artefacts in two repositories is a bridge record in +`docs/atlas/claims/bridges.jsonl`, with the generated view +link:../atlas/generated/bridges.adoc[`docs/atlas/generated/bridges.adoc`]. +The two cross-repository rows of the old register are candidates there: the +squeakwell R3 and R9 merge laws (echo-types and verisimdb), and the MaxPlus +rows of choreographic-types (choreographic-types and tropical-types). + +The other rows:: +The other rows were to-do items inside one repository. Each home repository +owns its claims and records their status in its own status document. The +catalogue names that document for each repository +(link:../atlas/generated/catalogue.adoc[`docs/atlas/generated/catalogue.adoc`], +column "Proof-status doc"). On 2026-11-10 the canon reader accepted no +receipt from these repositories, so the registry pins none of their claims. +The homes are: ++ +`hyperpolymath/absolute-zero`, `hyperpolymath/affinescript`, +`hyperpolymath/choreographic-types`, `hyperpolymath/echidna`, +`hyperpolymath/echo-types`, `hyperpolymath/epistemic-types`, +`hyperpolymath/invariant-path`, `hyperpolymath/januskey`, +`hyperpolymath/kategoria`, `hyperpolymath/nextgen-typing`, +`hyperpolymath/occupancy-types`, `hyperpolymath/proof-burrower`, +`hyperpolymath/residual-evidence-types`, `hyperpolymath/secret-types`, +`hyperpolymath/squeakwell` (rungs R5 to R8 and R10), +`hyperpolymath/trope-checker` and `hyperpolymath/vcl-ut`. diff --git a/scripts/registry/bridges.mjs b/scripts/registry/bridges.mjs new file mode 100644 index 0000000..31bad6b --- /dev/null +++ b/scripts/registry/bridges.mjs @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// The bridge records of the atlas (re-anchoring plan, "The bridge centre"). +// +// docs/atlas/claims/bridges.jsonl holds one record for each bridge: a relation +// between two artefacts in two repositories. A record has a `stage`. A +// `candidate` (WO 2.4) carries only what Mathesis has read: the two endpoints +// with their §2.2 states, the relation, the bridge's own §2.2 state, the basis +// and the source. The full record (commit, path and blob digest at each end, +// criterion, what it preserves and forgets) is the `recorded` stage of WO 5.2, +// which this validator does not accept yet. A record holds no token and no +// grade. claims-registry.mjs renders docs/atlas/generated/bridges.adoc. + +const STAGES = new Set(['candidate']); +const SYSTEMS = new Set(['agda', 'rocq', 'lean']); +// PROOF-POLICY §2.2 correspondence states. +const STATES = new Set(['NOT-INVENTORIED', 'INVENTORIED', 'AGDA-PENDING', 'AGDA-VERIFIED', 'COQ-CHECKED', + 'LEAN-CHECKED', 'BRIDGE-PENDING', 'RECONCILED', 'COUNTEREXAMPLE', 'QUARANTINED']); +const RELATIONS = new Set(['same-statement', 'refinement', 'conditional-transport', 'countermodel', 'unassessed']); +const BASES = new Set(['read', 'generated', 'transported', 'proved']); +const FIELDS = new Set(['id', 'stage', 'subject', 'endpoints', 'relation', 'state', 'basis', 'source', 'note', + 'proposed_by', 'reviewed_by']); +const ENDPOINT_FIELDS = new Set(['repository', 'system', 'name', 'state']); + +const text = v => typeof v === 'string' && v.trim() !== ''; + +// Throw unless every record is a well-formed candidate whose repositories are +// public in the census inventory. +export function validateBridges(records, inventory) { + const visibility = new Map(inventory.map(r => [r.full_name, r.visibility])); + const seen = new Set(); + for (const b of records) { + const where = b && text(b.id) ? b.id : JSON.stringify(b); + for (const k of Object.keys(b)) if (!FIELDS.has(k)) throw new Error(`Unknown field ${k} (a bridge holds no token or grade): ${where}`); + if (!/^[a-z0-9]+(-[a-z0-9]+)*$/.test(b.id ?? '')) throw new Error(`id must be lowercase words joined by hyphens: ${where}`); + if (seen.has(b.id)) throw new Error(`Duplicate id: ${b.id}`); + seen.add(b.id); + if (!STAGES.has(b.stage)) throw new Error(`stage ${b.stage} is not accepted; only candidate until WO 5.2: ${where}`); + if (!text(b.subject)) throw new Error(`Missing subject: ${where}`); + if (!Array.isArray(b.endpoints) || b.endpoints.length !== 2) throw new Error(`A bridge has two endpoints: ${where}`); + for (const e of b.endpoints) { + for (const k of Object.keys(e)) if (!ENDPOINT_FIELDS.has(k)) throw new Error(`Unknown endpoint field ${k}: ${where}`); + if (!text(e.repository) || visibility.get(e.repository) !== 'public') throw new Error(`Nonpublic or unlisted repository ${e.repository}: ${where}`); + if (!SYSTEMS.has(e.system)) throw new Error(`Unknown system ${e.system}: ${where}`); + if (!text(e.name)) throw new Error(`Missing endpoint name: ${where}`); + if (!STATES.has(e.state)) throw new Error(`Endpoint state ${e.state} is not a §2.2 state: ${where}`); + } + if (b.endpoints[0].repository === b.endpoints[1].repository) throw new Error(`A bridge crosses repositories: ${where}`); + if (!RELATIONS.has(b.relation)) throw new Error(`Unknown relation ${b.relation}: ${where}`); + if (!STATES.has(b.state)) throw new Error(`Bridge state ${b.state} is not a §2.2 state: ${where}`); + if (!BASES.has(b.basis)) throw new Error(`Unknown basis ${b.basis}: ${where}`); + if (!text(b.source)) throw new Error(`Missing source: ${where}`); + if (b.note !== undefined && !text(b.note)) throw new Error(`An empty note: ${where}`); + if (b.proposed_by !== 'agent' && b.proposed_by !== 'person') throw new Error(`proposed_by is agent or person: ${where}`); + if (b.reviewed_by !== null && !text(b.reviewed_by)) throw new Error(`reviewed_by is null or a name: ${where}`); + // An agent's proposal stays unassessed until a person reviews a comparison + // that a home repository holds. + if (b.proposed_by === 'agent' && b.reviewed_by === null && b.relation !== 'unassessed') { + throw new Error(`An unreviewed agent proposal has relation unassessed: ${where}`); + } + } + return records; +} + +const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '); +const end = e => `https://github.com/${e.repository}[${e.repository}] ${e.system} \`${cell(e.name)}\` (${e.state})`; + +// Render the bridge view as AsciiDoc, ordered by id. +export function renderBridges(records) { + const ordered = [...records].sort((a, b) => (a.id < b.id ? -1 : a.id > b.id ? 1 : 0)); + const out = [ + '// 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: ${records.filter(b => b.stage === 'candidate').length}.`, + '', + '[cols="2,4,4,1,1,3",options="header"]', + '|===', + '|Bridge |Subject |Endpoints (§2.2 state) |Relation |State |Source; note', + '', + ]; + for (const b of ordered) { + const notes = [b.source, b.note].filter(Boolean).map(cell).join('; '); + out.push(`|\`${b.id}\` |${cell(b.subject)} |${b.endpoints.map(end).join(' +\n')} |\`${b.relation}\` |\`${b.state}\` |${notes}`, ''); + } + out.push('|===', ''); + return out.join('\n'); +} diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index 872fa1a..ba75e2f 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -27,11 +27,14 @@ import {createHash} from 'node:crypto'; import {fileURLToPath, pathToFileURL} from 'node:url'; import path from 'node:path'; import {readJsonl} from '../atlas/census-atlas.mjs'; +import {validateBridges, renderBridges} from './bridges.mjs'; const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..'); const claimsFile = path.join(root, 'docs/atlas/claims/claims.jsonl'); const reposFile = path.join(root, 'docs/atlas/census/repos.jsonl'); const viewFile = path.join(root, 'docs/atlas/generated/registry.adoc'); +const bridgesFile = path.join(root, 'docs/atlas/claims/bridges.jsonl'); +const bridgesView = path.join(root, 'docs/atlas/generated/bridges.adoc'); const KINDS = new Set(['theorem', 'demonstration', 'assumption']); const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']); @@ -216,17 +219,21 @@ async function main() { } const i = args.indexOf('--receipts-dir'); const receiptsDir = i >= 0 ? path.resolve(args[i + 1]) : null; - const rows = validate(await readJsonl(claimsFile), await readJsonl(reposFile)); + const inventory = await readJsonl(reposFile); + const rows = validate(await readJsonl(claimsFile), inventory); + const bridges = validateBridges(await readJsonl(bridgesFile), inventory); const derived = await deriveAll(rows, receiptsDir, await loadReader()); - const view = render(derived); + const views = [[viewFile, render(derived)], [bridgesView, renderBridges(bridges)]]; if (cmd === 'build') { await mkdir(path.dirname(viewFile), {recursive: true}); - await writeFile(viewFile, view); - console.log(`WROTE ${path.relative(root, viewFile)} (${rows.length} claims)`); + for (const [file, body] of views) await writeFile(file, body); + console.log(`WROTE ${path.relative(root, viewFile)} (${rows.length} claims) and ${path.relative(root, bridgesView)} (${bridges.length} bridges)`); } else { - const committed = await readFile(viewFile, 'utf8').catch(() => ''); - if (committed !== view) throw new Error(`${path.relative(root, viewFile)} is stale; run: bun scripts/registry/claims-registry.mjs build`); - console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); view matches (${rows.length} claims)`); + for (const [file, body] of views) { + const committed = await readFile(file, 'utf8').catch(() => ''); + if (committed !== body) throw new Error(`${path.relative(root, file)} is stale; run: bun scripts/registry/claims-registry.mjs build`); + } + console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges)`); } } diff --git a/tests/registry/bridges.test.mjs b/tests/registry/bridges.test.mjs new file mode 100644 index 0000000..d2c69bf --- /dev/null +++ b/tests/registry/bridges.test.mjs @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +import {test, expect} from 'bun:test'; +import {readFileSync} from 'node:fs'; +import {validateBridges, renderBridges} from '../../scripts/registry/bridges.mjs'; +import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; + +const read = p => parseJsonl(readFileSync(new URL(p, import.meta.url), 'utf8')); +const records = read('../../docs/atlas/claims/bridges.jsonl'); +const inventory = read('../../docs/atlas/census/repos.jsonl'); + +const inv = [{full_name: 'o/a', visibility: 'public'}, {full_name: 'o/b', visibility: 'public'}, {full_name: 'o/p', visibility: 'private'}]; +const good = {id: 'a-b', stage: 'candidate', subject: 'a subject', relation: 'unassessed', state: 'BRIDGE-PENDING', + basis: 'read', source: 'a source', proposed_by: 'agent', reviewed_by: null, + endpoints: [{repository: 'o/a', system: 'agda', name: 'A.agda', state: 'AGDA-VERIFIED'}, + {repository: 'o/b', system: 'rocq', name: 'B.v', state: 'COQ-CHECKED'}]}; +const ends = (i, e) => good.endpoints.map((x, j) => (j === i ? {...x, ...e} : x)); + +test('the committed bridge records validate against the census inventory', () => { + expect(validateBridges(records, inventory)).toHaveLength(records.length); + expect(records.every(b => b.stage === 'candidate' && b.relation === 'unassessed')).toBe(true); +}); + +test('a bridge holds no token and no grade', () => { + expect(() => validateBridges([{...good, pwg: 'PWG-3'}], inv)).toThrow(/no token or grade/); + expect(() => validateBridges([{...good, token: 'proven'}], inv)).toThrow(/no token or grade/); + expect(() => validateBridges([{...good, endpoints: ends(0, {pwg: 'PWG-1'})}], inv)).toThrow(/Unknown endpoint field/); +}); + +test('validation fails closed', () => { + expect(validateBridges([good], inv)).toHaveLength(1); + expect(() => validateBridges([good, good], inv)).toThrow(/Duplicate/); + expect(() => validateBridges([{...good, stage: 'recorded'}], inv)).toThrow(/only candidate until WO 5.2/); + expect(() => validateBridges([{...good, endpoints: [good.endpoints[0]]}], inv)).toThrow(/two endpoints/); + expect(() => validateBridges([{...good, endpoints: ends(1, {repository: 'o/a'})}], inv)).toThrow(/crosses repositories/); + expect(() => validateBridges([{...good, endpoints: ends(1, {repository: 'o/p'})}], inv)).toThrow(/Nonpublic/); + expect(() => validateBridges([{...good, endpoints: ends(1, {state: 'PWG-3'})}], inv)).toThrow(/§2.2 state/); + expect(() => validateBridges([{...good, state: 'RECONCILED?'}], inv)).toThrow(/§2.2 state/); + expect(() => validateBridges([{...good, relation: 'equivalent'}], inv)).toThrow(/Unknown relation/); + expect(() => validateBridges([{...good, basis: 'vibes'}], inv)).toThrow(/Unknown basis/); + expect(() => validateBridges([{...good, id: 'A B'}], inv)).toThrow(/id must be/); +}); + +test('an unreviewed agent proposal stays unassessed', () => { + expect(() => validateBridges([{...good, relation: 'refinement'}], inv)).toThrow(/unassessed/); + expect(validateBridges([{...good, relation: 'refinement', reviewed_by: 'the owner'}], inv)).toHaveLength(1); +}); + +test('the view is deterministic and says a candidate is not evidence', () => { + const two = [good, {...good, id: 'a-c'}]; + const v = renderBridges(two); + expect(renderBridges([...two].reverse())).toEqual(v); + expect(v).toContain('A candidate is not evidence, and it gives no grade'); + expect(v).toContain('Candidates: 2.'); + expect(v).not.toMatch(/PWG-/); +});