Skip to content

PROOF-STATUS.adoc

Latest commit

 

History

History
267 lines (232 loc) · 16.1 KB

PROOF-STATUS.adoc

File metadata and controls

267 lines (232 loc) · 16.1 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. 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).

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