Skip to content

PROOF-STATUS.adoc

Latest commit

 

History

History
500 lines (432 loc) · 32 KB

PROOF-STATUS.adoc

File metadata and controls

500 lines (432 loc) · 32 KB
Raw

absolute-zero — Proof Status

Table of Contents
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 (now archived as archive/proofs/verify-all-provers.six-prover.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. The six-prover self-test (now archive/proofs/tests/gate-selftest.six-prover.sh) proved 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. 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.

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)

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 4.16.0, Z3-CHECK OK, sat/unsat/sat). The 2026-11-09 OND-3 rewrite expects 5 verdicts, sat/unsat/sat/sat/sat, observed with z3 4.8.12 — 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

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.

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 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, 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.

Reproduction receipts (this environment, 2026-11-09)

Working tree on branch claude/ephapax-architecture-plan-gzyctr over cbe9ae9.

  • Z3 — REPRODUCED HERE. Z3 version 4.8.12 - 64 bit, on the rewritten OND-3 check. z3 proofs/z3/ond/OND_checks.smt2 prints sat unsat sat sat sat (+ the OND-5 model s1 = 2, s2 = 3, pub = 0), exit 0; bash proofs/z3/verify.sh → ok: ond/OND_checks.smt2 — 5 (check-sat) verdict(s) match, Z3-CHECK OK, exit 0. Mutation check: replacing writer_step by a step that copies the secret to the output cell turns the OND-3 dir 2 verdict from unsat to sat, so the check is no longer vacuous (see the Z3 section).

  • Agda — REPRODUCED HERE, on the CNO.agda before #199 (so not a receipt for the current module). Agda version 2.6.3, stdlib registered by scripts/provision-agda-stdlib.sh (agda-stdlib v1.7.3 = 0817da6877aa045932221134913d8511caa78d97, into a scratch AGDA_DIR). agda --safe --without-K on CNO.agda, OND.agda, EchoBridgeScaffold.agda, EchoBridgeCNO.agda: exit 0 each. agda --safe --without-K --cubical-compatible on the same four: exit 0 each. (The stdlib modules themselves were checked under the stdlib’s own pragmas, not re-checked under --cubical-compatible.)

  • Gate self-test. bash proofs/tests/gate-selftest.sh → GATE-SELFTEST OK: 27/27 cases.

  • Idris 2 — not run here.

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, 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 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 — ARCHIVED (historical receipt, 2026-07-07; not built or gated since 2026-10-10)

  • 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 (historical; the tree is archived): cd archive/proofs/coq && coq_makefile -f _CoqProject -o Makefile.all && make -f Makefile.all -j.

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 WAS CI-gated until the 2026-10-10 archive ruling (no longer run): archive/proofs/coq/audit/Assumptions.v lists the 17 and archive/proofs/coq/check-assumptions.sh (formerly the Coq job of proofs.yml, and the then-canonical proofs/verify-all-provers.sh gate, now archive/proofs/verify-all-provers.six-prover.sh) failed 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)

archive/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 — archive/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 — the disclosure pillar (Coq/Lean legs ARCHIVED; Agda + Z3 legs active)

archive/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 (archive/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.

  • Standard library: agda-stdlib v1.7.3 (commit 0817da6), registered by scripts/provision-agda-stdlib.sh (just provision-agda-stdlib) — the same script the CI agda job runs; it fails if the tag no longer resolves to the pinned commit. Set AGDA_DIR to keep it out of ~/.agda.

Lean 4 — ARCHIVED (historical receipt; not built or gated since 2026-10-10)

  • 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 (archive/proofs/lean4/OND.lean, core-Lean only, zero sorry).

  • Mathlib-free core WAS CI-gated (2026-09-22 until the 2026-10-10 archive ruling; the lean job no longer exists): archive/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 archive/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 archive/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 — ACTIVE, bounded checks (tested-only)

  • Historical (2026-07-07): z3 4.16.0 on proofs/z3/ond/OND_checks.smt2: the OND-3 timing-leak witness is sat, writer-is-OND is unsat, and the OND-5 composite leak is sat with a concrete model. Correction (2026-11-09): the writer-is-OND block then asserted (not (and (= 0 0) (= 1 1))) — the writer’s observables written down as constants — which is unsat for any program, so that unsat checked nothing about the writer.

  • Current (2026-11-09, z3 4.8.12, 5 verdicts sat unsat sat sat sat): the OND-3 dir 2 block now models writer_op per archive/proofs/coq/ond/OND.v: memory as (Array Int Int), inj s p, writer_step m = store m 0 7, writer_time = 1, and the O_all observable (output cell 2, time) computed from them; asserting the observables differ for two secrets at the same public input is unsat (writer is OND under O_all). A control block runs the same query on a writer that copies the secret to the output cell (sat), and a third block witnesses writer_not_null (sat). Mutating writer_step to leak flips the main verdict to sat.

  • Remaining scope limit: the OND-3 dir 1 block (time_leaky secret = secret) and the OND-5 block (p_out = 0, comp_out = secret) still state the observables directly rather than computing them from step functions; they are hand transcriptions of the OND.v results, not independent checks of the composition.

Isabelle/HOL — ARCHIVED (historical receipt; not built or gated since 2026-10-10)

  • Isabelle2025-2, session AbsoluteZero-CNO (archive/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 — ARCHIVED (historical receipt; not built or gated since 2026-10-10)

  • Mizar 8.1.15; accom CNO && verifier CNO on archive/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 archive/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 the active stack with proofs/verify-active-provers.sh (after scripts/provision-agda-stdlib.sh); the former six-prover gate is archived as archive/proofs/verify-all-provers.six-prover.sh and is not run.

  • The Coq census and tag-grammar bullets below describe the archived tree (archive/proofs/coq/); their scripts are no longer run.

  • Axiom census (machine-generated via archive/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 <dir> <Root> 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 archive/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, formerly CI-gated by archive/proofs/coq/check-assumptions.sh; not run since the 2026-10-10 archive ruling).