[hyperpolymath]

Summary

This brings the echidna proof route into mathesis.

• echidnabot's catalogue row was stale. It came from the 2026-10-26 census, so it pointed at docs/proof-debt.adoc and missed the receipt-boundary theory files added since.
• hypatia was listed under the wrong status document. The census took whichever status document sorted first, so it showed docs/proof-debt.adoc instead of hypatia's CI-checked verification/PROOF-STATUS.adoc.
• This PR adds a dated, source-anchored record of the route's theorems, receipts and derived Proof Witness Grades (PROOF-POLICY §8). It is not a claims registry: the atlas README leaves that design open.

Related: hyperpolymath/echidnabot#195 (theory receipts and CI gate) and metadatastician/standards#1434 (ultraplan v0.2.3; asks D-10, recommending mathesis as the home for the token-lattice theory).

Changes

• scripts/census/build-rows.sh: when a repository has several status documents, prefer PROOF-STATUS, then PROOF-NEEDS, then proof-debt. Within one kind, the first in sort order still wins.
• docs/catalogue/census/catalogue-rows.json: the echidnabot and hypatia rows are rebuilt from a census of those two repositories:
  • census-repo.sh → summarise.sh → build-rows.sh;
  • the two new rows replace the old ones by repository name;
  • no other row changes.
• docs/catalogue/catalogue.adoc and docs/atlas/generated/*: regenerated from the rows, not edited by hand.
• docs/reports/audit/echidna-proof-route-2026-11-09.adoc (new): theory theorems with their home, the §5 token and §2.2 state for each leg, and the derived PWG.
  • Census: 1 at PWG-3, 3 ungraded (planned), out of 4.
  • It also lists the engineering proofs, which are not graded, and the census corrections.
  • It is marked agent-drafted and unreviewed.

RSR Quality Checklist

Required

• Tests pass: render-catalogue.sh | diff against the committed catalogue is empty, and bun scripts/atlas/census-atlas.mjs check prints PASS.
• Linter is clean: ShellCheck passes on build-rows.sh; asciidoctor renders the new report with no warnings.
• No banned language patterns.
• No unsafe, no banned functions.
• SPDX headers present on the new file.
• No secrets.

As Applicable

• Repo deed and ROADMAP: not changed. The record is a dated report, not a change of project state.

Testing

• The two-repo census was run with MATHESIS_DATA in a scratch directory.
• Rows came out as follows:
  • echidnabot: 12 own files (agda 2, lean 4, rocq 3, idris2 3), status docs/PROOF-STATUS.adoc;
  • hypatia: 43 own files, status verification/PROOF-STATUS.adoc.
• After the splice, the catalogue was re-rendered and the render check matches. The atlas was rebuilt over all 239 rows, and check prints PASS.
• Other rows pick up the new status-document rule at the next full census. Running the full census here (476 repositories) was out of scope.

---

Generated by Claude Code

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 21 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

• Source mode: Auto
• Repository: hyperpolymath/mathesis
• Branch: claude/clever-heisenberg-q9qp32
• File: .coderabbit.yaml
• Commit: 318f827
• Layers: Repository YAML
• Review profile: CHILL
• Plan: Advanced
• Run ID: 461996fd-9240-4b61-a764-f425c6215746

Commits

Reviewing files that changed from the base of the PR and between a3dbe73 and 318f827.

Files ignored due to path filters: 4

• docs/atlas/generated/az.adoc is excluded by !**/generated/**
• docs/atlas/generated/classes.adoc is excluded by !**/generated/**
• docs/atlas/generated/index.json is excluded by !**/generated/**
• docs/atlas/generated/organisations.adoc is excluded by !**/generated/**

Files selected for processing: 5

• docs/architecture/REPOSITORY-MAP.adoc
• docs/catalogue/catalogue.adoc
• docs/catalogue/census/catalogue-rows.json
• docs/reports/audit/echidna-proof-route-2026-11-09.adoc
• scripts/census/build-rows.sh

• 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

[hyperpolymath]

Status of the two red checks on this PR

• estate-rules: fixed here. The staleness check failed because docs/architecture/REPOSITORY-MAP.adoc was out of date. applied-systems/ landed on main without the map being regenerated, so main fails this check too (run 42592014015).
  • I ported the regenerated map into this branch.
  • Locally, the determinism test passes under the C, en_US.UTF-8, C.UTF-8 and POSIX locales.
  • The change becomes a no-op once main carries the same regeneration.
• Canon lockstep: not this PR's. It compares the version and sha256 pins in mathesis_chora.deed with the released canon identity. This PR changes neither the deed nor the canon lock. main fails the same step, "Compare this repo's declared pin", in Dogfood Gate run 42592014015.
  • Fixing it means moving the deed's canon pin to the current release.
  • That is a deliberate pin bump, so it belongs in its own change rather than in this census PR.
  • No fix exists yet that I could port.

---

Generated by Claude Code

[sonarqubecloud]

Quality Gate passed

Issues
0 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]

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