[hyperpolymath]

Summary

On 2026-11-04 the owner ruled that the brief's §5–§6 grade ladder becomes estate policy, with corrections. It is now PROOF-POLICY §8, Proof Witness Grades (PWG-3, PWG-2i, PWG-2ii, PWG-1), added in metadatastician/standards#1410. This PR makes Mathesis route to §8 instead of the brief, and it settles the five items of this repository's issue 11, plus the Agda axiom-tracking point.

This PR depends on standards#1410: the #proof-witness-grades anchor resolves on standards main only after that PR merges. Merge #1410 first.

Closes #11

Changes

• docs/proposals/estate-mathematical-architecture.adoc gets a supersession note at the head of the brief. The original brief text is untouched, kept as provenance. The note maps each brief grade to its PWG and states each correction:
  • Grade 3: the --safe --without-K --cubical-compatible flags must be recorded. --erasure is not canonical, and full --cubical needs the §2.1 profile. (Item 1.)
  • Grade 2i: a rung is not a discharge, so a 2i theorem still owes the second leg. A leg counts only when it is RECONCILED. (Item 2.)
  • Grade 2ii: this now means both of the policy's legs, Rocq and Lean. A non-DTT witness is the +foundation-diverse tag, not the condition for 2ii.
  • Grade 1: this is claim-gated. It needs pinned, headless receipts per commit, and a regression drops the grade. (Item 5.)
  • Superseded and Regressed: these become a receipt lineage state. The status vocabulary stays closed. (Item 3.)
  • No percentages: grades are published as a census with a denominator. (Item 4.)
  • Name collision: the note flags the clash between PWG and Mathesis's own per-verb coaptation "grades" and the estate's CRG, TRG, ARG and FRG schemes.
• docs/standards/AUTHORITY.adoc routes proof grades to §8. Mathesis derives grades from home-repository receipts and never assigns them. The brief's grade text is marked superseded.
• docs/status/CROSS-PROVER-RECONCILIATION.adoc now says correspondence states and PWG are separate fields. A leg raises the grade only once it is RECONCILED. The revdate is bumped.
• Agda axiom tracking (--safe, a postulate scan, and the import cone) is specified in §8.4 of the policy itself, so the brief needs no edit for it.

RSR Quality Checklist

Required

• Tests pass: docs-only change, with no code touched.
• Code is formatted: not applicable.
• Linter is clean: asciidoctor 2.0.26 -v reports 0 warnings on all three files.
• No banned language patterns
• No unsafe blocks without // SAFETY: comments: not applicable.
• No banned functions
• SPDX license headers present: existing headers kept.
• No secrets, credentials, or .env files included

As Applicable

• Documentation updated for user-facing changes

Testing

Each touched file was rendered with asciidoctor -v, and each gave 0 warnings. I checked the mapping table's superseded\|regressed cell, where the escaped pipe is easy to break: it renders as one cell.

---

Generated by Claude Code

[coderabbitai]

Caution

Review failed

The pull request is closed.

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

Codex Review Summary

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

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-05T00:26:23.479464Z	e87a78b	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.