Absolute Zero — Glossary

Cross-reference glossary for README.adoc, EXPLAINME.adoc, and the absolute-zero wiki.

Contents

The two pillars

CNO (Certified Null Effect): A program that does nothing to the world: terminates, maps input state to identical output state, is pure, and is thermodynamically reversible. The conserved quantity is state. Classification: novel assembly (standard concepts combined; the intended notion has four parts, while the active Agda IsCNO record has two fields, see [is-cno]).

OND (Observational Null Disclosure): A program that reveals nothing about its secret input to a declared observer: its observable trace is constant over the secret, relative to a declared observation model O. The conserved quantity is the secret-to-observable channel. Classification: novel formalisation.

Coupling dial: The conceptual connection between CNO (a thing) and OND (the trace it casts). Framing, not theorem. Classification: project-specific (vocabulary).

IsCNO(p): The core predicate. Intended notion: Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p). Active Agda (proofs/agda/CNO.agda): from every state the pc-driven machine stops normally (cno-terminates), and every normal stop is obs-eq to the start (cno-identity). Purity and observational reversibility are derived; no thermodynamic claim is made. Classification: project-specific (formalisation).

Landauer’s principle: Erasing one bit of information dissipates at least kT ln 2 of energy. A CNO erases no information, hence dissipates zero energy. Classification: standard (Landauer 1961).

Reversible computing: Computation that can be undone with zero energy cost (Bennett 1973). Part of the intended CNO notion; the active Agda proves only observational reversibility (cno-left-inverse), not an energy bound. Classification: standard (Bennett 1973).

Observation model (O): The declared set of observables (timing, size, output) that an OND proof reasons about. An OND certificate is valid only relative to O. Classification: project-specific.

Residue list: The explicit list of out-of-scope observables shipped with every OND claim. The honest boundary between the proof and the physical metal. Classification: project-specific.

OND-6 (conditional composition): The open research capstone: composing OND-certified operations under conditions. OND-1..5 are proved; OND-6 is deferred. Classification: project-specific (open problem).

Axiom vs. Qed: In this repo, "Qed" means the proof is discharged in the prover. "Axiom" means an unproven assumption is introduced. A theorem with 0 Admitted but 61 Axioms is machine-checked relative to those axioms, not axiom-free. Classification: standard (proof engineering terminology).

Multi-prover cross-validation: Verifying the same mathematical claim in independent proof systems (Coq, Lean, Agda, Z3, Isabelle, Mizar) to increase confidence. Classification: standard (methodology).