hyperpolymath · Nov 10, 2026 · Nov 9, 2026 · Nov 10, 2026
@@ -80,4 +80,4 @@ jobs:
       - name: Emit the receipt for this commit
         run: |
           bash scripts/grade-receipt.sh --write --commit "$(git rev-parse --short=12 HEAD)"
-          sed -n '1,80p' verification/receipts/agda-grade3_praxis.deed
+          sed -n '1,80p' verification/receipts/agda_praxis.deed
@@ -10,6 +10,23 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 ==== Fixed
 
+* **The canonical Agda invocation is in force, and grades follow PROOF-POLICY §8.**
+** `--cubical-compatible` (PROOF-POLICY §2.1) is in `scripts/proof-flags.sh`, so
+   the gate, the laws certificate and the receipt all run under
+   `--safe --without-K --cubical-compatible`. The thirteen
+   `just`-injectivity clauses in `Noninterference.Generic` read the run's result
+   through `Prelude.just-inj`, defined by `cong`, not by matching. No statement,
+   semantics or fixture changed. Waiver W-1 is closed.
+** `tests/flag-control/IndexedMatch.agda` proves the flag is in force:
+   `scripts/check.sh` fails if that fixture is ever accepted.
+** "mathesis Grade 3" was the unratified brief's wording; the theorems are now
+   recorded as `PWG-3` with the §8.5 fields (`pwg`, `foundation-diverse`, and
+   each leg's route, token and §2.2 state). The receipt moved from
+   `agda-grade3_praxis.deed` to `agda_praxis.deed`, because a grade is derived
+   and can change, and pins the `PROOF-POLICY` commit it reads.
+** `docs/EXPLAINME.adoc` listed `--cubical-compatible` among the checker flags
+   while the flag was waived; that line is now true.
+
 * **Mint machinery synced to rsr-template-repo 2be7b88.** estate-rules was red:
   the inherited `tests/e2e/use_template_mint_test.sh` (template c481073)
   re-minted this already-minted tree and failed on an unfilled token. The

@@ -1,45 +1,48 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = secret-types — Proof Status
-:revdate: 2026-11-01
+:revdate: 2026-11-09
 
-Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN, with the closed ledger
-tokens of `standards/docs/README-EXPLAINME-STANDARD.adoc` §5 in
+Statuses are the closed vocabulary of `standards/3-practice/PROOF-POLICY.adoc`
+§5 (PROVEN / PROVEN-WITH-AXIOMS / TESTED / ASSUMED / OPEN), with the matching
+ledger tokens of `standards/docs/README-EXPLAINME-STANDARD.adoc` §5 in
 link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger]. Every PROVEN line names
-its module. All modules are `--safe --without-K --no-libraries`, checked with
-`--double-check` and `-W error` by
-`scripts/check.sh`, no postulates. The flag set and the Agda pin live in exactly
-one place, `scripts/proof-flags.sh`, so this file, the gate and the receipt
-cannot disagree. CI: TESTED. `.github/workflows/proofs.yml` (Debian 13,
-`agda-bin=2.6.4.3-1+b2`) ran both gates green on f149e08, run
-https://github.com/hyperpolymath/secret-types/actions/runs/39289501788[39289501788],
-whose log ends `PASS: minimal-laws certificate (3 laws, each needed)`.
-
-== Grade, and the independent-witness legs
-
-This repository reports **mathesis Grade 3** and no higher. The grade is not a
-claim we invented: it is the estate's own record vocabulary
-(`mathesis/estate-mathematical-architecture` §5), and Grade 3 is precisely
-"type-checks locally in Agda under strict flags, not translated to an independent
-foundational system".
-
-[cols="1,2,2",options="header"]
+its module. Every module is checked by `scripts/check.sh` under the §2.1
+canonical invocation, `agda --safe --without-K --cubical-compatible`, and four
+stricter flags (`--no-libraries --ignore-interfaces --double-check -W error`),
+with no postulates. The flag set and the Agda pin live in exactly one place,
+`scripts/proof-flags.sh`, so this file, the gate and the receipt cannot
+disagree, and a flag-control fixture proves the flag is really in force.
+
+== Proof Witness Grades, and the independent-witness legs
+
+Grades here are the estate's *Proof Witness Grades*, `PROOF-POLICY.adoc` §8
+(owner ruling 2026-11-04): `PWG-3`, `PWG-2i`, `PWG-2ii`, `PWG-1`, lower is
+stronger, `ungraded` below the ladder. They are derived from the receipt, never
+asserted (§8.4). This file previously said "mathesis Grade 3", the unratified
+brief's wording; §8 supersedes it, and its `PWG-3` additionally needs the §2.1
+invocation, which this repository has met since waiver W-1 closed.
+
+[cols="1,1,3",options="header"]
 |===
-| Claim | Grade | Why not higher
+| Claim | PWG | Why not higher
 
-| N-1, N-2, N-3, N-7, N-8, N-9 | *Grade 3* | No Rocq leg and no Lean leg exists. Under
-  `standards/3-practice/PROOF-POLICY.adoc` §2 both are required for Grade 2i/ii,
-  and `transported`/`re-proved` is the only vocabulary either leg may use.
+| N-1, N-2, N-3, N-7, N-8, N-9 | `PWG-3` | The Agda proof is PROVEN under the §2.1
+  invocation (receipt below). No Rocq leg and no Lean leg exists, so no leg
+  counts (§8.2). No axioms: `--safe`, a postulate scan of the import cone, and the
+  recorded cone. `foundation-diverse`: no.
 
-| N-4, N-5, N-6 | below Grade 3 (`tested-only`) | They are checked demonstrations —
-  refusals, computed witnesses, a shell-orchestrated law-ablation certificate —
-  not theorems. Mathesis grades theorems; recording these as Grade 3 would grade
-  the wrong object.
-
-| Termination-sensitive noninterference under the current typing rules | REFUTED | N-9
-  formalizes the N-5 counterexample when finishing versus non-finishing is
-  observable. A stronger typing discipline remains open. Declassification is OPEN.
+| N-4, N-5, N-6 | `ungraded` | TESTED demonstrations (refusals, computed
+  witnesses, a law-ablation certificate), not theorems; §8.1 grades theory
+  theorems only.
 |===
 
+N-9 is a proved *refutation*: termination-sensitive noninterference is false for
+the current typing rules when finishing versus non-finishing is observable. A
+stronger typing discipline is OPEN, and so is declassification.
+
+A grade is not a discharge (§8.4.1): at `PWG-3` every theorem above still owes
+its Rocq and Lean legs (§2).
+
 === The two legs, recorded honestly
 
 `PROOF-POLICY.adoc` §2 requires every Agda theory proof to be rechecked in Rocq
@@ -52,12 +55,10 @@ would need its own CI receipt.
 |===
 | Claim | Rocq leg | Lean leg | Record
 
-| N-1, N-2, N-3, N-7, N-8 | `unavailable` | `unavailable`
-| No Agda→Dedukti transport has been attempted from this repository (the
-  estate's exchange layer lives in `echidna`, and `PROOF-POLICY` §2.2 names
-  ECHIDNA as a longer-term destination, not a prerequisite), and no hand
-  re-proof has been attempted. Nothing was skipped silently: this is the
-  opening state, stated.
+| N-1, N-2, N-3, N-7, N-8, N-9 | `unavailable` (`OPEN`) | `unavailable` (`OPEN`)
+| No Agda→Dedukti transport and no hand re-proof has been attempted from this
+  repository yet. §2.2 state of each: `AGDA-VERIFIED`. Nothing was skipped
+  silently: this is the opening state, stated.
 
 | all rows | — | —
 | *A leg that does not exist cannot be evidenced by a file that happens to be
@@ -70,69 +71,55 @@ would need its own CI receipt.
   link:docs/reports/audit/consistency-audit-2026-11-01.adoc.
 |===
 
-Should a leg ever be attempted, `PROOF-POLICY` §2.2 fixes the record: exact
+When a leg is attempted, `PROOF-POLICY` §2.2 fixes the record: exact
 proposition, assumptions, universe discipline, source revision, compiler and
 library versions, invocation, observed result, and the bridge or statement
-correspondence — *transported* or *re-proved* — and the local statuses
+correspondence — *transported* or *re-proved* — and the correspondence states
 AGDA-VERIFIED / COQ-CHECKED / LEAN-CHECKED / BRIDGE-PENDING before RECONCILED.
+Only a RECONCILED leg raises the grade.
 
-=== `--cubical-compatible`: met (W-1 retired)
+=== The §2.1 invocation, and how waiver W-1 closed
 
 `PROOF-POLICY` §2.1 (dated 2026-11-01) names
-`agda --safe --without-K --cubical-compatible` as the canonical invocation. The
-gate (`scripts/proof-flags.sh`) now runs exactly that, with four stricter
-options: `--no-libraries --ignore-interfaces --double-check -W error`. Because
-`-W error` makes every `UnsupportedIndexedMatch` warning fatal, the flag is
-checked rather than nominal: a later indexed match fails the gate.
-
-From 2026-11-01 the flag was waived (W-1, link:docs/proof-debt.adoc#waivers[]).
-Every clause that matched on an indexed relation needed constructor injectivity,
-which Cubical Agda does not support. Two re-representations closed it:
-
-* *The order* (2026-11-01). `_⊑_` became a computed predicate
-  (`L ⊑ _ = ⊤`, `H ⊑ L = ⊥`), so the order laws hold by computation.
-* *`just`-injectivity* (2026-11-09). The 13 remaining warnings, in `tini`, `go`,
-  `confine` and `confineW`, came from matching `refl : just s ≡ just t`. The
-  clauses now take the equation as a variable and use `Prelude.just-inj`, which
-  is `cong` of a total projection and never matches on that equation. No theorem
-  statement changed, and the fuel semantics is untouched: the relational
-  big-step semantics that W-1 named as the way out, and its consequence for N-5,
-  are not needed.
-
-The receipt records `cubical-compatible = "met"`.
+`agda --safe --without-K --cubical-compatible` as the canonical invocation. It is
+in force. Adopting it took two rounds:
+
+* *2026-11-01.* Two constructor-injectivity lemmas were removed or re-expressed
+  (`just-inj` deleted, `_≟_` through `pred`), and the two-point order became a
+  computed predicate (`L ⊑ _ = ⊤`, `H ⊑ L = ⊥`), which removed every
+  `L`/`H`-injectivity warning. Thirteen warnings remained, all
+  `just`-injectivity in `Noninterference.Generic`, from matching `refl`
+  against `exec … ≡ just t`. The flag was waived (W-1), on the belief that only
+  a relational big-step semantics could remove them.
+* *2026-11-09.* That belief was wrong, and was measured rather than argued. The
+  thirteen clauses now read the run's result through `Prelude.just-inj`, defined
+  by `cong` through a computing projection, which needs no unification rule. The
+  statements, the semantics and every fixture are unchanged. Conversely, a
+  relational semantics alone would *not* have been enough: a probe proving
+  determinism of `c , s ⇓ t` raised 22 `UnsupportedIndexedMatch` warnings,
+  because inverting two derivations of one command needs injectivity of `Cmd`'s
+  constructors.
+
+The warning is never suppressed. `tests/flag-control/IndexedMatch.agda` is a
+correct proof that only `--cubical-compatible` refuses; `scripts/check.sh` fails
+if it is ever accepted, so dropping the flag cannot pass the gate (tested both
+ways). W-1 is kept, closed, in link:docs/proof-debt.adoc#waivers[`docs/proof-debt.adoc`].
 
 === What the grade is anchored to
 
-`verification/receipts/agda-grade3_praxis.deed`, generated by
-`scripts/grade-receipt.sh` and checked in CI, records the exact source commit,
-the Agda pin and provenance, the flag set, the `sha256` of every module, the
-claim IDs with their ledger tokens and legs, and the trust-base counts
-(`postulates = 0`, `escape-hatches = 0`, `library-dependencies = 0`,
-`axioms-assumed = 0`). A change to a proved statement cannot leave the receipt
-intact; a claim added here cannot leave the receipt intact either, in either
-direction.
+`verification/receipts/agda_praxis.deed`, generated by `scripts/grade-receipt.sh`
+and checked in CI, records the exact source commit, the Agda pin and provenance,
+the flag set, the `PROOF-POLICY` commit it reads (`hyperpolymath/standards`
+`9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5`), the `sha256` of every module (the
+import cone of `SecretTypes.All`), the trust-base counts (`postulates = 0`,
+`escape-hatches = 0`, `library-dependencies = 0`, `axioms-assumed = 0`), and for
+each claim its ledger token, its derived `pwg`, `foundation-diverse`, and each
+leg's route, token and §2.2 state (§8.5). A change to a proved statement cannot
+leave the receipt intact; a claim added here cannot leave the receipt intact
+either, in either direction.
 
 Proof debt, in the four dispositions the trusted-base policy requires, is
 link:docs/proof-debt.adoc[] — all four empty, and enforced rather than asserted.
-Its `#waivers` section is empty of open waivers. It keeps W-1
-(`--cubical-compatible`) as retired, with the evidence for the waiver and the
-re-representations that closed it.
-
-CI: the whole gate, under the flags above with `--cubical-compatible`, is green
-on `b64974c` under the pinned Agda 2.6.4.3, run
-link:https://github.com/hyperpolymath/secret-types/actions/runs/42633550884[42633550884].
-The gate covers the core proofs, the expected rejections, the laws certificate,
-the receipt drift check and the receipt emit. That run was on the branch of
-hyperpolymath/secret-types#30. A later commit on that branch changed only these
-records and the receipt generator, not the proof sources or the flags. The first
-green `proofs.yml` run on `main` after the merge is the run the receipt rests on.
-
-Earlier run, kept as the evidence for what it showed: run
-link:https://github.com/hyperpolymath/secret-types/actions/runs/41327614303[41327614303]
-on `8e421cc`, under the flags *without* `--cubical-compatible`. It is the
-evidence for the two Agda changes the 2026-11-01 flag attempt forced (`just-inj`
-removed as dead code, `_≟_` re-expressed through `pred`), which is why those
-changes are recorded rather than quietly folded in.
 
 == Fragment (stated before the claims)
 

@@ -38,7 +38,7 @@ worth stating because it was measured on 2026-11-01:
 link:https://github.com/metadatastician/lintel[`metadatastician/lintel`] imports
 `SecretTypes.{Prelude,Vars,Lattice.Record,Lang,Noninterference.Generic}`, defines
 `reader-sets : Lattice`, and opens the generic TINI at it, so the estate does
-have a mechanised consumer of this calculus. It is pinned at `ee01db4`; Lintel's
+have a mechanised consumer of this calculus. It is pinned at `d1d843b`; Lintel's
 own gate was run against this repository's HEAD on 2026-11-01 and passes, so the
 lattice re-representation described in link:docs/proof-debt.adoc#waivers[the
 proof-debt record] is non-breaking for it. Recording a consumer that exists is
@@ -77,16 +77,17 @@ Echo fibre over its outputs does not separate secret inputs — the Echo
 reading of noninterference, and the first candidate connection
 Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`.
 
-*Grade.* The proved claims are **mathesis Grade 3** and no higher: they
-type-check in Agda under the estate's canonical strict flags
-(`scripts/proof-flags.sh`) and have not been translated to an independent
-foundational system. The Rocq and Lean recheck legs that `PROOF-POLICY.adoc` §2
-requires for Grade 2 do not exist; they are recorded `unavailable`, not skipped
-silently. Per-claim evidence is in link:docs/EXPLAINME.adoc#proof-ledger[the Proof
-Ledger], the machine record is
-link:verification/receipts/agda-grade3_praxis.deed[`verification/receipts/agda-grade3_praxis.deed`]
+*Grade.* The proved theorems are at **`PWG-3`** (a Proof Witness Grade,
+`standards/3-practice/PROOF-POLICY.adoc` §8) and no higher: they type-check in
+Agda under the canonical §2.1 invocation, `--safe --without-K
+--cubical-compatible`, plus four stricter flags (`scripts/proof-flags.sh`), with
+no axioms. The Rocq and Lean recheck legs that §2 requires do not exist yet, so
+no leg counts; they are recorded `unavailable`, not skipped silently, and a grade
+is not a discharge. Per-claim evidence is in
+link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger], the machine record is
+link:verification/receipts/agda_praxis.deed[`verification/receipts/agda_praxis.deed`]
 (checked in CI), and link:docs/proof-debt.adoc[proof debt] is empty in all four
-dispositions. This paragraph states no grade the ledger does not support.
+dispositions. This paragraph states no grade the receipt does not support.
 
 == Where things belong
 

@@ -103,10 +103,10 @@ only tested or still open. Tokens are the standard's closed vocabulary.
 | Independent recheck in Rocq and in Lean (PROOF-POLICY §2)
 | open
 | —
-| `PROOF-STATUS.adoc` "Grade and the independent-witness legs",
-  `verification/receipts/agda-grade3_praxis.deed`
+| `PROOF-STATUS.adoc` "Proof Witness Grades, and the independent-witness legs",
+  `verification/receipts/agda_praxis.deed`
 | No transport has been attempted and no hand re-proof exists, so every proven
-  row above is Grade 3 and no higher. The template skeletons under
+  theorem above is `PWG-3` (PROOF-POLICY §8) and no higher. The template skeletons under
   `verification/proofs/{coq,lean4}` are *not* these legs and prove nothing here.
 
 | Strengthened termination-sensitive typing discipline
@@ -123,7 +123,7 @@ only tested or still open. Tokens are the standard's closed vocabulary.
 | The baseline declassifies nothing, by design.
 |===
 
-The machine copy of this ledger is `verification/receipts/agda-grade3_praxis.deed`
+The machine copy of this ledger is `verification/receipts/agda_praxis.deed`
 (generated by `scripts/grade-receipt.sh`; CI fails if it drifts from the tree or
 from the claim IDs in `PROOF-STATUS.adoc`).