hyperpolymath · Nov 9, 2026
@@ -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` is degenerate and that its termination and reversibility components hold by construction.
 ====
 
 == Claim-to-implementation map
@@ -55,7 +55,7 @@ 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.

@@ -45,22 +45,25 @@ 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+
+| 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. 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
 
 | `proofs/z3/` — `ond/OND_checks.smt2` via `proofs/z3/verify.sh`
@@ -104,9 +107,71 @@ 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 were rechecked cold
+with Agda 2.6.3 and agda-stdlib 2.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. *Open:* redefine `state-eq` without the PC.
+
+| `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. The pillar's
+"terminates on every input" is not formalised in the active Agda.
+
+| `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.
+
+| 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.
+|===
+
+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` 5.3.3 as recorded (2026-11-09: this version string
+is unverified — no Z3 5.x release is known, and the receipt below records 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 +199,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,15 @@ 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 is
+currently degenerate (it holds only for `Halt`-only programs), and its
+termination and thermodynamic-reversibility components hold by
+construction. 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 +194,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,16 @@ 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. In the active Agda
+(`proofs/agda/CNO.agda`), (1) and (4) hold by construction for every program,
+and (2) uses a state equality that includes the program counter, so `IsCNO`
+holds only for `Halt`-only programs. 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

@@ -211,6 +211,15 @@ thermodynamically-reversible p =
 ----------------------------------------------------------------------------
 
 -- A Certified Null Operation
+--
+-- Audit note (2026-11-09, see PROOF-STATUS.adoc "Design audit"): as stated,
+-- this class is degenerate.  `state-eq` includes `state-pc`, and `step`
+-- moves the PC on every instruction except `Halt`, so `cno-identity` holds
+-- only for `Halt`-only programs.  `cno-terminates` and `cno-reversible` hold
+-- for every program by construction (`terminates-always`, and
+-- `energy-dissipated` is constantly zero).  Results over `IsCNO` are proved
+-- but are about that narrow class.  Redefining `state-eq` without the PC (as
+-- the archived Coq did on 2026-05-18) is an open obligation.
 record IsCNO (p : Program) : Set where
   field
     cno-terminates : ∀ s → terminates p s