hyperpolymath · Nov 10, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026
@@ -3,7 +3,7 @@
 # Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # Proof verification CI for the ACTIVE proof stack (owner ruling 2026-10-10):
-#   * Agda      — CNO + OND + EchoBridge (--safe --without-K)
+#   * Agda      — CNO + OND + EchoBridge (PROOF-POLICY 2.1 invocation + strict flags)
 #   * Z3        — CNO + OND bounded checks (expect-annotated)
 #   * Idris 2   — the ABI package (absolute-zero-abi.ipkg)
 # Each is an INDEPENDENT job, so one flaking never blocks the others.
@@ -66,14 +66,19 @@ jobs:
           mkdir -p "$HOME/.agda"
           echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries"
           echo "standard-library" > "$HOME/.agda/defaults"
-      - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K)
+      - name: Type-check CNO + OND + EchoBridge (4 modules, PROOF-POLICY 2.1 + strict flags)
         working-directory: proofs/agda
+        # The canonical invocation (standards PROOF-POLICY 2.1) is
+        # `agda --safe --without-K --cubical-compatible`.  The other strict
+        # language flags (--exact-split --no-sized-types --no-guardedness)
+        # are declared in each module's OPTIONS pragma, not here, so they do
+        # not also apply to the standard library.
         run: |
           agda --version
-          agda --safe --without-K CNO.agda
-          agda --safe --without-K OND.agda
-          agda --safe --without-K EchoBridgeScaffold.agda
-          agda --safe --without-K EchoBridgeCNO.agda
+          agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch CNO.agda
+          agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch OND.agda
+          agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch EchoBridgeScaffold.agda
+          agda --safe --without-K --cubical-compatible --double-check -W error -W noUnsupportedIndexedMatch EchoBridgeCNO.agda
           echo "✓ Agda: CNO + OND + EchoBridgeScaffold + EchoBridgeCNO type-check"
 
   z3:

@@ -9,7 +9,7 @@ This file backs every factual claim in link:README.adoc[README.adoc] with code p
 
 [IMPORTANT]
 ====
-*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths below of the form `proofs/coq/…` / `proofs/lean4/…` refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records the estate proof grades (mathesis `estate-mathematical-architecture` §5) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` at **Grade 3** (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are `tested-only`, and OND-6 is `open`.
+*Archive notice (2026-10-10, reconciled 2026-11-01).* The active proof stack is Agda (`proofs/agda/`, `--safe --without-K`, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under `archive/proofs/`; paths below of the form `proofs/coq/…` / `proofs/lean4/…` refer to the *archived* trees (`archive/proofs/coq/…` etc.), and counts such as "115 Qed / 61 Axioms" are *historical* figures of those archived trees. The canonical active-vs-archived proof-status table is link:PROOF-STATUS.adoc[PROOF-STATUS.adoc], which also records Proof Witness Grades (standards PROOF-POLICY §8) and the closed ledger vocabulary of `hyperpolymath/standards` (`proven` / `proven-with-postulates` / `tested-only` / `argued` / `open`): the active Agda proofs are `proven` and `ungraded` (no PWG-3 receipt recorded yet), the Z3 bounded checks are `tested-only`, and OND-6 is `open`. Its 2026-11-09 design audit records that the active Agda `IsCNO` was degenerate (termination and reversibility held by construction) and how it was restated over a pc-driven machine the same day.
 ====
 
 == Claim-to-implementation map
@@ -55,10 +55,10 @@ Caveat::
 ____Verify CNO properties in six independent proof systems.____
 
 How this is implemented::
-Artefacts exist for Coq, Lean 4, Agda, Z3, Isabelle, and Mizar in `link:proofs/[]`. `link:proofs/verify-all-provers.sh[]` orchestrates verification. CI gates Coq, Lean 4, and Agda.
+Active artefacts are Agda, Z3 and the Idris 2 ABI in `link:proofs/[]`, run by `link:proofs/verify-active-provers.sh[]` and CI. Coq, Lean 4, Isabelle and Mizar are archived under `archive/proofs/` and are not built or gated.
 
 Caveat::
-**Z3, Isabelle, and Mizar are generated but not yet run in CI.** The artefacts exist but are not evidence until machine-executed and green. The "six prover" claim describes the target architecture, not the current CI gate.
+**Isabelle and Mizar are archived and not run in CI.** Z3 runs in CI (the `z3` job in `.github/workflows/proofs.yml`) as bounded, `tested-only` checks. The "six prover" claim describes the target architecture, not the current CI gate.
 
 === Thermodynamic reversibility follows from Landauer's principle
 

@@ -12,7 +12,7 @@ Cross-reference glossary for link:README.adoc[README.adoc], link:EXPLAINME.adoc[
 [[cno]]
 CNO (Certified Null Effect)::
   A program that does nothing to the world: terminates, maps input state to identical output state, is pure, and is thermodynamically reversible. The conserved quantity is state.
-  *Classification:* **novel assembly** (standard concepts combined into this specific 4-field record).
+  *Classification:* **novel assembly** (standard concepts combined; the intended notion has four parts, while the active Agda `IsCNO` record has two fields, see <<is-cno>>).
 
 [[ond]]
 OND (Observational Null Disclosure)::
@@ -28,7 +28,7 @@ Coupling dial::
 
 [[is-cno]]
 IsCNO(p)::
-  The core predicate: `Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p)`.
+  The core predicate. Intended notion: `Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p)`. Active Agda (`proofs/agda/CNO.agda`): from every state the pc-driven machine stops normally (`cno-terminates`), and every normal stop is `obs-eq` to the start (`cno-identity`). Purity and observational reversibility are derived; no thermodynamic claim is made.
   *Classification:* **project-specific** (formalisation).
 
 [[landauer-principle]]
@@ -38,7 +38,7 @@ Landauer's principle::
 
 [[reversible-computing]]
 Reversible computing::
-  Computation that can be undone with zero energy cost (Bennett 1973). A required field of `IsCNO`.
+  Computation that can be undone with zero energy cost (Bennett 1973). Part of the intended CNO notion; the active Agda proves only observational reversibility (`cno-left-inverse`), not an energy bound.
   *Classification:* **standard** (Bennett 1973).
 
 == OND concepts

@@ -45,27 +45,30 @@ ground truth** — see "Role of this repository" below.
 `hyperpolymath/standards` (`3-practice/PROOF-POLICY.adoc` §5 and
 `docs/README-EXPLAINME-STANDARD.adoc` §5): `proven`, `proven-with-postulates`,
 `tested-only`, `argued`, `open` — recorded exactly, never flattened into a
-percentage. Estate grades follow mathesis's `estate-mathematical-architecture`
-§5–6: **Grade 3** = type-checks locally in Agda under strict flags but not yet
-translated to an independent foundational system; **Grade 2i/2ii** =
-translation to one/two independent foundations (2ii requires a non-DTT
-second system, e.g. Isabelle/HOL); **Grade 1** = headless CI via verified
-checker APIs. Verification receipts are tied to commit hashes; superseded
-claims are marked historical, not silently dropped, and axiom dependence
-(`Print Assumptions` / `#print axioms`) is tracked per row.
+percentage. Grades are Proof Witness Grades (PWG) as defined in
+PROOF-POLICY §8 (owner ruling 2026-11-04), which supersedes the "Grade
+3/2i/2ii/1" ladder of mathesis's `estate-mathematical-architecture` brief
+that this file used until 2026-11-09. `PWG-3` needs an Agda receipt under the
+§2.1 invocation `agda --safe --without-K --cubical-compatible`, recording the
+Agda version, standard-library pin, flags in force, import cone and source
+commit; `PWG-2i`/`PWG-2ii` additionally need one/both Rocq and Lean legs whose
+§2.2 correspondence state is `RECONCILED`. A theorem below `PWG-3` is
+`ungraded`. A status token and a grade are separate fields and are never
+written in one cell. Superseded claims are marked historical, not silently
+dropped, and axiom dependence is tracked per row.
 
 [cols="2,1,2,3",options="header"]
 |===
 | Artefact / claim | Stack status | Proof status (ledger token — estate grade) | Scope and assumptions
 
 | `proofs/agda/` — `CNO.agda`, `OND.agda`, `EchoBridgeScaffold.agda`, `EchoBridgeCNO.agda`
 | ACTIVE (CI `agda` job; `proofs/verify-active-provers.sh`)
-| `proven` — **Grade 3**: type-checked locally in Agda, zero postulates, every file `{-# OPTIONS --safe --without-K #-}`; EchoBridge takes funext as an *explicit hypothesis*, not a global postulate. Not translated to any independent foundation, so not Grade 2+
-| Domain formalisation of both pillars; discharges OND-1..5; contains no OND-6. Open obligation: recheck under the 2026-11-01 canonical profile `agda --safe --without-K --cubical-compatible` (standards PROOF-POLICY §2.1) — prior `--safe --without-K` receipts are not receipts for the combined profile
+| Status: `proven` for each stated Agda term — zero postulates, every file `{-# OPTIONS --safe --without-K #-}`; EchoBridge takes funext as an *explicit hypothesis*, not a global postulate. Grade: `ungraded` (no PWG-3 receipt recorded; see the 2026-11-09 audit below). *What the CNO terms state is narrower than the pillar description*: see "Design audit (2026-11-09)" below before citing any CNO result
+| Domain formalisation of both pillars; discharges OND-1..5; contains no OND-6. The canonical profile `agda --safe --without-K --cubical-compatible` (standards PROOF-POLICY §2.1) passes locally (2026-11-09) and is the CI invocation from 2026-11-09. Open obligation: a PWG-3 receipt for that profile
 
 | `proofs/z3/` — `ond/OND_checks.smt2` via `proofs/z3/verify.sh`
 | ACTIVE as bounded-check solver (CI `z3` job)
-| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (z3 5.3.3, `Z3-CHECK OK`, sat/unsat/sat) — see receipts below
+| `tested-only` — bounded SMT checks, no proof grade; every `(check-sat)` carries a `; expect sat|unsat` annotation. Receipt reproduced in this sandbox 2026-11-01 (`z3` 4.16.0, `Z3-CHECK OK`, sat/unsat/sat) — see receipts below
 | Bounds: finite/bounded programs under a finite declared `O`; not a general proof
 
 | `src/abi/` + `absolute-zero-abi.ipkg` (Idris 2)
@@ -104,9 +107,69 @@ claims are marked historical, not silently dropped, and axiom dependence
 | Declared observation models `+O+` and residue lists; every OND certificate is relative to its declared `+O+`
 |===
 
+=== Design audit (2026-11-09)
+
+A statement-level review of the active Agda (`proofs/agda/` at `cbe9ae9`)
+against the claims in this file, README, EXPLAINME and `docs/TWO-PILLARS.adoc`.
+The terms all type-check: on 2026-11-09 the four modules at `cbe9ae9` were rechecked cold
+with Agda 2.6.3 and agda-stdlib 2.3 (CI pairs Agda 2.6.3 with agda-stdlib 1.7.3) under
+`agda --safe --without-K --cubical-compatible`, and all passed. That is a local check, not a CI
+receipt. The findings concern what the terms *state*.
+
+[cols="2,3,2",options="header"]
+|===
+| Item | What the Agda actually states | Honest label
+
+| `IsCNO` (`CNO.agda`)
+| `state-eq` includes `state-pc`. `step` advances the PC on `Nop`, `Load`,
+`Store` and `Add` and sets it on `Jump`; `eval` never restores it. So
+`cno-identity : ∀ s → state-eq (eval p s) s` holds only for programs made
+of `Halt` instructions (and the empty program). The archived Coq fixed
+the same defect on 2026-05-18 by excluding the PC from `state_eq`; the
+active Agda did not.
+| `IsCNO` is a degenerate class in the active stack. `halt-is-cno`,
+`cno-composition` and every result quantified over `IsCNO` are `proven`
+but about that class only. *Resolved 2026-11-09:* `IsCNO` now judges a run by `obs-eq` (memory, registers, I/O; no PC). `nop-is-cno` and `jump-exit-is-cno` show the class is not Halt-only; `load-not-cno` shows it is not everything. `state-eq` keeps the PC and is still the full equality.
+
+| `terminates`, `terminates-always`
+| `terminates p s = ∃ s′. eval p s ≡ s′`, inhabited by `(eval p s , refl)`
+for every program. `eval` is a total fold over the instruction list.
+| Holds by construction; *not* a termination result. *Resolved 2026-11-09:* `eval` is replaced by a pc-driven machine: a big-step relation `_⊢_⇓_` and a fuel interpreter `run`, related by `run-sound` and `run-complete`. `Terminates p s` asks for a normal stop from pc 0, and `jump-self-diverges` shows `Jump 0` never stops. A Store or Add on a missing register faults and does not terminate.
+
+| `thermodynamically-reversible`, `energy-dissipated`
+| `energy-dissipated _ _ _ = zero`, so every program, reversible or not,
+satisfies it. `reversible` is defined but never used.
+| Holds by construction; *not* a Landauer/Bennett result. The archived Coq
+`StatMech`/`LandauerDerivation` development is the only thermodynamic
+formalisation, and it is archived. *Resolved 2026-11-09:* `energy-dissipated`, `thermodynamically-reversible` and the unused `reversible` are removed. `cno-left-inverse` proves observational reversibility (running any CNO after a CNO restores memory, registers and I/O) as a consequence of the identity law, and claims nothing thermodynamic.
+
+| OND-5 "mirrored in Lean 4, Agda, Z3"
+| Agda states OND-5 under `O-out`; the archived Coq and Lean state it under
+`O_all`. Both are true; they are different propositions.
+| Correspondence state `unassessed` (PROOF-POLICY §2.2). The rows are not
+mirrors of one theorem.
+
+| OND-3 "anchored to `is_CNO`"
+| `OND.agda` uses a local `is-null` and never imports `CNO`. The anchoring
+(`writer_program_not_core_CNO`, `skip_program_is_core_CNO`) exists only in
+the archived Coq.
+| The active Agda OND-3 is *not* anchored to `IsCNO`.
+
+| EchoBridge
+| The `≡`-form results (`echo-from-cno-program-≡`, `absolute-zero-echo-≡`)
+take funext as a hypothesis; the `EchoRel` results do not. The echo is the
+fixed-point witness `(s , cno-identity)`.
+| `proven`, conditional on funext where stated; inherits the `IsCNO`
+degeneracy above. *Resolved 2026-11-09:* restated over `cno-result` and `obs-eq`; the `≡` form is now on the observable projection `observe`, and `program-state-model` is a `CNOModel` over observable states.
+|===
+
+Downstream: `hyperpolymath/echo-types` imports `CNO` (`EchoCNOBridge`,
+`EchoCNOSemantics`, `EchoThermodynamicsArbitrary`, `EchoCNOPackaging`); its
+CNO-facing results inherit these limits.
+
 === Reproduction receipts (this environment, 2026-11-01)
 
-* *Z3 — REPRODUCED HERE.* `z3` 5.3.3 (64-bit, via the `z3-solver` PyPI wheel,
+* *Z3 — REPRODUCED HERE.* `z3` 4.16.0 (64-bit, via the `z3-solver` PyPI wheel,
 the only package host reachable from this sandbox) running
 `bash proofs/z3/verify.sh` → `Z3-CHECK OK`: 1 file
 (`proofs/z3/ond/OND_checks.smt2`), 3 `(check-sat)` verdicts `sat unsat sat`,
@@ -134,7 +197,7 @@ be cited as proof status for any other repository.
 *Cross-repo note (2026-11-01).* `epistemic-types` (at `5422cd5`) is an
 *independent* proof library with **no dependency on absolute-zero**. Any
 cross-repo claim must therefore name the exact theorem, its scope, and its
-assumptions (e.g. "OND-1..5, `proven`, Grade 3, Agda `--safe --without-K`,
+assumptions (e.g. "OND-1..5, `proven`, `ungraded`, Agda `--safe --without-K`,
 relative to a declared `O`") — never a bare count imported from this repo.
 Mathesis (the estate mathematical knowledge commons) may *catalogue* these
 receipts and grades, but per its own architecture the original repositories

@@ -54,9 +54,17 @@ Secret→observable channel
 
 |===
 
-Both pillars are machine-checked. OND obligations OND-1..5 are proved
-with zero axioms in Coq, mirrored in Lean 4, Agda, and Z3. The
-independence theorem is anchored to `+is_CNO+`. OND-6 (conditional
+OND obligations OND-1..5 are proved with zero axioms in the active Agda
+(`proofs/agda/OND.agda`); archived Coq and Lean developments and bounded Z3
+checks exist, but the Agda and Coq/Lean OND-5 statements are different
+propositions, and the anchoring of the independence theorem to `+is_CNO+`
+exists only in the archived Coq. The active Agda CNO definition was
+degenerate until 2026-11-09 (Halt-only, with termination and
+reversibility holding by construction). It is now stated over a
+pc-driven machine: termination is a real property, identity is up to
+observable state (memory, registers, I/O), and nothing thermodynamic is
+claimed. See the 2026-11-09 design audit in
+link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. OND-6 (conditional
 composition, the research capstone) remains open by design.
 
 == What is standard and what is ours
@@ -188,10 +196,10 @@ The *canonical* proof-status table — separating active, archived, proved,
 axiomatic and generated artefacts, with OND-6 explicitly open — lives in
 link:PROOF-STATUS.adoc[PROOF-STATUS.adoc]. Figures quoted above for archived
 provers are historical counts of those archived trees, not active status.
-Estate proof grades (mathesis `estate-mathematical-architecture` §5) are
-recorded there too: the active Agda proofs are **Grade 3** (local,
-strict-flag, zero-postulate — not yet translated to an independent
-foundation), the Z3 checks are `tested-only` (bounded), and OND-6 is `open`.
+Proof Witness Grades (standards PROOF-POLICY §8) are recorded there too:
+the active Agda proofs are `proven` but `ungraded` until a PWG-3 receipt
+is recorded, the Z3 checks are `tested-only` (bounded), and OND-6 is
+`open`.
 
 == [CAUTION]
 

@@ -61,6 +61,19 @@ Agda, Isabelle, Mizar), `is_CNO p` bundles four properties:
 4. *Thermodynamic reversibility* — zero energy dissipation by Landauer's
    principle (logical reversibility ⇒ no entropy increase, via Bennett).
 
+[WARNING]
+.Active Agda status (2026-11-09)
+====
+These four properties describe the intended notion. The active Agda
+(`proofs/agda/CNO.agda`, restated 2026-11-09) formalises (1) as a normal stop
+of a pc-driven machine, (2) up to memory, registers and I/O (not the program
+counter), and (3) as a consequence of (2). It formalises (4) only as
+observational reversibility (`cno-left-inverse`), with no energy model. Before
+that date (1) and (4) held by construction and `IsCNO` was Halt-only. See the
+design audit in
+link:../PROOF-STATUS.adoc[PROOF-STATUS.adoc].
+====
+
 The defining feature of CNO is that *everything it talks about is inside the
 model*. State is a modelled object; "the output state equals the input state"
 is a closed mathematical statement, provable without reference to any physical