[hyperpolymath]

Summary

Work order 4.1 of docs/proposals/mathesis-re-anchoring.adoc, the first of stage 4. The theory shelf now has its admission rule, an authored admission record for each home theorem, and a theorem index generated from the same derivation as the claims registry.

Owner rulings, 2026-11-11:

• remove all template example proofs;
• keep the admission records together in one authored file, generated into the index;
• use JSON Lines;
• remove the six template stubs under docs/theory/;
• the append-only ledger of the theory work follows in its own PR.

Changes

• The rule. docs/theory/README.adoc states the admission rule. A theorem enters only when three conditions hold:

  • it is theory by the test of PROOF-POLICY §1;
  • no single system owns it;
  • an estate rule, vocabulary or interface depends on it, and the record names that dependant.

• The record. docs/theory/admissions.jsonl holds THY-1's admission. Its dependant is the --all-features rule in standards docs/UPSTREAM-DEPENDENCY-WATCH.adoc.

• The validator and the index. scripts/registry/theory.mjs validates the admissions against the home theorem pins:

  • closed fields, and no grade;
  • a public dependant;
  • exactly one record per home theorem.

  It renders docs/theory/generated/index.adoc as a third view of the registry. So just check fails on a stale index or on a home theorem with no admission. The grade in the index comes from the canon reader, never from the admission.

• Tests. tests/registry/theory.test.mjs has 3 tests, with 10 negative controls.

• Removed:

  • verification/proofs/idris2/ and tlaplus/;
  • agda/Properties.agda, coq/TypeSafety.v and lean4/ApiTypes.lean, with their manifest lines;
  • the six stub READMEs under docs/theory/.

  The golden-path control now plants its failing proof in FeatureReachability.agda.

• Deed.

  • The (ply) theory entry is rewritten. The writer cannot address one (directory) among its siblings, so the whole clause goes through deed-clause.sh, as in WO 3.2.
  • TLA+ and Zig leave the language list.
  • (variant (paths :removed)) and :diverged record the changes.

• Generated files. CLAUDE.md, the coaptation receipt and the repository map are regenerated.

• Documents. README, EXPLAINME, PROOF-NEEDS, PROOF-STATUS, READINESS and ROADMAP are updated to match.

For you

• The intend contract still marks stage 3 in_progress and stage 4 declared. Correcting it is a contract edit, so it needs your review; it is recorded in the ROADMAP.
• The coaptation band stays amber.
• The one added U+2014 is in the generated marker line of CLAUDE.md. A hand edit would break validate-claude-md.

RSR Quality Checklist

Required

• Tests pass (just check-views; registry tests 17 pass)
• No banned language patterns
• SPDX licence headers on the new files
• No secrets

As Applicable

• docs/status/ROADMAP.adoc updated
• Documentation updated

Testing

Run in this session on main aeb3c8b plus this change:

• just check-views: 0 FAIL lines. just registry-check: "views match (18 claims, 2 bridges, 1 admissions)".
• just validate-claude-md, validate-coapt, validate-state, validate-rsr, validate-repo-map and census-test: pass.
• Canon deed lint and k9 validator: pass. Canon capability check: "scaffold matches declared capabilities".
• AsciiDoc: 174 files render clean. The admissions file is I-JSON/JCS. Root shape and the shape tests: pass.

Not run here: the proof checks, which need Guix and the provers. CI runs them, together with the moved golden-path control.

Screenshots

Not applicable.

---

Generated by Claude Code

[coderabbitai]

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

• Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

• 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
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.