// SPDX-License-Identifier: MPL-2.0 = Absolute Zero — EXPLAINME :toc: preamble :toc-title: Contents :icons: font :doctype: article This file backs every factual claim in link:README.adoc[README.adoc] with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code. [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`. ==== == Claim-to-implementation map === CNO and OND are logically independent [quote, README.adoc] ____ The two pillars are logically independent (a proved theorem, with witnesses). ____ How this was implemented:: The independence theorem was proved in Coq (`archive/proofs/coq/ond/OND.v`, anchored to the core `is_CNO` definition, with witnesses that CNO does not entail OND and OND does not entail CNO); the active Agda `OND.agda` carries the same obligation zero-postulate. Caveat:: None currently known for the independence proof itself. However, the *coupling dial* between them (connecting a thing to the trace it casts) is explicitly framing, not theorem. === OND-1..5 are proved with zero axioms [quote, README.adoc (active stack)] ____OND obligations OND-1..5 are proved with zero postulates in Agda (`proofs/agda/OND.agda`, `--safe --without-K`)____ How this is implemented:: `link:proofs/agda/OND.agda[]` contains the active proofs; CI (`proofs.yml`, `agda` job) type-checks all four Agda modules under `--safe --without-K`. The historical Coq proof (`archive/proofs/coq/ond/OND.v`, every theorem `Closed under the global context`) and the Lean 4 mirror are archived; Z3 confirms the bounded instances (`proofs/z3/ond/OND_checks.smt2`, expect-annotated). Caveat:: OND proofs are axiom-free *relative to the declared observation model `O`*. The choice of `O` is a proof input, not a proof output. If `O` omits a real-world observable channel (e.g., power analysis), the OND proof is sound but physically incomplete. The residue list in `link:proofs/residue/[]` records this gap. === Coq CNO: 115 Qed, 0 Admitted, 61 Axioms [quote, README.adoc] ____115 Qed / 0 Admitted / 61 Axioms across 13 files — every theorem is discharged (no Admitted), but the development rests on 61 Coq + 52 Lean axioms.____ How this is implemented:: `link:proofs/coq/[]` contains all CNO theories. CI runs `coq_makefile` and confirms Qed counts and axiom counts. The axioms are domain-specific assumptions (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws) that are *assumed* but not derived within Coq. Caveat:: **This is not an axiom-free machine-checked proof.** "Machine-checked" here means the proof is valid *assuming the axioms hold*. If an axiom is false in the intended model, the theorem fails. The 61 Coq + 52 Lean axioms represent the proof debt. Discharging them (especially quantum unitarity and filesystem inverse laws) is the next major obligation. === Multi-prover verification across six systems [quote, README.adoc] ____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. 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. === Thermodynamic reversibility follows from Landauer's principle [quote, README.adoc] ____ThermodynamicallyReversible(p) — Zero energy____ How this is implemented:: `link:proofs/coq/physics/StatMech.v[]` and `link:proofs/lean4/StatMech.lean[]` formalise Landauer's principle and Bennett's reversible computing, proving CNOs dissipate zero energy because they erase no information. Caveat:: The physics formalisation relies on axioms about the physical model (e.g., that the thermodynamic system satisfies the assumptions of Landauer's principle). This is standard for formalisations of physics, but the gap between the mathematical model and physical metal is real. === CNO verification is undecidable in general [quote, README.adoc] ____The problem "Is program p a CNO?" is undecidable in general.____ How this is implemented:: Proved by reduction from the halting problem. Constructive witness: the ability to decide CNO-ness would decide halting. Caveat:: This is a standard result. The practical consequence is that the verified CNOs in this repo are specific programs or finite-state classes, not arbitrary input programs. == Dogfooded Across The Account [cols="1,2,2", options="header"] |=== | Technology / Pattern | Used here | Also used in | Coq CNO/OND formalisation | `proofs/coq/` | link:https://github.com/hyperpolymath/echo-types[echo-types] (EchoBridgeCNO) | Multi-prover pattern | Six provers + Idris ABI | link:https://github.com/hyperpolymath/kategoria[Kategoria] (Route δ) | OND residue-list honesty | `proofs/residue/` | link:https://github.com/hyperpolymath/epistemic-types[epistemic-types] (proof transport) |=== == Known gaps [CAUTION] ==== **61 Coq + 52 Lean axioms are unproven — in the ARCHIVED stack.** The archived CNO development (`archive/proofs/`) was machine-checked *relative to these axioms* (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws). These are historical counts of the archived trees, not active proof status and not estate-wide ground truth. The *active* Agda stack is zero-postulate. ==== [CAUTION] ==== **Coq, Lean 4, Isabelle/HOL and Mizar artefacts are archived and not run.** `archive/proofs/` is not built or gated. The active machine-checked evidence is Agda (`proofs/agda/`), Z3 bounded checks (`proofs/z3/`), and the Idris 2 ABI build — via `proofs/verify-active-provers.sh`. ==== [CAUTION] ==== **OND-6 (conditional composition) is OPEN — not proved, not assumed.** OND-1..5 are proved (zero postulates, active Agda). The capstone composition theorem remains the deliberate research fork; no `Admitted` or postulate stands in for it anywhere in the active stack. ==== [CAUTION] ==== **OND proofs are conditional on declared `O`.** An OND certificate is valid only for the observables in `O`. Out-of-scope channels (timing, power, cache, EM radiation) are listed in the residue, not blocked by the proof. ==== [CAUTION] ==== **CNO↔OND coupling dial is framing, not theorem.** The connection between a thing and the trace it casts to an observer is a conceptual bridge, not a formal result. ==== == Evidence Index [cols="2,3", options="header"] |=== | Path | Proves | `proofs/agda/` (CNO, OND, EchoBridge) | ACTIVE: both pillars, OND-1..5, zero postulates (`--safe --without-K`) | `proofs/z3/` + `proofs/verify-active-provers.sh` | ACTIVE: bounded expect-checked instances; one-shot active gate | `archive/proofs/coq/common/CNO.v` | ARCHIVED: core CNO framework (historical 115 Qed, 61 Axioms) | `archive/proofs/coq/ond/OND.v` | ARCHIVED: OND-1..5 (zero axioms) | `archive/proofs/coq/physics/StatMech.v` | ARCHIVED: Landauer's principle, thermodynamic reversibility | `archive/proofs/coq/category/CNOCategory.v` | ARCHIVED: universal CNO definition, model independence | `archive/proofs/lean4/` | ARCHIVED: Lean 4 mirrors (historical Phases 1–4, 52 Axioms) | `proofs/observation-models/` | Declared `O` inputs for OND | `proofs/residue/` | OND residue lists (out-of-scope observables) |===abc def ghi jkl mno pqr stu