diff --git a/docs/proposals/estate-mathematical-architecture.adoc b/docs/proposals/estate-mathematical-architecture.adoc index daf1f882..c6b7ffa1 100644 --- a/docs/proposals/estate-mathematical-architecture.adoc +++ b/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] diff --git a/docs/standards/AUTHORITY.adoc b/docs/standards/AUTHORITY.adoc index c92e711f..555cfcba 100644 --- a/docs/standards/AUTHORITY.adoc +++ b/docs/standards/AUTHORITY.adoc @@ -7,6 +7,7 @@ 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. @@ -14,7 +15,7 @@ Mathesis is a discovery and proof-orientation system, not a second estate standa == 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. diff --git a/docs/status/CROSS-PROVER-RECONCILIATION.adoc b/docs/status/CROSS-PROVER-RECONCILIATION.adoc index 327e0cde..43a47a34 100644 --- a/docs/status/CROSS-PROVER-RECONCILIATION.adoc +++ b/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"]