docs: route proof grades to PROOF-POLICY §8 (Proof Witness Grades)

docs/proposals/estate-mathematical-architecture.adoc

@@ -5,6 +5,63 @@ Status: *unratified architectural brief*. Preserved from the former Mathesis roo
 
 The controlling estate proof policy lives at https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]. Mathesis's live census and first atlas slice are described in link:../../README.adoc[the README] and link:../atlas/README.adoc[the atlas README]. In particular, any conflicting grade definitions, tool flags, integration claims, or proposed storage arrangements below require explicit review, not silent adoption.
 
+[IMPORTANT]
+.§5 grades superseded: Proof Witness Grades (owner ruling 2026-11-04)
+====
+The grade ladder in §5–§6 below was adopted as estate policy, with
+corrections, as *Proof Witness Grades* (PWG) in
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc#proof-witness-grades[PROOF-POLICY §8]
+(standards#1410, which closes mathesis#11). That section governs. The text
+below is kept unedited as provenance. Read it with this map:
+
+[cols="1,1,3",options="header"]
+|===
+|Brief |Policy |What changed
+
+|Grade 3
+|`PWG-3`
+|The flags must be in force *and* recorded under the canonical
+`agda --safe --without-K --cubical-compatible` (PROOF-POLICY §2.1).
+`--erasure` is not part of it. Full `--cubical` needs the separately
+reviewed proof profile of §2.1.
+
+|Grade 2i
+|`PWG-2i`
+|One recheck leg (Rocq or Lean) counts. A leg counts only when it is
+kernel-checked *and* its statement correspondence is `RECONCILED` (§2.2),
+whether it was transported or re-proved. A rung is not a discharge: the
+theorem still owes the second leg.
+
+|Grade 2ii
+|`PWG-2ii`
+|Both of the policy's legs, Rocq *and* Lean, count. A non-DTT witness, such
+as Isabelle/HOL, is the separate tag `+foundation-diverse`. It is no
+longer the condition for 2ii, and it never stands in for a leg.
+
+|Grade 1
+|`PWG-1`
+|Claim-gated. It needs a current receipt from a pinned, headless,
+isolated checker for every witness, at the exact source commit. AXLE,
+`isabelle server` and coq-lsp are examples, not requirements. Any
+"verified" or "machine-checked through …" claim needs these receipts, and
+a regression drops the grade.
+
+|§6 `Superseded` / `Regressed`
+|Receipt lineage
+|Recorded on the receipt as `state: superseded\|regressed`, with the
+reason. The status vocabulary stays closed.
+
+|§6 "no percentages"
+|Census rule
+|Grade counts are published with their denominator, with the lower and
+`ungraded` rungs named. Never as a percentage.
+|===
+
+Always write the `PWG-` prefix. Mathesis also uses "grade" for its
+per-verb coaptation grades (`.machine_readable/coaptation/`), and the
+estate uses it for CRG, TRG, ARG and FRG. None of those is a PWG.
+====
+
 == Original working brief (preserved)
 
 [literal]

docs/standards/AUTHORITY.adoc

@@ -7,14 +7,15 @@ Mathesis is a discovery and proof-orientation system, not a second estate standa
 == Authority by responsibility
 
 * *Estate-wide proof and verification policy*: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[metadatastician/standards — PROOF-POLICY]. This owns the permitted trust classes, proof languages, and requirements for proof claims. Follow the standards repo's own versioning and pinned revision when verifying a historical result.
+* *Proof grades*: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc#proof-witness-grades[PROOF-POLICY §8, Proof Witness Grades] (`PWG-3`, `PWG-2i`, `PWG-2ii`, `PWG-1`; owner ruling 2026-11-04). This is the only estate proof grade. Mathesis catalogues grades by *deriving* them from home-repository receipts and §2.2 correspondence records. It never assigns them. A machine-readable mirror is `3-practice/proof-witness-grades.k9.ncl` in the standards repository.
 * *Estate-wide test policy*: https://github.com/metadatastician/standards/tree/main/3-practice/testing-and-benchmarking[testing and benchmarking] and https://github.com/metadatastician/standards/blob/main/3-practice/ZIGZAG-TESTING.adoc[Zigzag testing].
 * *Repository-local mathematical architecture*: link:../atlas/README.adoc[Mathesis atlas], link:../catalogue/catalogue.adoc[existing proof census], and link:../../README.adoc[Mathesis README]. Mathesis may propose proof-index schemas and navigation views; a proposed ranking never becomes estate policy by appearing here.
 * *Individual theorem truth and proof obligations*: the theorem's home repository, its exact source revision and its kernel-check receipts. A census row, index, file count, or interpreted dependency is not a proof.
 * *Implementation assurance*: https://github.com/hyperpolymath/proven-tests-and-benches[proven-tests-and-benches] owns reusable test evidence and fixture doctrine; https://github.com/hyperpolymath/cicd-suite[cicd-suite] owns executable assurance gates. The status of a CI job is not automatically a theorem verification result.
 
 == Distinguish proposals from decisions
 
-The root link:../proposals/estate-mathematical-architecture.adoc[estate-mathematical-architecture] is an *unratified architecture brief*, preserved for provenance. In particular, its proposed proof grades, indexing/storage design, and implementation stages are not replacements for the canonical PROOF-POLICY or for the current census implementation.
+The root link:../proposals/estate-mathematical-architecture.adoc[estate-mathematical-architecture] is an *unratified architecture brief*, preserved for provenance. Its proof-grade ladder (§5–§6) has since been adopted, with corrections, as PROOF-POLICY §8. Cite §8, not the brief: the brief's own grade text is superseded, and a note at its head maps each brief grade to its policy grade. Its indexing/storage design and implementation stages remain unratified, and are not replacements for the canonical PROOF-POLICY or for the current census implementation.
 
 The generic RSR architecture files under `docs/` reflect template lineage and should not be treated as independent Mathesis standards. If local documentation and estate policy disagree, record the conflict, the source revisions, and the required decision; do not silently make either one authoritative.
 

docs/status/CROSS-PROVER-RECONCILIATION.adoc

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = Cross-prover proof reconciliation — working policy
-:revdate: 2026-11-01
+:revdate: 2026-11-05
 :toc:
 :sectnums:
 
@@ -95,6 +95,15 @@ A proof can have multiple statuses: a successful independent proof is
 not inherently a verified Agda–Lean–Coq bridge. Use separate fields
 when publishing a machine-readable register.
 
+These statuses are *correspondence states*. A theorem's *Proof Witness
+Grade* (`PWG-3`, `PWG-2i`, `PWG-2ii`, `PWG-1`) is a separate field, derived
+from these states and the kernel receipts. Its rules are in
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc#proof-witness-grades[PROOF-POLICY §8].
+A recheck leg raises the grade only once it is `RECONCILED`. A
+`COQ-CHECKED`, `LEAN-CHECKED` or `BRIDGE-PENDING` leg does not raise it.
+Never write a grade into a status field, and never write a status into the
+grade field.
+
 == Source-anchored first reconciliation targets
 
 [cols="2,3,3",options="header"]