[hyperpolymath]

Summary

The first content for mathesis, the estate's maths section: a generated catalogue of where proofs live across the hyperpolymath repositories, and the census it is built from.

• catalogue/catalogue.adoc lists the 239 repositories that have proof files of their own once RSR template boilerplate is set aside. Rows are split into theory and engineering, with prover file counts, hole/axiom/unsafe/policy counts from proof-craft's proof-holes.sh, and the repo's proof-status document. The private repositories that could not be read are listed at the end.
• data/ holds the census: repositories, proof files, top-level declarations, hole findings, Agda --safe options and proof-status paths. All JSONL is one sorted-key object per line, plus the summary table.
• scripts/census/ reruns it (run-census.sh, census-repo.sh, summarise.sh, generate-catalogue.sh, plus a copy of proof-holes.sh).
• Justfile gains census, catalogue and catalogue-check (fails when the committed catalogue drifts from the committed data).
• README.adoc replaces the template's placeholder README and explains the census and its limits.

First-pass limits (also in the README)

• 476 repositories listed and 462 cloned; 37 private ones could not be read, including cut-calculus. The listing only returned repositories pushed since 2026-09-15, so older ones may be missing.
• Theory/engineering is a heuristic: more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK files reads as theory. Each row needs confirming against PROOF-POLICY.
• Hole and axiom counts are textual candidates, not kernel verdicts.
• just repo-init has not been run, so other template placeholders remain in the tree, and there is no mathesis_chora.deed yet.

Checks

• just catalogue-check passes locally, and regeneration is deterministic: three runs gave identical output.
• The template's scripts/check-ijson-jcs.sh over data/ was still running when this was pushed. The JSONL is written by jq -cS, which matches JCS for this data (string and integer values only), but CI's verdict is the authority.

---

Generated by Claude Code

[coderabbitai]

Caution

Review failed

The pull request is closed.

Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

🧪 Generate unit tests (beta)

• Commit to this branch
• Create a new PR

• 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

_{Comment @coderabbitai help to get the list of available commands.}

[sonarqubecloud]

Quality Gate passed

Issues
41 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

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

Review	Status	Commit	Review trigger
📝 Code Review	🔄 Running since 2026-10-26T18:17:36.581833Z	55aa899	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.

[hyperpolymath]

Two red checks here come from the repository not having been minted from the template yet (just repo-init has not run). They are not caused by the catalogue:

• openssf-compliance: {{PLACEHOLDER}} tokens remain across the template files (www/.well-known/*, www/policies/*, www/public/index.html, …). The same check is red on main at the template's initial commit.
• Canon lockstep: there is no mathesis_chora.deed, so the repo cannot declare a canon pin. The deed is still the template's rsr-template-repo_chora.deed; repo-init renames it at mint.

Both clear when the repo is minted. That can run non-interactively (RSR_NON_INTERACTIVE=1 with PROJECT_NAME, REPO, OWNER, AUTHOR, AUTHOR_EMAIL). It makes owner-level choices (author, contacts, description), so I've left it for the owner rather than folding it into this PR. I can do it as a separate PR on request.

The other failures on this PR were the catalogue's and are fixed:

• root shape, no-Markdown-in-docs and the V-language ban, in 55aa899;
• the ijson_jcs bench regression, in the latest push.

---

Generated by Claude Code