Cross-reference glossary for README.adoc, EXPLAINME.adoc, and the absolute-zero wiki.
- 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 into this specific 4-field record).
- 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:
Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p). Classification: project-specific (formalisation).
- Landauer’s principle
-
Erasing one bit of information dissipates at least
kT ln 2of 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). A required field of
IsCNO. 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).