EXPLAINME.adoc

Absolute Zero — EXPLAINME

This file backs every factual claim in README.adoc with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code.

Important

Archive notice (2026-10-10, reconciled 2026-11-01). The active proof stack is Agda (proofs/agda/, --safe --without-K, zero postulates) + Z3 as a bounded-check solver + the Idris 2 ABI. Coq, Lean 4, Isabelle/HOL and Mizar now live under archive/proofs/; paths below of the form proofs/coq/… / proofs/lean4/… refer to the archived trees (archive/proofs/coq/… etc.), and counts such as "115 Qed / 61 Axioms" are historical figures of those archived trees. The canonical active-vs-archived proof-status table is PROOF-STATUS.adoc, which also records the estate proof grades (mathesis estate-mathematical-architecture §5) and the closed ledger vocabulary of hyperpolymath/standards (proven / proven-with-postulates / tested-only / argued / open): the active Agda proofs are proven at Grade 3 (local strict-flag check, no independent-foundation translation), the Z3 bounded checks are tested-only, and OND-6 is open.

Contents

• Claim-to-implementation map
  • CNO and OND are logically independent
  • OND-1..5 are proved with zero axioms
  • Coq CNO: 115 Qed, 0 Admitted, 61 Axioms
  • Multi-prover verification across six systems
  • Thermodynamic reversibility follows from Landauer’s principle
  • CNO verification is undecidable in general
• Dogfooded Across The Account
• Known gaps
• Evidence Index

Claim-to-implementation map

CNO and OND are logically independent

The two pillars are logically independent (a proved theorem, with witnesses).

— README.adoc

How this was implemented

The independence theorem was proved in Coq (archive/proofs/coq/ond/OND.v, anchored to the core is_CNO definition, with witnesses that CNO does not entail OND and OND does not entail CNO); the active Agda OND.agda carries the same obligation zero-postulate.

Caveat

None currently known for the independence proof itself. However, the coupling dial between them (connecting a thing to the trace it casts) is explicitly framing, not theorem.

OND-1..5 are proved with zero axioms

_OND obligations OND-1..5 are proved with zero postulates in Agda (proofs/agda/OND.agda, --safe --without-K)_

— README.adoc (active stack)

How this is implemented

proofs/agda/OND.agda contains the active proofs; CI (proofs.yml, agda job) type-checks all four Agda modules under --safe --without-K. The historical Coq proof (archive/proofs/coq/ond/OND.v, every theorem Closed under the global context) and the Lean 4 mirror are archived; Z3 confirms the bounded instances (proofs/z3/ond/OND_checks.smt2, expect-annotated).

Caveat

OND proofs are axiom-free relative to the declared observation model O. The choice of O is a proof input, not a proof output. If O omits a real-world observable channel (e.g., power analysis), the OND proof is sound but physically incomplete. The residue list in proofs/residue/ records this gap.

Coq CNO: 115 Qed, 0 Admitted, 61 Axioms

_115 Qed / 0 Admitted / 61 Axioms across 13 files — every theorem is discharged (no Admitted), but the development rests on 61 Coq + 52 Lean axioms._

— README.adoc

How this is implemented

proofs/coq/ contains all CNO theories. CI runs coq_makefile and confirms Qed counts and axiom counts. The axioms are domain-specific assumptions (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws) that are assumed but not derived within Coq.

Caveat

This is not an axiom-free machine-checked proof. "Machine-checked" here means the proof is valid assuming the axioms hold. If an axiom is false in the intended model, the theorem fails. The 61 Coq + 52 Lean axioms represent the proof debt. Discharging them (especially quantum unitarity and filesystem inverse laws) is the next major obligation.

Multi-prover verification across six systems

_Verify CNO properties in six independent proof systems._

— README.adoc

How this is implemented

Artefacts exist for Coq, Lean 4, Agda, Z3, Isabelle, and Mizar in proofs/. proofs/verify-all-provers.sh orchestrates verification. CI gates Coq, Lean 4, and Agda.

Caveat

Z3, Isabelle, and Mizar are generated but not yet run in CI. The artefacts exist but are not evidence until machine-executed and green. The "six prover" claim describes the target architecture, not the current CI gate.

Thermodynamic reversibility follows from Landauer’s principle

_ThermodynamicallyReversible(p) — Zero energy_

— README.adoc

How this is implemented

proofs/coq/physics/StatMech.v and proofs/lean4/StatMech.lean formalise Landauer’s principle and Bennett’s reversible computing, proving CNOs dissipate zero energy because they erase no information.

Caveat

The physics formalisation relies on axioms about the physical model (e.g., that the thermodynamic system satisfies the assumptions of Landauer’s principle). This is standard for formalisations of physics, but the gap between the mathematical model and physical metal is real.

CNO verification is undecidable in general

_The problem "Is program p a CNO?" is undecidable in general._

— README.adoc

How this is implemented

Proved by reduction from the halting problem. Constructive witness: the ability to decide CNO-ness would decide halting.

Caveat

This is a standard result. The practical consequence is that the verified CNOs in this repo are specific programs or finite-state classes, not arbitrary input programs.

Dogfooded Across The Account

Technology / Pattern	Used here	Also used in
Coq CNO/OND formalisation	proofs/coq/	echo-types (EchoBridgeCNO)
Multi-prover pattern	Six provers + Idris ABI	Kategoria (Route δ)
OND residue-list honesty	proofs/residue/	epistemic-types (proof transport)

Known gaps

Caution

61 Coq + 52 Lean axioms are unproven — in the ARCHIVED stack. The archived CNO development (archive/proofs/) was machine-checked relative to these axioms (quantum-gate unitarity, complex-analysis identities, Shannon-entropy non-negativity, filesystem inverse laws). These are historical counts of the archived trees, not active proof status and not estate-wide ground truth. The active Agda stack is zero-postulate.

Caution

Coq, Lean 4, Isabelle/HOL and Mizar artefacts are archived and not run. archive/proofs/ is not built or gated. The active machine-checked evidence is Agda (proofs/agda/), Z3 bounded checks (proofs/z3/), and the Idris 2 ABI build — via proofs/verify-active-provers.sh.

Caution

OND-6 (conditional composition) is OPEN — not proved, not assumed. OND-1..5 are proved (zero postulates, active Agda). The capstone composition theorem remains the deliberate research fork; no Admitted or postulate stands in for it anywhere in the active stack.

Caution

OND proofs are conditional on declared O. An OND certificate is valid only for the observables in O. Out-of-scope channels (timing, power, cache, EM radiation) are listed in the residue, not blocked by the proof.

Caution

CNO↔OND coupling dial is framing, not theorem. The connection between a thing and the trace it casts to an observer is a conceptual bridge, not a formal result.

Evidence Index

Path	Proves
proofs/agda/ (CNO, OND, EchoBridge)	ACTIVE: both pillars, OND-1..5, zero postulates (--safe --without-K)
proofs/z3/ + proofs/verify-active-provers.sh	ACTIVE: bounded expect-checked instances; one-shot active gate
archive/proofs/coq/common/CNO.v	ARCHIVED: core CNO framework (historical 115 Qed, 61 Axioms)
archive/proofs/coq/ond/OND.v	ARCHIVED: OND-1..5 (zero axioms)
archive/proofs/coq/physics/StatMech.v	ARCHIVED: Landauer’s principle, thermodynamic reversibility
archive/proofs/coq/category/CNOCategory.v	ARCHIVED: universal CNO definition, model independence
archive/proofs/lean4/	ARCHIVED: Lean 4 mirrors (historical Phases 1–4, 52 Axioms)
proofs/observation-models/	Declared O inputs for OND
proofs/residue/	OND residue lists (out-of-scope observables)