Proof Systems

Proof Systems

Why six?

Each prover trades off three axes:

	Constructive	Automated	Mathlib
Coq	✅	⚪	⚪
Lean 4	✅	⚪	✅
Agda	✅	⚪	⚪
Isabelle	⚪	⚪	✅
Mizar	⚪	⚪	✅
Z3	⚪	✅	⚪

A property proved in all six is robust against any single backend's foundational quirks. A property proved in some but not others flags a foundational dependency worth understanding.

What lives where

proofs/coq/ (the load-bearing system)

• common/CNO.v — core CNO definitions and properties
• physics/StatMech.v — Landauer bound axiomatised
• physics/LandauerDerivation.v — Landauer bound derived (the two together form ADR-002's "dual formalisation")
• category/CNOCategory.v — CNOs as identity morphisms
• lambda/LambdaCNO.v — lambda calculus CNOs
• quantum/QuantumCNO.v — quantum CNOs
• quantum/QuantumMechanicsExact.v — exact QM formulation
• malbolge/MalbolgeCore.v — Malbolge VM semantics
• filesystem/FilesystemCNO.v — filesystem CNOs

Status (PR #100, 2026-07-06): 14/14 theories compile, 0 Admitted, now including ond/OND.v (the OND pillar, OND-1..5, zero axioms). CNO axioms cut 98→small classified remainder: filesystem/category/QuantumMechanicsExact fully discharged; genuine physical postulates kept as tagged METAL-BOUNDARY; a few class-A items openly labelled; three unsound axioms removed/corrected. See PROOF-STATUS.adoc and docs/PROOF-CLASSIFICATION.adoc.

proofs/lean4/

• CNO.lean, StatMech.lean, CNOCategory.lean, LambdaCNO.lean, QuantumCNO.lean, FilesystemCNO.lean
• Built with lake build; mathlib + 6 lean_lib targets; 1631/1632 green (verified 2026-05-20).

proofs/z3/

SMT proofs of decidable fragments. Fast counterexample search for candidate CNO claims before committing to a constructive proof.

proofs/agda/

Type-level CNO certificates exploiting dependent types.

proofs/isabelle/, proofs/mizar/

Cross-validation. Catches Coq-specific tactic quirks; connects Mizar's standard maths library.

Reproducible build

just build-coq      # coqc -R common CNO physics/StatMech.v ...
just build-lean     # cd proofs/lean4 && lake build
just build-agda     # agda CNO.agda
just build-isabelle # isabelle build
just build-z3       # z3 *.smt2 (when present)
just verify         # all of the above + ABI + Rust

Discharged axioms (recent)

• ADR-007 (2026-05-20, PR #24): eval_deterministic Axiom → Theorem via step_deterministic_strong
• ADR-008 (2026-05-20, PR #32): deleted unsound eval_respects_state_eq_{left,right} axioms; weakened logically_reversible to observational reversibility (=st=)
• ADR-009 (2026-05-25, PR #41 / #40): deleted unsound Idris2 alignmentMatchesPlatformWord postulate; consolidated div/mod axioms into shared AbsoluteZero.ABI.Proofs.DivMod

See Audit Trail for the full ledger.

Idris2 ABI (the seventh)

The Idris2 surface in src/abi/ isn't a proof system per se, but carries formal alignment + size proofs for the C FFI boundary. See ABI.