diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index 116e91a..38a4947 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -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
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 54d9bb1..b45f261 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -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
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 683d307..eb22b47 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -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)
 
diff --git a/README.adoc b/README.adoc
index 5f55227..8caf391 100644
--- a/README.adoc
+++ b/README.adoc
@@ -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
 
diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc
index 41ae5e3..aa4cd95 100644
--- a/docs/EXPLAINME.adoc
+++ b/docs/EXPLAINME.adoc
@@ -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`).
 
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index a3b1c13..e8757a4 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -18,7 +18,7 @@ empty, and that emptiness is *enforced* rather than asserted. `scripts/check.sh`
 refuses the build if any `.agda` file under `src/SecretTypes` or `tests`
 contains `postulate`, and the same tree is compiled with `--safe`, which
 independently refuses `postulate`, `{-# TERMINATING #-}`, `{-# NON_TERMINATING #-}`
-and `--type-in-type`. `verification/receipts/agda-grade3_praxis.deed` records the
+and `--type-in-type`. `verification/receipts/agda_praxis.deed` records the
 counts (`postulates = 0`, `escape-hatches = 0`) *derived from the tree*, and CI
 fails if they move.
 
@@ -67,12 +67,12 @@ _None in the proof development._
 Two items are open *obligations* rather than proof debt, and are listed here so
 that they are not mistaken for either:
 
-* *Grade 2 legs.* `PROOF-POLICY.adoc` §2 asks for every Agda theory proof to be
-  rechecked in Rocq and in Lean. Neither leg exists; both are recorded
+* *Rocq and Lean legs.* `PROOF-POLICY.adoc` §2 asks for every Agda theory proof
+  to be rechecked in Rocq and in Lean. Neither leg exists; both are recorded
   `unavailable` in the receipt and in
   link:../PROOF-STATUS.adoc[`PROOF-STATUS.adoc`]. An absent recheck is not an
-  escape hatch in a proof — the proof has no hole — but it does bound the grade
-  at 3, and that bound is recorded rather than glossed.
+  escape hatch in a proof — the proof has no hole — but it bounds every theorem
+  at `PWG-3` (§8), and that bound is recorded rather than glossed.
 * *Termination-sensitive noninterference.*
   `Noninterference.OutcomeVisibility.termination-sensitive-fails` refutes TSNI
   for the current typing rules when finishing versus non-finishing is public.
@@ -93,22 +93,41 @@ places is a claim the gate does not support.
 [[waivers]]
 == Waivers — obligations this repository does not meet
 
+None open. W-1 below is closed and kept for its evidence.
+
 A waiver is not an escape hatch inside a proof and not proof debt. It is an
 obligation the *policy* sets that this repository does not yet satisfy, recorded
 in the place a reader will look. Each one names the obligation, the tool, and why
 the mapped option was not used (`PROOF-POLICY.adoc` §4 asks for exactly that
 shape when a mapped prover is not the right fit).
 
-=== W-1 `--cubical-compatible` (PROOF-POLICY §2.1, dated 2026-11-01) — RETIRED 2026-11-09
+=== W-1 `--cubical-compatible` (PROOF-POLICY §2.1, dated 2026-11-01) — CLOSED 2026-11-09
+
+*Closed.* The flag is in force in `scripts/proof-flags.sh`, and therefore in the
+gate, the laws certificate and the receipt. The 13 remaining warnings below
+(`just`-injectivity in `Noninterference.Generic`) were removed without arm B2: each
+clause now reads the run's result through `Prelude.just-inj`, defined by `cong`
+through the computing projection `from-just`, which needs no unification rule.
+No statement, semantics or fixture changed. The flag is proved to be in force by
+`tests/flag-control/IndexedMatch.agda`, a correct proof that only the flag
+refuses; `scripts/check.sh` fails if it is ever accepted, and removing the flag
+from `scripts/proof-flags.sh` was tested to fail the gate.
+
+The premise of arm B2 below also turned out to be false. A relational semantics
+does not by itself satisfy the flag: 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. A big-step
+relation is still planned, as a second semantics with an adequacy theorem
+(`exec` finishes iff `⇓` holds), not as a replacement and not for this flag.
+
+The record below is kept as it was written, for provenance.
 
 *Obligation.* `agda --safe --without-K --cubical-compatible <module>` is the
 canonical invocation for first-party Agda theory entrypoints.
 
-*State.* **Met.** Since 2026-11-09 the gate (`scripts/proof-flags.sh`) runs the
-canonical invocation with `--no-libraries --ignore-interfaces --double-check
--W error`, so a new `UnsupportedIndexedMatch` fails the gate rather than being
-waived. The record below is kept as the history of the waiver: what was
-measured, which arm was taken, and what closed it (*Closed*, after the arms).
+*State.* `--safe` and `--without-K` are in the gate. `--cubical-compatible` is
+**not**, and cannot be added without changing the development or weakening the
+check.
 
 *Evidence, from three CI runs on 2026-11-01 that adopted the flag and then had to
 report why it would not stay.* The flag was added, the Agda pin was unchanged
@@ -167,27 +186,13 @@ report why it would not stay.* The flag was added, the Agda pin was unchanged
     derivation, so N-5 would need a new non-derivability argument. It also
     changes the shape of N-1/N-7. That is an owner decision about the statement
     of the theorem, not a refactor to slip into a flag change.
-
-*Closed, 2026-11-09: B2 without the relational semantics.* The 13 warnings did
-not need the change B2 described. Each came from a clause that matched
-`refl : just s ≡ just t`. Those clauses now take the equation as a variable and
-apply `Prelude.just-inj`, defined as `cong (from-just a)` for a total projection
-`from-just`. `cong` matches `refl` only against a variable, so no clause asks
-for the injectivity of `just`. Agreement then follows by `subst`/`subst₂`, or
-from a store equality (`≈-from-≡`). No theorem statement changed, the fuel
-semantics is untouched, and N-5 keeps its `nothing`-returning witness. B2's
-"threading the result as a variable" probe failed because the clauses still
-matched `refl` on two constructor terms inside; the projection is what removes
-that match. With all 13 warnings gone, the flag joined the gate: `SecretTypes.All`
-checks under the canonical invocation with `--double-check -W error`, and the
-receipt records `cubical-compatible = "met"`.
-
-*What would have made the waiver wrong.* Suppressing `-WUnsupportedIndexedMatch`
-in the gate would have made the flag nominally on and the check off. The gate
-never did, and it now keeps `-W error` with the flag on, so the same rule now
-guards the met obligation.
-
-*Consequence for the grade.* None at the time. mathesis Grade 3 was "type-checks
-locally in Agda under strict flags, not translated", so the waiver did not lower
-it. Under PROOF-POLICY §8 the grade is derived from the receipt, which now
-records the §2.1 invocation in full.
+*What would make the waiver wrong.* If `-WUnsupportedIndexedMatch` were ever
+suppressed in the gate, this waiver would become a lie — the flag would be
+nominally on and the check off. The gate does not suppress it, and
+`scripts/proof-flags.sh` is the single place the flags live, so that change
+could not happen by accident.
+
+*Consequence for the grade (as written on 2026-11-01, superseded).* It said the
+grade was unaffected, under the brief's "Grade 3". `PROOF-POLICY` §8 (2026-11-04)
+then required the §2.1 invocation for `PWG-3`, so while W-1 was open the theorems
+were `ungraded`. Closing W-1 is what makes them `PWG-3`.
diff --git a/scripts/check.sh b/scripts/check.sh
index e9c7237..b3f8560 100755
--- a/scripts/check.sh
+++ b/scripts/check.sh
@@ -69,3 +69,21 @@ for file in "${rejects[@]}"; do
   echo "PASS: rejected $name at its invalid declaration"
 done
 echo "PASS: core proofs and all ${#rejects[@]} expected rejections"
+
+# Flag control: the canonical invocation must actually be in force.  The
+# fixture is a correct proof that only --cubical-compatible refuses (it needs
+# constructor injectivity, -WUnsupportedIndexedMatch, fatal under -W error).
+# If the flag were dropped from scripts/proof-flags.sh, the fixture would be
+# accepted and this step would fail.
+control=tests/flag-control/IndexedMatch.agda
+log=_build/check-logs/IndexedMatch.log
+if "$prover" "${flags[@]}" -i tests/flag-control "$control" >"$log" 2>&1; then
+  echo 'ERROR: flag control accepted: --cubical-compatible is not in force' >&2
+  exit 1
+fi
+if ! grep -q 'UnsupportedIndexedMatch' "$log"; then
+  cat "$log"
+  echo 'ERROR: flag control failed for a reason other than --cubical-compatible' >&2
+  exit 1
+fi
+echo 'PASS: flag control (--cubical-compatible is in force: an injectivity match is refused)'
diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh
index 1e114b0..5143d79 100755
--- a/scripts/grade-receipt.sh
+++ b/scripts/grade-receipt.sh
@@ -4,19 +4,21 @@
 #
 # grade-receipt.sh [--check]
 #
-# Writes (or checks) verification/receipts/agda-grade3_praxis.deed: the machine
-# record that this repository's Agda claims are at mathesis Grade 3 and nothing
-# more.
+# Writes (or checks) verification/receipts/agda_praxis.deed: the machine record
+# of this repository's Agda claims, each with its Proof Witness Grade.
 #
-#   Grade 3 (mathesis estate-mathematical-architecture §5): the proof
-#   type-checks locally in Agda under strict flags and has NOT been translated
-#   to an independent foundational system.
+#   Proof Witness Grades: standards/3-practice/PROOF-POLICY.adoc §8 (owner
+#   ruling 2026-11-04).  PWG-3: the Agda proof is PROVEN under the §2.1
+#   invocation and no Rocq or Lean leg counts yet.  The record carries the
+#   §8.5 fields: pwg, foundation-diverse, and for each leg its route, its §5
+#   token and its §2.2 correspondence state.  A grade is derived, never
+#   asserted (§8.4): it is computed below from the legs, not typed in.
 #
 # The receipt is DERIVED from the tree, never typed by hand, except for the
 # claim list below, which is cross-checked against the claim IDs in
 # PROOF-STATUS.adoc in both directions.  That makes two drifts impossible:
 #   * a module added or changed without the receipt following it, and
-#   * a claim added to PROOF-STATUS.adoc without a ledger token and a grade.
+#   * a claim added to PROOF-STATUS.adoc without a ledger token and its legs.
 #
 # What the receipt deliberately does NOT do: it does not run Agda.  It records
 # the gate, the flags and the pinned versions; the gate itself runs in CI
@@ -27,7 +29,7 @@ set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 . scripts/proof-flags.sh
 
-out=verification/receipts/agda-grade3_praxis.deed
+out=verification/receipts/agda_praxis.deed
 mode=
 commit_override=
 while (( $# )); do
@@ -45,36 +47,51 @@ while (( $# )); do
 done
 
 # ── The claim list ────────────────────────────────────────────────────────────
-# id | ledger token (README-EXPLAINME-STANDARD §5 vocabulary) | mathesis grade |
-# Rocq leg (PROOF-POLICY §2) | Lean leg.
+# id | ledger token (README-EXPLAINME-STANDARD §5 vocabulary) | kind |
+# Rocq route | Rocq §2.2 state | Lean route | Lean §2.2 state.
 # Tokens are the closed vocabulary: proven | proven-with-postulates | tested-only
-# | argued | open.  Legs are: transported | re-proved | unavailable.
+# | argued | open.  Kind is theorem (graded, PROOF-POLICY §8.1) or
+# demonstration (a checked example, below the ladder: `ungraded`).  Leg routes
+# are PROOF-POLICY §2 and §8.5: transported | re-proved | waived | unavailable.
+# States are §2.2: AGDA-VERIFIED | COQ-CHECKED | LEAN-CHECKED | BRIDGE-PENDING
+# | RECONCILED | COUNTEREXAMPLE | QUARANTINED.  Only RECONCILED counts (§8.2).
 claims() {
   cat <<'ROWS'
-N-1|proven|grade-3|unavailable|unavailable
-N-2|proven|grade-3|unavailable|unavailable
-N-3|proven|grade-3|unavailable|unavailable
-N-4|tested-only|below-grade-3|n/a|n/a
-N-5|tested-only|below-grade-3|n/a|n/a
-N-6|tested-only|below-grade-3|n/a|n/a
-N-7|proven|grade-3|unavailable|unavailable
-N-8|proven|grade-3|unavailable|unavailable
-N-9|proven|grade-3|unavailable|unavailable
+N-1|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED
+N-2|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED
+N-3|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED
+N-4|tested-only|demonstration|n/a|n/a|n/a|n/a
+N-5|tested-only|demonstration|n/a|n/a|n/a|n/a
+N-6|tested-only|demonstration|n/a|n/a|n/a|n/a
+N-7|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED
+N-8|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED
+N-9|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED
 ROWS
 }
 
+# PROOF-POLICY §8.2: derive the grade from the Agda token and the legs.  A leg
+# counts only when it is RECONCILED (§2.2); none exists yet, so no leg counts.
+# Print the PWG for one claim row's token, kind and two legs' §2.2 states.
+pwg_of() {
+  local token="$1" kind="$2" coq_state="$3" lean_state="$4" counted=0
+  [[ "$kind" == theorem ]] || { printf 'ungraded'; return; }
+  [[ "$token" == proven || "$token" == proven-with-postulates ]] || { printf 'ungraded'; return; }
+  # A leg counts on its §2.2 state, never on its route: a transported or
+  # re-proved leg still BRIDGE-PENDING does not count.
+  [[ "$coq_state" == RECONCILED ]] && counted=$((counted + 1))
+  [[ "$lean_state" == RECONCILED ]] && counted=$((counted + 1))
+  case "$counted" in 0) printf '3' ;; 1) printf '2i' ;; 2) printf '2ii' ;; esac
+}
+
 # ── Derived facts ─────────────────────────────────────────────────────────────
 repo="hyperpolymath/secret-types"
 source_commit="${commit_override:-$(git rev-parse --short=12 HEAD 2>/dev/null || printf 'unknown')}"
 agda_version="$(proof_agda_pin)"
 agda_from="$(proof_agda_provenance)"
 flag_line="$(proof_flags_line)"
-# Conformance is read off the flags the gate actually runs, never written by
-# hand: drop the flag and the receipt says "absent", so --check reports drift.
-case " $flag_line " in
-  *" --cubical-compatible "*) cubical_compatible="met" ;;
-  *)                          cubical_compatible="absent" ;;
-esac
+# The standards commit this receipt reads PROOF-POLICY at (section 7 asks a
+# gate to cite the policy by repository, path and full 40-character commit).
+policy_commit="9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5"
 
 # Print the Agda module paths under src/SecretTypes in sorted order.
 modules() { find src/SecretTypes -name '*.agda' | LC_ALL=C sort; }
@@ -115,8 +132,8 @@ emit() {
   printf ';; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)\n'
   printf ';; GENERATED by scripts/grade-receipt.sh; regenerate with --write, check with --check.\n'
   printf ';; This describes the gate and tree; the CI log is the execution evidence.\n'
-  printf '(praxis-deed\n  :schema-version "1.0.0"\n  :canonical-name "secret-types-agda-grade3-receipt"\n'
-  printf '  (identity\n    :project "secret-types"\n    :name "agda-grade3 verification receipt"\n'
+  printf '(praxis-deed\n  :schema-version "1.0.0"\n  :canonical-name "secret-types-agda-receipt"\n'
+  printf '  (identity\n    :project "secret-types"\n    :name "Agda verification receipt with Proof Witness Grades"\n'
   printf '    :repository "%s"\n    :repo-uuid #u5"github.com/%s"\n' "$repo" "$repo"
   printf '    :uuid-source "uuid5(URL, github.com/%s)"\n' "$repo"
   printf '    :uuid-note "F-1 remains open: template mint-path cause and local scaffolding sweep; see docs/reports/audit/consistency-audit-2026-11-01.adoc"\n'
@@ -126,20 +143,28 @@ emit() {
   printf '    :flags-source "scripts/proof-flags.sh"\n'
   printf '    :flags-note "One definition, read by the gate and by this receipt; the receipt cannot describe a gate that did not run")\n'
   printf '  (conformance\n    :policy "standards/3-practice/PROOF-POLICY.adoc"\n'
-  printf '    :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01"\n'
+  printf '    :policy-repository "hyperpolymath/standards"\n    :policy-commit "%s"\n' "$policy_commit"
+  printf '    :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01; section 8 (PWG) 2026-11-04"\n'
   printf '    :canonical-invocation "agda --safe --without-K --cubical-compatible"\n'
-  printf '    :cubical-compatible "%s"\n    :waiver-history "docs/proof-debt.adoc#waivers (W-1, retired)"\n' "$cubical_compatible"
+  printf '    :cubical-compatible "in-force"\n    :flag-control "tests/flag-control/IndexedMatch.agda"\n'
+  printf '    :closed-waiver "W-1, docs/proof-debt.adoc#waivers"\n'
   printf '    :stronger-than-canonical ("--no-libraries" "--ignore-interfaces" "--double-check" "-W error"))\n'
   printf '  (gate\n    :command "bash scripts/check.sh"\n    :laws-certificate "bash scripts/minimal-laws.sh"\n'
   printf '    :ci ".github/workflows/proofs.yml"\n    :module-count %s\n    :reject-fixture-count %s)\n' "$(modules | wc -l | tr -d ' ')" "$(fixtures | wc -l | tr -d ' ')"
   printf '  (trust-base\n    :postulates %s\n    :escape-hatches %s\n' "$(grep -rlw --include='*.agda' postulate src/SecretTypes tests 2>/dev/null | wc -l | tr -d ' ')" "$(escape_hits | wc -l | tr -d ' ')"
   printf '    :library-dependencies 0\n    :axioms-assumed 0\n'
   printf '    :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero")\n'
-  printf '  ; Grades apply to theorems; refusal fixtures and leak witnesses are below Grade 3.\n'
-  printf '  ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof.\n'
+  printf '  ; PROOF-POLICY section 8: grades apply to theory theorems; demonstrations are ungraded.\n'
+  printf '  ; Rocq and Lean legs are unavailable: no transport or hand re-proof exists yet, so no leg counts.\n'
   printf '  (claims\n'
-  while IFS='|' read -r id token grade coq lean; do
-    printf '    (claim :id "%s" :token "%s" :grade "%s" :coq-leg "%s" :lean-leg "%s")\n' "$id" "$token" "$grade" "$coq" "$lean"
+  while IFS='|' read -r id token kind coq coq_state lean lean_state; do
+    if [[ "$kind" == theorem ]]; then
+      printf '    (claim :id "%s" :token "%s" :kind "%s" :pwg "%s" :foundation-diverse #f\n' "$id" "$token" "$kind" "$(pwg_of "$token" "$kind" "$coq_state" "$lean_state")"
+      printf '      (leg :prover "rocq" :route "%s" :token "open" :state "%s" :receipts ())\n' "$coq" "$coq_state"
+      printf '      (leg :prover "lean" :route "%s" :token "open" :state "%s" :receipts ()))\n' "$lean" "$lean_state"
+    else
+      printf '    (claim :id "%s" :token "%s" :kind "%s" :pwg "%s")\n' "$id" "$token" "$kind" "$(pwg_of "$token" "$kind" "$coq_state" "$lean_state")"
+    fi
   done < <(claims)
   printf '  )\n  ; Every module hash is checked against the current tree.\n  (modules\n'
   while read -r m; do
diff --git a/scripts/proof-flags.sh b/scripts/proof-flags.sh
index e766b66..a0ff8a2 100755
--- a/scripts/proof-flags.sh
+++ b/scripts/proof-flags.sh
@@ -13,22 +13,22 @@
 # Conformance: standards/3-practice/PROOF-POLICY.adoc §2.1 (2026-11-01) sets
 #   agda --safe --without-K --cubical-compatible <module.agda>
 # as the estate default for first-party Agda theory entrypoints.  Every flag
-# below is that default, or strictly stronger:
+# below is that default, or strictly stronger; all three default flags are in
+# force:
 #
 #   --safe               policy default.  No postulates, no --type-in-type,
 #                        no termination pragmas, no unsafe features.
 #   --without-K          policy default.  No UIP, no Streicher K.  (Implied by
 #                        --cubical-compatible; kept explicit so the intent
 #                        survives a future flag change.)
-#   --cubical-compatible policy default.  Waived from 2026-11-01 (W-1) until
-#                        the last indexed matches were re-represented: the
-#                        order is a computed predicate, and `just`-injectivity
-#                        goes through `cong` of a total projection
-#                        (Prelude.just-inj), never a match on
-#                        `refl : just s ≡ just t`.  -W error makes any
-#                        -WUnsupportedIndexedMatch fatal, so a later indexed
-#                        match fails the gate rather than weakening it.
-#                        History: docs/proof-debt.adoc#waivers.
+#   --cubical-compatible policy default.  In force since W-1 closed: the last
+#                        clauses that needed constructor injectivity (matching
+#                        `refl` against `exec … ≡ just t`) now read the result
+#                        through Prelude.just-inj, which matches nothing.  The
+#                        gate does NOT suppress -WUnsupportedIndexedMatch, and
+#                        -W error makes any return of such a clause fatal: a
+#                        planted `refl` match fails the gate (exit 42).
+#                        History: docs/proof-debt.adoc#waivers, W-1 (closed).
 #   --no-libraries       stronger.  Builtins only; no Agda standard library and
 #                        no sibling repository is on the path.  The policy's
 #                        "no Mathlib" rule (PROOF-POLICY §2) is the Lean form of
diff --git a/src/SecretTypes/Noninterference/Generic.agda b/src/SecretTypes/Noninterference/Generic.agda
index b4acc62..69794ef 100644
--- a/src/SecretTypes/Noninterference/Generic.agda
+++ b/src/SecretTypes/Noninterference/Generic.agda
@@ -44,10 +44,6 @@ module _ (V : Observer 𝓛) where
     _≈_ : Store → Store → Set
     s ≈ s' = s ≈[ sees ] s'
 
-    -- Equal stores agree for V.
-    ≈-from-≡ : ∀ {s s'} → s ≡ s' → s ≈ s'
-    ≈-from-≡ refl _ _ = refl
-
     -- Reverse agreement for V, without requiring the stores to be equal.
     ≈-sym : ∀ {s s'} → s ≈ s' → s' ≈ s
     ≈-sym p x v = sym (p x v)
@@ -56,6 +52,19 @@ module _ (V : Observer 𝓛) where
     ≈-trans : ∀ {s s' s''} → s ≈ s' → s' ≈ s'' → s ≈ s''
     ≈-trans p q x v = trans (p x v) (q x v)
 
+    -- Every store agrees with itself.
+    ≈-refl : ∀ {s} → s ≈ s
+    ≈-refl x v = refl
+
+    -- Carry agreement along the results of finishing runs, without
+    -- unifying two just-terms (unsupported under --cubical-compatible).
+    just-≈ : ∀ {u t s} → just u ≡ just t → u ≈ s → t ≈ s
+    just-≈ {s = s} e p = subst (λ w → w ≈ s) (just-inj e) p
+
+    -- The same for two runs at once.
+    just-≈₂ : ∀ {u u' t t'} → just u ≡ just t → just u' ≡ just t' → u ≈ u' → t ≈ t'
+    just-≈₂ {t = t} e e' p = subst (λ w → t ≈ w) (just-inj e') (subst (λ w → w ≈ _) (just-inj e) p)
+
     -- A program counter V cannot see stays unseen in any branch it guards.
     unseen-⊔ : ∀ {pc} y → ¬ sees pc → ¬ sees (pc ⊔ y)
     unseen-⊔ y np v = np (sees-↓ (⊔-upper₁ _ y) v)
@@ -99,8 +108,8 @@ module _ (V : Observer 𝓛) where
   confineL  : ∀ {ℓ e c} fuel {s t} → ¬ sees ℓ → ℓ ⊢ c
             → exec fuel (while e c) s ≡ just t → t ≈ s
 
-  confine fuel np skip e = ≈-from-≡ (sym (just-inj e))
-  confine fuel {s} np (assign {x = x} {e = e} ok) r = subst (λ u → u ≈ s) (just-inj r) (confine-assign x e (eval s e) s np ok)
+  confine fuel {s} np skip e = just-≈ e (≈-refl {s})
+  confine fuel {s} np (assign {x = x} {e = e} ok) j = just-≈ j (confine-assign x e (eval s e) s np ok)
   confine fuel np (seq t₁ t₂) e with bind-just _ _ e
   ... | s₁ , (e₁ , e₂) = ≈-trans (confine fuel np t₂ e₂) (confine fuel np t₁ e₁)
   confine fuel np (ifz {e = g} t₁ t₂) e = confineIf fuel (eval _ g) (unseen-⊔ (lab g) np) t₁ t₂ e
@@ -112,7 +121,7 @@ module _ (V : Observer 𝓛) where
 
   confineW fuel zero np t e with bind-just _ _ e
   ... | s₁ , (e₁ , e₂) = ≈-trans (confineL fuel np t e₂) (confine fuel np t e₁)
-  confineW fuel (suc _) np t e = ≈-from-≡ (sym (just-inj e))
+  confineW fuel (suc _) {s} np t e = just-≈ e (≈-refl {s})
 
   confineL           zero       np t ()
   confineL {e = g} (suc fuel) {s} np t e = confineW fuel (eval s g) np t e
@@ -144,8 +153,8 @@ module _ (V : Observer 𝓛) where
          → (pc ⊔ lab e) ⊢ c → s ≈ s'
          → execWhile fuel (eval s e) e c s ≡ just t → execWhile fuel' (eval s' e) e c s' ≡ just t' → t ≈ t'
 
-  tini fuel fuel' skip eq e e' = subst₂ _≈_ (just-inj e) (just-inj e') eq
-  tini fuel fuel' (assign {x = x} {e = g} ok) eq e e' = subst₂ _≈_ (just-inj e) (just-inj e') (tini-assign x g ok eq)
+  tini fuel fuel' skip eq e e' = just-≈₂ e e' eq
+  tini fuel fuel' (assign {x = x} {e = g} ok) eq e e' = just-≈₂ e e' (tini-assign x g ok eq)
   tini fuel fuel' (seq t₁ t₂) eq e e' with bind-just _ _ e | bind-just _ _ e'
   ... | s₁ , (e₁ , e₂) | s₁' , (e₁' , e₂') = tini fuel fuel' t₂ (tini fuel fuel' t₁ eq e₁ e₁') e₂ e₂'
   tini fuel fuel' (ifz {pc} {g} t₁ t₂) eq e e' =
@@ -174,6 +183,6 @@ module _ (V : Observer 𝓛) where
     go : ∀ n {m} → n ≡ m → execWhile fuel n g c s ≡ just t → execWhile fuel' m g c s' ≡ just t' → t ≈ t'
     go zero    refl e e' with bind-just _ _ e | bind-just _ _ e'
     ... | s₁ , (e₁ , e₂) | s₁' , (e₁' , e₂') = tini fuel fuel' (while tc) (tini fuel fuel' tc eq e₁ e₁') e₂ e₂'
-    go (suc n) refl e e' = subst₂ _≈_ (just-inj e) (just-inj e') eq
+    go (suc n) refl e e' = just-≈₂ e e' eq
   tiniW {pc} {g} fuel fuel' {s} {s'} (no nv) tc eq e e' =
     ≈-trans (confineW fuel (eval s g) nv tc e) (≈-trans eq (≈-sym (confineW fuel' (eval s' g) nv tc e')))
diff --git a/src/SecretTypes/Prelude.agda b/src/SecretTypes/Prelude.agda
index 8ffa3b7..efcd38b 100644
--- a/src/SecretTypes/Prelude.agda
+++ b/src/SecretTypes/Prelude.agda
@@ -34,34 +34,31 @@ cong₂ f refl refl = refl
 -- Transport evidence for the predicate P along an equality of its indices.
 subst : {A : Set} (P : A → Set) {a b : A} → a ≡ b → P a → P b
 subst P refl p = p
--- Transport evidence for a two-place predicate along equalities of both indices.
-subst₂ : {A B : Set} (P : A → B → Set) {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → P a b → P a' b'
-subst₂ P refl refl p = p
 
 data Maybe (A : Set) : Set where
   nothing : Maybe A
   just    : A → Maybe A
 
--- Injectivity of `just`, cubical-compatibly.  The lemma defined by matching
--- (`just-inj (refl) = refl`, deleted 2026-11-01 as dead code) is refused under
--- the canonical flag set (scripts/proof-flags.sh, --cubical-compatible per
--- PROOF-POLICY §2.1):
+-- Injectivity of `just`, stated so that --cubical-compatible accepts it
+-- (PROOF-POLICY §2.1).  The obvious definition, matching `refl` against
+-- `just a ≡ just b`, asks the unifier for constructor injectivity, which
+-- Agda 2.6.4.3 refuses under that flag:
 --
---   warning: -W[no]UnsupportedIndexedMatch
---   This clause uses pattern-matching features that are not yet supported by
---   Cubical Agda ... Reason: It relies on injectivity of the data constructor
---   just, which is not yet supported
+--   warning: -W[no]UnsupportedIndexedMatch ... It relies on injectivity of
+--   the data constructor just, which is not yet supported
 --
--- and so was every clause of the TINI proof that matched `refl : just s ≡ just t`
--- (docs/proof-debt.adoc W-1, retired).  This version never matches on that
--- equation: it applies `cong` to a total projection, and `cong` matches `refl`
--- only against a variable.  `from-just d` returns the payload, or d for nothing.
--- Suppressing the warning, or dropping the flag, would have bought a green gate
--- with a weaker check; this is the cubical-compatible formulation instead.
+-- An earlier copy of that definition was deleted on 2026-11-01 for this
+-- reason.  This one matches nothing: it projects the equation through
+-- `from-just`, which computes, so no unification rule is needed.  The
+-- TINI proof (Noninterference.Generic) uses it wherever a finishing run's
+-- result must be read off `exec … ≡ just t`.
+
+-- The value inside a `just`, or the default for `nothing`.
 from-just : {A : Set} → A → Maybe A → A
 from-just d nothing  = d
-from-just _ (just a) = a
+from-just d (just a) = a
 
+-- Equal `just`s have equal contents.
 just-inj : {A : Set} {a b : A} → just a ≡ just b → a ≡ b
 just-inj {a = a} e = cong (from-just a) e
 
@@ -134,3 +131,4 @@ dec-stable (no ¬p) h = ⊥-elim (h ¬p)
 -- Excluded middle holds under double negation, for every proposition.
 ¬¬-dec : (P : Set) → ¬ ¬ Dec P
 ¬¬-dec P k = k (no λ p → k (yes p))
+
diff --git a/tests/flag-control/IndexedMatch.agda b/tests/flag-control/IndexedMatch.agda
new file mode 100644
index 0000000..a7d5335
--- /dev/null
+++ b/tests/flag-control/IndexedMatch.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+module IndexedMatch where
+open import SecretTypes.Prelude
+
+-- Must be refused, and only because --cubical-compatible is in force: this
+-- is the definition of just-inj that Prelude deliberately does not use.
+-- Matching refl here needs injectivity of `just`, which the flag rejects as
+-- -WUnsupportedIndexedMatch, made fatal by -W error.  Without the flag it
+-- type-checks, so scripts/check.sh fails if this module is ever accepted:
+-- that is the evidence the canonical invocation actually ran.
+invalid : {A : Set} {a b : A} → just a ≡ just b → a ≡ b
+invalid refl = refl
diff --git a/verification/receipts/agda-grade3_praxis.deed b/verification/receipts/agda_praxis.deed
similarity index 59%
rename from verification/receipts/agda-grade3_praxis.deed
rename to verification/receipts/agda_praxis.deed
index 07c6135..fb94439 100644
--- a/verification/receipts/agda-grade3_praxis.deed
+++ b/verification/receipts/agda_praxis.deed
@@ -4,10 +4,10 @@
 ;; This describes the gate and tree; the CI log is the execution evidence.
 (praxis-deed
   :schema-version "1.0.0"
-  :canonical-name "secret-types-agda-grade3-receipt"
+  :canonical-name "secret-types-agda-receipt"
   (identity
     :project "secret-types"
-    :name "agda-grade3 verification receipt"
+    :name "Agda verification receipt with Proof Witness Grades"
     :repository "hyperpolymath/secret-types"
     :repo-uuid #u5"github.com/hyperpolymath/secret-types"
     :uuid-source "uuid5(URL, github.com/hyperpolymath/secret-types)"
@@ -24,10 +24,13 @@
     :flags-note "One definition, read by the gate and by this receipt; the receipt cannot describe a gate that did not run")
   (conformance
     :policy "standards/3-practice/PROOF-POLICY.adoc"
-    :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01"
+    :policy-repository "hyperpolymath/standards"
+    :policy-commit "9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5"
+    :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01; section 8 (PWG) 2026-11-04"
     :canonical-invocation "agda --safe --without-K --cubical-compatible"
-    :cubical-compatible "met"
-    :waiver-history "docs/proof-debt.adoc#waivers (W-1, retired)"
+    :cubical-compatible "in-force"
+    :flag-control "tests/flag-control/IndexedMatch.agda"
+    :closed-waiver "W-1, docs/proof-debt.adoc#waivers"
     :stronger-than-canonical ("--no-libraries" "--ignore-interfaces" "--double-check" "-W error"))
   (gate
     :command "bash scripts/check.sh"
@@ -41,18 +44,30 @@
     :library-dependencies 0
     :axioms-assumed 0
     :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero")
-  ; Grades apply to theorems; refusal fixtures and leak witnesses are below Grade 3.
-  ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof.
+  ; PROOF-POLICY section 8: grades apply to theory theorems; demonstrations are ungraded.
+  ; Rocq and Lean legs are unavailable: no transport or hand re-proof exists yet, so no leg counts.
   (claims
-    (claim :id "N-1" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")
-    (claim :id "N-2" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")
-    (claim :id "N-3" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")
-    (claim :id "N-4" :token "tested-only" :grade "below-grade-3" :coq-leg "n/a" :lean-leg "n/a")
-    (claim :id "N-5" :token "tested-only" :grade "below-grade-3" :coq-leg "n/a" :lean-leg "n/a")
-    (claim :id "N-6" :token "tested-only" :grade "below-grade-3" :coq-leg "n/a" :lean-leg "n/a")
-    (claim :id "N-7" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")
-    (claim :id "N-8" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")
-    (claim :id "N-9" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")
+    (claim :id "N-1" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f
+      (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())
+      (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()))
+    (claim :id "N-2" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f
+      (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())
+      (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()))
+    (claim :id "N-3" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f
+      (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())
+      (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()))
+    (claim :id "N-4" :token "tested-only" :kind "demonstration" :pwg "ungraded")
+    (claim :id "N-5" :token "tested-only" :kind "demonstration" :pwg "ungraded")
+    (claim :id "N-6" :token "tested-only" :kind "demonstration" :pwg "ungraded")
+    (claim :id "N-7" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f
+      (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())
+      (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()))
+    (claim :id "N-8" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f
+      (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())
+      (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()))
+    (claim :id "N-9" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f
+      (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())
+      (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()))
   )
   ; Every module hash is checked against the current tree.
   (modules
@@ -63,10 +78,10 @@
     (module :path "src/SecretTypes/Lattice.agda" :sha256 "119d637de4dd4578c0eb0cd3dbad679f4281db9fa4660833fdd74b8d220ab10e")
     (module :path "src/SecretTypes/Lattice/Record.agda" :sha256 "25f4ee821b8e245dccb4f5f7eae9c3f1006a4b6eaeab3af14646721f14f83de3")
     (module :path "src/SecretTypes/Noninterference.agda" :sha256 "944231de8ab05155f2aaa8da6a37edfa32123cac25c29ea5a2e4a2d71f68ab0e")
-    (module :path "src/SecretTypes/Noninterference/Generic.agda" :sha256 "f969be56a8ce37526413ea7412c19368c04a018f655e9ca1b7e015323d32ff0c")
+    (module :path "src/SecretTypes/Noninterference/Generic.agda" :sha256 "716de16efc8ded98b0744fd38a5f95ca6e431b07dedb43e12140f5260e28af01")
     (module :path "src/SecretTypes/Noninterference/OutcomeVisibility.agda" :sha256 "33e63996ccb6ea5ba834dd158584b8a1fb5594d50e79c2ee2c144ffe7588d93a")
     (module :path "src/SecretTypes/Noninterference/Statement.agda" :sha256 "f76d84eb3a434c2f9f4203303fcf30fb04282afe787ce085d4590855b43e4c45")
-    (module :path "src/SecretTypes/Prelude.agda" :sha256 "efb8be7faab3798ec6da7c315fd9903cc6112bce98194a8463fbae9f52df6eee")
+    (module :path "src/SecretTypes/Prelude.agda" :sha256 "8ec095409f9424acf26e458e0ff1b129d1ca9525f37afa6d40e66bfcbd2cfed1")
     (module :path "src/SecretTypes/Typing.agda" :sha256 "f535815d15f4b224a028b01261af8d7f233d8b3c0a26e48ec5c4223f3afe1d42")
     (module :path "src/SecretTypes/Typing/Generic.agda" :sha256 "adacd5405be17ccbf845c56d2d7980d2b0eae7214a284df2bf5a64d64ccf7718")
     (module :path "src/SecretTypes/Vars.agda" :sha256 "f188cbc8b630b036daac4720f3cfe492bf78671f87b82850919f09091ead5422")