diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 5d5ebfc..b321355 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -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. diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 62aa215..cfbac8b 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -45,14 +45,17 @@ 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"] |=== @@ -60,7 +63,7 @@ claims are marked historical, not silently dropped, and axiom dependence | `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 diff --git a/README.adoc b/README.adoc index 7aa1739..6aa2e6a 100644 --- a/README.adoc +++ b/README.adoc @@ -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] diff --git a/docs/TWO-PILLARS.adoc b/docs/TWO-PILLARS.adoc index 906283c..4cee7b0 100644 --- a/docs/TWO-PILLARS.adoc +++ b/docs/TWO-PILLARS.adoc @@ -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 diff --git a/proofs/agda/CNO.agda b/proofs/agda/CNO.agda index 5b52d65..c4a2669 100644 --- a/proofs/agda/CNO.agda +++ b/proofs/agda/CNO.agda @@ -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