// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = absolute-zero — Proof Status :toc: [abstract] absolute-zero formalises *two co-equal pillars* (see `docs/TWO-PILLARS.adoc`): *CNO* — Certified Null Operations (certified null *effect*) — and *OND* — Observational Null Disclosure (certified null *disclosure*). This document records the *actually reproduced* verification state in this environment, prover by prover, and is explicit about which axioms remain and why. [IMPORTANT] .2026-07-07 — both pillars machine-checked across six provers (HISTORICAL since 2026-10-10) ==== *Historical (superseded by the 2026-10-10 archive ruling below):* all six provers were reproduced in this environment via `proofs/verify-all-provers.sh` (`ALL-PROVERS-GREEN`): *Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar*, plus the *Idris 2* ABI. Today only Agda, Z3 (bounded) and the Idris 2 ABI are active — see the canonical table below. Both the CNO and OND pillars were covered. An absent prover is a *failure*, never a skip (since 2026-09-23 — before that Isabelle and Mizar printed "skipped" and the gate could say GREEN on four of six), and Z3 verdicts are compared with the `; expect sat|unsat` annotation on every `(check-sat)` (`proofs/z3/verify.sh`). Since 2026-09-23 the gate also runs the Coq `Print Assumptions` audit and its `--control` after the build, so a theorem resting on an axiom, or an audit that can no longer say no, turns it red. `proofs/tests/gate-selftest.sh` proves both gates turn red for each absent or failing prover, for each verdict mutant and for both audit mutants (16 cases, run in CI). ==== [IMPORTANT] ==== *Archive notice (2026-10-10).* The active proof stack is now Idris 2 (ABI) and Agda (CNO, OND, EchoBridge), with Z3 as a bounded-check solver. Coq, Lean 4, Isabelle/HOL and Mizar are archived under `archive/proofs/` (see `archive/README.adoc`). Text that describes those provers as active is historical until the full rewrite lands. ==== == Canonical proof-status reconciliation (2026-11-01) This table is the *single canonical statement* of proof status in this repository. Where older prose (README, EXPLAINME, ROADMAP, `docs/*`) quotes counts such as "115 Qed / 0 Admitted / 61 Axioms", those figures describe the *archived* Coq tree under `archive/proofs/coq/` only. They are historical, they are not active, and they are **not estate-wide proof-status ground truth** — see "Role of this repository" below. *Grading scheme.* Statuses below use the closed proof-ledger vocabulary of `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. [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 | `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 | Bounds: finite/bounded programs under a finite declared `O`; not a general proof | `src/abi/` + `absolute-zero-abi.ipkg` (Idris 2) | ACTIVE (CI `idris` job) | `argued` — engineering-path interface artefact; type-checks, proves nothing | ABI/FFI boundary only; carries `believe_me` escape hatches (T7 ruling) — not evidence for any theorem | `archive/proofs/coq/` — 14 theories | ARCHIVED 2026-10-10 — not built, not gated | `proven-with-postulates` — *historical, superseded*: headline "115 Qed / 0 Admitted / 61 Axioms"; census 109/182 top-level theorems closed under the global context, 73 resting on stdlib classical axioms and/or tagged parameters; 17 headline theorems zero-axiom. At best a Grade 2i *candidate* (Coq is DTT-family like Agda); receipts predate the archive ruling and are not CI evidence | Counts describe this archived tree only; class-A / METAL-BOUNDARY tag grammar as recorded in the tree | `archive/proofs/lean4/` | ARCHIVED 2026-10-10 — not built, not gated | `proven-with-postulates` — *historical*: 52 Lean axioms incl. the strengthened `FilesystemCNO` preconditions and the class-A `y_combinator_not_identity`. Lean is DTT-family, so this leg adds no foundational diversity toward Grade 2ii | Historical counts describe this tree only | `archive/proofs/isabelle/`, `archive/proofs/mizar/` | ARCHIVED 2026-10-10 — not built, not gated | *Historical receipts*: proved in their day (Isabelle: no `sorry`/`oops`; Mizar: empty `CNO.err`). Isabelle/HOL is the non-DTT (HOL/LCF) leg that could have supported Grade 2ii diversity — but it is archived and unexecuted, so it confers no current grade | Not evidence in the active gate | `archive/proofs/verify-all-provers.six-prover.sh` + `archive/proofs/tests/gate-selftest.six-prover.sh` | ARCHIVED — superseded by `proofs/verify-active-provers.sh` | GENERATED gate script — historical | Former six-prover gate (Coq, Agda, Lean, Z3, Isabelle, Mizar + Idris ABI) | OND-6 — conditional composition (research capstone) | OPEN in every stack | `open` — not proved, not assumed; no `Admitted`/postulate smuggled in anywhere in the active stack | `docs/OND-ROADMAP.adoc`; deliberately open research fork | `proofs/observation-models/`, `proofs/residue/` | ACTIVE inputs | `argued` — declarative/generate proof inputs and honesty registers, not proofs | Declared observation models `+O+` and residue lists; every OND certificate is relative to its declared `+O+` |=== === Reproduction receipts (this environment, 2026-11-01) * *Z3 — REPRODUCED HERE.* `z3` 5.3.3 (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`, all matching their `; expect` annotations, exit 0. Receipt commit: working tree on branch `arena/1a7659fe-absolute-zero` over `bb46232`. * *Agda, Idris 2, Coq, Lean 4, Isabelle/HOL, Mizar, Rust/Creusot — NOT RUNNABLE HERE.* The sandbox egress allowlist (github.com, codeload.github.com, api.github.com, registry.npmjs.org, pypi.org, files.pythonhosted.org) blocks apt mirrors, static.rust-lang.org, opam.ocaml.org and Hackage, so none of these toolchains can be installed in this session. Per standards `3-practice/PROOF-POLICY.adoc` §6, a leg that cannot run is *said so*, never reported as passing: the Agda `--safe --without-K` checks, the `--cubical-compatible` recheck (open obligation, above), and the Idris 2 ABI build remain CI receipts (`proofs.yml`: `agda`, `z3`, `idris` jobs), not sandbox receipts. Archived provers stay archived and unexecuted. === Role of this repository (consumer, not estate-wide ground truth) absolute-zero is a *consumer and domain formalisation*: it applies standard results (Landauer 1961, Bennett 1973, the non-interference literature, category theory) to its own CNO/OND domain concepts. Its historical prover counts (above) are evidence about its own archived trees only, and must not 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`, 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 remain the sovereign owners of their mathematics; this file is the local proof-status record of record. [NOTE] ==== The per-prover sections below this table are *historical* for Coq, Lean 4, Isabelle/HOL and Mizar (archived 2026-10-10) and *active* only for Agda, Z3 (bounded) and the Idris 2 ABI. They are kept for the record; the table above is the canonical summary. ==== == Coq — VERIFIED (this environment) * `coqc` **8.18.0**; clean build from scratch (all `.vo`/`.glob` deleted first), via `coq_makefile -f _CoqProject` over **14/14 theories → zero errors**. * Reproduce: `cd proofs/coq && coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all -j`. [cols="1,3",options="header"] |=== | Area | Theory | common | `CNO.v`, `Complex.v`, `PhysicsConstants.v`, `StatMechBasis.v` | category | `CNOCategory.v` | quantum | `QuantumCNO.v`, `QuantumMechanicsExact.v` | lambda | `LambdaCNO.v` | filesystem| `FilesystemCNO.v` | physics | `StatMech.v`, `StatMech_helpers.v`, `LandauerDerivation.v` | ond | `OND.v` (NEW — the disclosure pillar) | malbolge | `MalbolgeCore.v` |=== === CNO axiom discharge (2026-07-07) The CNO domain modules previously *axiomatised* their headline results. They have been re-grounded on concrete models and re-proved. Axiom/`Parameter`/`Conjecture` count fell from **98** to a small, classified remainder: * *Fully discharged to zero project axioms*: `FilesystemCNO.v` (13 axioms + 3 parameters → 0; `mkdir_rmdir_inverse`, `transaction_cno`, `snapshot_restore_identity`, … all `Closed under the global context`), `CNOCategory.v` (identity/hom functor constructed), `QuantumMechanicsExact.v` (X-gate unitarity proved; density matrix defined). * `QuantumCNO.v`: 41 → 12. *19 axioms discharged, 8 parameters concretised*; **two latent-unsound axioms removed** (`no_cloning` was provably false in the flat model; `Cconj_Cexp` false for a genuine phase). Remainder = 2 tagged metal-boundary physics postulates + 4 honestly-labelled class-A items (below). * `LambdaCNO.v`: `compile_lambda` and `hom_functor` (in `CNOCategory.v`) concretised; **a third latent-unsound axiom corrected** — `eta_equivalence` was *false as stated* (counterexample `f = LVar 5`, a normal form that never β-reduces to `f`; root cause: this file's `subst` does not re-index under binders). It is replaced by the honest, proved theorem `eta_equivalence` guarded by a `no_lambda body` hypothesis (a genuine statement-shape change, disclosed in-file, made to remove an inconsistency risk — not to dodge a proof). * Physics (`StatMechBasis.v`, `PhysicsConstants.v`, `StatMech.v`, `LandauerDerivation.v`): derivable lemmas discharged; the genuine *physical postulates* kept and tagged `METAL-BOUNDARY AXIOM` — Boltzmann constant `kB` and `kB > 0`, absolute `temperature > 0`, the Second Law, Landauer's 1961 bound. These are empirical physics and *must* remain axioms; `state_dec` is kept because `Memory = nat -> nat` is not decidably equal (genuinely unprovable). === Honestly-remaining axioms (class A — true, provable in principle, not yet machine-proved) Every remaining project axiom is either a tagged physical postulate (above) or one of these, each documented in-file with its blocker: * `LambdaCNO.v` — `y_not_cno` (`~ is_lambda_CNO y_combinator`). True (Y diverges), but a rigorous proof must rule out reaching the argument under *every* β-congruence interleaving — a coinductive / step-indexed non-termination argument beyond a single-file fix. * `QuantumCNO.v` — `CNOT_gate_unitary` (needs a 4-dimensional tensor model), `unitary_inverse_property` (needs finite-dimensional linear algebra), `fidelity_bound` / `approximate_cno` (need a concrete fidelity). All out of reach of the flat `nat -> C` single-qubit model; faithful discharge is a separate formalisation. These are the analogue of the OND-6 research fork: openly labelled, not silently assumed. `Print Assumptions` on each of the 17 theorems this document names in backticks prints `Closed under the global context` — no stdlib axiom and no project axiom (measured 2026-09-23, Coq 8.18). That is CI-gated: `proofs/coq/audit/Assumptions.v` lists the 17 and `proofs/coq/check-assumptions.sh` (Coq job of `proofs.yml`, and the canonical `proofs/verify-all-provers.sh` gate since 2026-09-23) fails on any `Axioms:` block or a missing line; its `--control` mode proves the gate bites by requiring that `landauer_limit_positive`, which rests on `kB_positive`, is rejected. The wider tree is not closed — 109 of 182 top-level theorems are; the other 73 rest on stdlib classical axioms and/or the tagged parameters — see #171 for the census and the tag-grammar work. === Reversibility <-> CNO bridge (2026-07-16, the theorem MAA cites) `proofs/coq/common/CNO.v` now carries the bridge between `reversible` and the "composes to a no-op" characterisation the MAA framework (aletheia) cites. All five new results are **`Closed under the global context` (zero axioms)**: * `reversible_iff_exists_reverses` — the repo's `reversible` is exactly "exists a one-sided left inverse" (`exists p_inv, reverses p p_inv`). * `reverses_seq_computes_identity` — the core lemma: a left inverse sequenced after `p` computes the state-identity on every composite transition (via `eval_app` + `eval_deterministic`). * `cno_equiv_seq_empty_of_reverses` — repackaged as `cno_equiv (p ;; p_inv) []` (CNO-equivalence to the canonical no-op). * `reversible_bridge_forward` — the faithful *forward* direction of the aletheia contract: a **two-sided** inverse makes *both* composites CNO-equivalent to the no-op. * `reversible_bridge_backward_upto` — the *backward* direction, **necessarily up to `=st=`**, with an explicit `p_inv`-termination hypothesis. *Honesty note.* The literal biconditional `reversible p <-> exists p_inv, is_CNO (p;;p_inv) /\ is_CNO (p_inv;;p)` is **not** provable under these definitions, and is deliberately *not* asserted: (1) `is_CNO` also demands purity and totality, which a `reversible` program need not have — so "=== CNO" is rendered by `cno_equiv _ []` (the identity-on-state component); (2) `state_eq` excludes the program counter while `eval` propagates it (the `eval_respects_state_eq_*` axioms were removed as unsound on 2026-05-20), forcing the backward direction to be up-to-`=st=`; (3) the repo's `reversible` is one-sided whereas the contract is two-sided. The in-file section header documents all three. This is a genuine statement-shape finding: it tells the aletheia contract to be stated two-sided and `=st=`-relative, not a proof dodged. *Lean mirror — `proofs/lean4/CNOBridge.lean` (UNVERIFIED in this environment).* A functional-model mirror of the five bridge results was written for Lean 4, but it could **not** be machine-checked here: the Lean toolchain and Mathlib cache download from GitHub release assets, which the egress policy blocked (HTTP 403). It is registered in `lakefile.lean` as a **non-`@[default_target]`** `lean_lib`, so it does not gate the standard `lake build`; verify with `lake build CNOBridge` (+ `#print axioms`) where the toolchain is available. Note the mirror states the bridge with *syntactic* state equality (Lean's `eval` is a total function and `ProgramState.eq` includes the PC), a stronger/cleaner form than the Coq `=st=`-relative statement — a disclosed cross-model difference, not a claim of literal equivalence. == OND — VERIFIED (this environment), the disclosure pillar `proofs/coq/ond/OND.v` discharges roadmap obligations *OND-1..OND-5* with **zero axioms** — every theorem is `Closed under the global context`: * OND-1 `is_OND O o` — nullity parameterised by an observation model `O` over an observable execution (declared output channel + timing); * OND-2 — `skip` is OND under *any* `O` (satisfiability); * OND-3 — `is_CNO ⊥ is_OND` independence, additionally anchored to the *real* core `is_CNO` (`writer_program_not_core_CNO`, `skip_program_is_core_CNO`); * OND-4 — a constant-time select operation is OND under a declared `O` (+ residue); * OND-5 — a non-composition counterexample (two ONDs whose composite leaks by state-chaining). Mirrored in *Lean 4* (`proofs/lean4/OND.lean`), *Agda* (`proofs/agda/OND.agda`), and *Z3* (`proofs/z3/ond/OND_checks.smt2`, the bounded/finite instances). OND-7's residue register carries its first real instance (`proofs/residue/ct_select.residue`). *OND-6* (conditional composition, research capstone) remains open by design — see `docs/OND-ROADMAP.adoc`. == Agda — VERIFIED (this environment) * `agda` 2.6.3 (CI) / 2.6.4.3 (local), `--safe --without-K`: `CNO.agda`, `OND.agda`, `EchoBridgeScaffold.agda`, `EchoBridgeCNO.agda` type-check; every file carries the `{-# OPTIONS --safe --without-K #-}` pragma and CI (`proofs.yml`) checks all four. Until 2026-09-23 CI checked only the first two and `EchoBridgeCNO.agda` had no pragma of its own. The EchoBridge modules take **funext as an explicit hypothesis** (not a global `postulate`); `OND.agda` uses zero postulates. == Lean 4 — VERIFIED (this environment) * Toolchain `leanprover/lean4:v4.16.0` with Mathlib `@ v4.16.0`; `lake exe cache get` + `lake build` → **build completed successfully**. Covers the CNO libraries and the new `OND` library (`proofs/lean4/OND.lean`, core-Lean only, zero `sorry`). * **Mathlib-free core is CI-gated (2026-09-22):** `proofs/lean4/check-core.sh` (job `lean` in `.github/workflows/proofs.yml`; toolchain from `lean-toolchain`, elan fetched as a checksum-verified tarball, zero third-party actions) compiles `CNO`, `OND`, `CNOCategory`, `CNOBridge`, `FilesystemCNO`, `LambdaCNO` with plain `lean` and runs `proofs/lean4/AxiomAudit.lean`: 96 `#guard_msgs` pinning every axiom signature, the three occupancy predicates in full, the #125 derivations as negative controls, and `#print axioms` for every theorem (no `sorryAx` anywhere). `just verify-lean-core` runs the same script locally. * **Issue #125 fixed — the Lean axioms no longer derive `False`:** `FilesystemCNO.lean` stated `mkdir_rmdir_inverse`, `create_unlink_inverse` and `rename_inverse` without the occupancy preconditions of the Coq lemmas they mirror; with `mkdir_idempotent` and `mkdir_not_identity` that proved `False`. They now carry `noDirAt` / `noFileAt` / `noEntryAt`, mirrored verbatim from `proofs/coq/filesystem/FilesystemCNO.v`, and the unconditional statement is refuted in-file (`unconditional_mkdir_rmdir_inverse_is_false`). `LambdaCNO.lean` carried the unrestricted `eta_equivalence` axiom (false as stated, the same `LVar 5` counterexample the Coq side documents above); it is now the proved `noLambda`-guarded theorem, `subst_closed_term` is proved, and the unrestricted claim is refuted (`unrestricted_eta_equivalence_is_false`). Lean axiom count: `FilesystemCNO` 21 → 21 (same names, three strengthened), `LambdaCNO` 3 → 1 (`y_combinator_not_identity`, the Lean twin of Coq's class-A `y_not_cno`). * **#167 port reverted pending completion (issue #176):** #174 attempted to port `FilesystemCNO.lean`'s 21 axioms to concrete definitions and proved theorems, but the port did not compile in the six-module job (unresolved `Directory`/`Symlink` alternatives, unknown identifiers, failed rewrites). Per #176's ruling, a half-port must not sit red on `main`: `FilesystemCNO.lean` and its paired `AxiomAudit.lean` guards are restored here to the revision above (their last state that compiled, identical to the pre-#174 commit and to the last green `main` run before #174). #167 stays open with finishing the port as its own acceptance criterion. == Z3 — VERIFIED (this environment) * `z3` 4.16.0 on `proofs/z3/ond/OND_checks.smt2`: the OND-3 timing-leak witness is `sat`, `writer`-is-OND is `unsat` (no secret distinguishes it), and the OND-5 composite leak is `sat` with a concrete model — the "decidable for bounded programs" demonstration. == Isabelle/HOL — VERIFIED (this environment) * `Isabelle2025-2`, session `AbsoluteZero-CNO` (`proofs/isabelle/ROOT`): `CNO.thy` (repaired — the reserved-keyword `value` type was renamed and the failing `nop`/`step` lemmas fixed) and `OND.thy` (new, OND-1..5) build with no `sorry`/`oops`. == Mizar — VERIFIED (this environment) * Mizar `8.1.15`; `accom CNO && verifier CNO` on `proofs/mizar/CNO.miz` completes with an **empty `CNO.err`** (zero errors). `MIZFILES` points at the bundled MML. The original article was machine-generated and unverifiable (277 errors); it was *rewritten* into a genuine article (StateSpace = pair of `Funcs(NAT,NAT)`; state-preserving / pure / reversible / terminating / thermo-reversible attributes; 12 proved theorems incl. composition with a real inverse construction). Requires the committed private vocabulary `proofs/mizar/dict/cno.voc` (lowercase filename, needed on Linux). Verifier build artifacts are git-ignored. == Idris 2 — VERIFIED (this environment), the ABI boundary * `idris2` 0.8.0; `idris2 --build absolute-zero-abi.ipkg` → clean, no warnings. The packaging bug (module paths vs. `sourcedir`) is fixed, files relocated to match module names, and six latent type errors repaired (null-pointer `So` witnesses via `choose`, `Decidable.Equality`/`Data.Bits` imports, `%runElab` stub, erased `HasSize` index, qualified `maxProgramLength`). Two unused, non-compiling `DecEq` instances were removed with a documented recovery path. == Honest scope * Multi-prover, not cross-prover *equivalence* — each prover checks its own formalisation of the two pillars. * "Verified here" = a reproduced compiler/checker run in this environment, not a reading of in-file comments. Reproduce everything with `proofs/verify-all-provers.sh`. * Axiom census (machine-generated via `proofs/coq/census-assumptions.sh`): of 182 top-level theorems across the 14 theories, exactly **109 are closed under the global context** (zero axioms), and 73 rest on Coq stdlib classical axioms (`ClassicalDedekindReals.*`, `FunctionalExtensionality.*`, `Classical_Prop.classic`, `ProofIrrelevance.*`) and/or the tagged project parameters. Each theory's logical root is read from `_CoqProject`'s own `-R ` bindings rather than hardcoded (issue #176: the census previously assumed every theory lived under `CNO.`, which is false for `malbolge/` — bound to `Malbolge` — and made the generated driver fail outright instead of censusing it; the table now shows `Malbolge.MalbolgeCore | 7 | 7 | 0`). A directory with no `-R` binding is a hard census failure, never a silent skip. * All top-level declarations are verified by `proofs/coq/check-axiom-tags.sh` to carry a unified tag grammar: `(* AXIOM: [METAL-BOUNDARY] ... *)` for physical constants and laws, or `(* AXIOM: [CLASS-A] ... *)` for provable-in-principle mathematics. The two former unsound declarations in `StatMechBasis.v` (`prob_nonneg` and `prob_normalized`, which claimed Kolmogorov properties over raw unconstrained functions `ProgramState -> R`) have been deleted; zero theorems depend on either. * The 17 named headline theorems remain 100% closed under the global context (zero axioms, CI-gated by `check-assumptions.sh`).