[hyperpolymath]

Summary

Work order 2.4 of the re-anchoring plan. The hand-written reconciliation register leaves Mathesis. Owner rulings of 2026-11-10: one bridge file with a stage field, and the single-repository rows point to their home repositories.

Changes

• docs/atlas/claims/bridges.jsonl: one record for each bridge, with stage. The two cross-repository rows of the register are now candidates:
  • squeakwell-r3-r9-merge-laws: echo-types Agda EchoPartialSection.agda and verisimdb Rocq formal/Recovery.v.
  • choreographic-maxplus-tropical: the choreographic-types MaxPlus rows and the tropical-types MaxPlus instance.
  • An unreviewed agent proposal has relation unassessed (plan, "The bridge centre"). The register's reading ("refinement") is kept in the note. A record holds no token and no grade.
• scripts/registry/bridges.mjs: a closed-schema validator (§2.2 states, public repositories, two endpoints in two repositories) and the renderer of docs/atlas/generated/bridges.adoc. claims-registry.mjs builds and checks it with the registry view. The recorded stage (commit, path and blob digest at each end) comes with WO 5.2, and the validator refuses it until then.
• docs/status/CROSS-PROVER-RECONCILIATION.adoc is now a pointer file at the same path, because other repositories cite it: 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 17 home repositories.
• The echidna route audit of 2026-11-09 gets a note: its grades are an agent's reading, not derived.
• Tests: tests/registry/bridges.test.mjs. just registry-check and CI now run all of tests/registry/.

Checks

• "Add a claim pin where a receipt exists": only Mathesis has a receipt that the canon reader accepts. The reader refuses the current secret-types and lintel receipts ("unexpected clause (identity)"), so no new pin.
• "No grade typed by hand": two typed grades remain, both stated here. One is Mathesis's own home record of THY-1 in PROOF-STATUS.adoc, which PROOF-POLICY §8.5 requires. The other is the dated echidna audit report, now annotated.
• just registry-check, atlas-check, catalogue-check, census-test, check-ijson-jcs.sh --enforce docs: pass.
• hyperpolymath/nextgen-typing cites the register's status vocabulary by name only; it does not read the file. The vocabulary is in PROOF-POLICY §2.2.

---

---

Generated by Claude Code

Summary by CodeRabbit

• New Features
  • Added a bridge-candidate view showing proposed cross-repository relationships, their review status, and known limitations. Candidates are clearly distinguished from evidence.
• Documentation
  • Updated reconciliation guidance to point to the canonical proof policy, generated registry views, and repository status documents.
  • Clarified that the audit report’s grades are historical readings, not machine-derived, and that no echidna claim is currently pinned.

[coderabbitai]

Caution

Review failed

The pull request is closed.

Walkthrough

The registry now validates bridge candidates and generates a bridge view alongside the claims registry. Build and check commands include both views. The change adds two candidate records and updates atlas, reconciliation, and audit documentation.

Changes: Bridge registry

Layer / File(s)	Summary
Bridge validation, rendering, and tests scripts/registry/bridges.mjs, tests/registry/bridges.test.mjs	Bridge records are checked for valid fields, endpoints, states, relations, and bases. Valid records are sorted and rendered as an AsciiDoc table. Tests cover validation and rendering behavior.
Registry build and candidate records scripts/registry/claims-registry.mjs, docs/atlas/claims/bridges.jsonl, docs/atlas/README.adoc, .github/workflows/proven-tests.yml, Justfile	Build and check now process the bridge source and generated view with the claims registry. Two candidate records are added, the atlas README lists the view, and both test commands run the full registry test directory.
Reconciliation and audit documentation docs/status/CROSS-PROVER-RECONCILIATION.adoc, docs/reports/audit/echidna-proof-route-2026-11-09.adoc	The reconciliation document points readers to canonical policy, generated views, and repository status documents. The audit report labels its grades historical and states that no echidna claim is pinned in the registry.

Estimated code review effort: 3 (Moderate) | ~20 minutes

Change: Feature

Sequence Diagram(s)

sequenceDiagram
  participant Registry as claims-registry.mjs
  participant Source as bridges.jsonl
  participant Inventory as repository inventory
  participant BridgeCode as bridges.mjs
  participant View as bridges.adoc
  Registry->>Source: read bridge records
  Registry->>Inventory: read repository inventory
  Registry->>BridgeCode: validate records and render view
  BridgeCode-->>Registry: return validated records and AsciiDoc
  Registry->>View: write during build or compare during check

Loading

Possibly related PRs

• hyperpolymath/mathesis#68: Adds grade derivation to the same registry build and check flow that this PR extends for bridge records.
• hyperpolymath/mathesis#22: Adds reconciliation entries to the document that this PR replaces with pointers to canonical sources.
• hyperpolymath/mathesis#10: Establishes reconciliation policy in the document that this PR changes into a pointer document.

Suggested reviewers: claude

Merge Risk: Minimal · up to 2ea06

No actionable merge-blocking issue is established; the generated bridge view matches its source records.

- [ ] Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[sonarqubecloud]

Quality Gate passed

Issues
4 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

[chatgpt-codex-connector]

Codex Review Summary: ❌ Failed

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	❌ Failed 2026-11-11T01:13:54.479084Z We couldn’t complete this review. Comment @codex review to try again.	2ea061e	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.