Skip to content

PROOF-STATUS.adoc

Latest commit

 

History

History
206 lines (171 loc) · 11.3 KB

PROOF-STATUS.adoc

File metadata and controls

206 lines (171 loc) · 11.3 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

All six provers are installed and were reproduced in this environment. A single gate, proofs/verify-all-provers.sh, builds every prover and prints ALL-PROVERS-GREEN: Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar, plus the Idris 2 ABI. Both the CNO and OND pillars are covered.

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.

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 every headline theorem shows only Coq stdlib axioms (ClassicalDedekindReals., functional_extensionality) plus, where relevant, the explicitly-tagged postulate above — never a hidden project axiom.

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, --safe --without-K: CNO.agda, OND.agda, EchoBridgeCNO.agda type-check. 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).

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.

  • Remaining axioms are exactly: (a) tagged physical postulates (the honest metal boundary), and (b) the class-A items listed above (true, provable in principle, openly labelled). No headline theorem depends on a hidden project axiom.