Expand glossary with CNO, OND concepts and more (#133)

Added glossary entries for CNO and OND concepts, proof engineering, and
pronunciation guide.

<!--
SPDX-License-Identifier: CC-BY-SA-4.0
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
## Summary

<!-- What does this PR do, and why? -->

Closes #

## Type of change

- [ ] 🐛 Bug fix (non-breaking change that fixes an issue)
- [ ] ✨ New feature (non-breaking change that adds functionality)
- [ ] 💥 Breaking change (would change existing behaviour)
- [ ] 🕳️ Soundness fix (fixes a checker/proof false-negative)
- [ ] 📖 Documentation
- [ ] 🧹 Refactor / tech debt (behaviour-preserving)
- [ ] ⚡ Performance
- [ ] 🔧 Build / CI / tooling

## How has this been verified?

<!-- Establish ground truth: which tool did you RUN, and what did it
report?
     Don't cite a status doc — cite the command and its output. -->

## Checklist

- [ ] My commits are **signed** (`git commit -S`).
- [ ] I ran the project's own checks/tests locally and they pass.
- [ ] New files carry the correct `SPDX-License-Identifier` (code/config
`MPL-2.0`,
      prose `CC-BY-SA-4.0`); I did not relicense existing files.
- [ ] Docs are updated, and no public claim now overstates what the code
does.
- [ ] I have not introduced a soundness hole (or I have flagged where I
might have).

## Notes for reviewers

<!-- Anything that needs special attention, follow-up, or context. -->

Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>

Author: hyperpolymath

GLOSSARY.adoc

@@ -0,0 +1,87 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Absolute Zero — Glossary
+:toc: preamble
+:toc-title: Contents
+:icons: font
+:doctype: article
+
+Cross-reference glossary for link:README.adoc[README.adoc], link:EXPLAINME.adoc[EXPLAINME.adoc], and the `absolute-zero` wiki.
+
+== The two pillars
+
+[[cno]]
+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]]
+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]]
+Coupling dial::
+  The conceptual connection between CNO (a thing) and OND (the trace it casts). Framing, not theorem.
+  *Classification:* **project-specific** (vocabulary).
+
+== CNO concepts
+
+[[is-cno]]
+IsCNO(p)::
+  The core predicate: `Terminates(p, σ) ∧ FinalState(p, σ) = σ ∧ NoSideEffects(p) ∧ ThermodynamicallyReversible(p)`.
+  *Classification:* **project-specific** (formalisation).
+
+[[landauer-principle]]
+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]]
+Reversible computing::
+  Computation that can be undone with zero energy cost (Bennett 1973). A required field of `IsCNO`.
+  *Classification:* **standard** (Bennett 1973).
+
+== OND concepts
+
+[[observation-model]]
+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]]
+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]]
+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).
+
+== Proof engineering
+
+[[axiom-vs-qed]]
+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]]
+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).
+
+== Pronunciation guide
+
+[cols="1,2", options="header"]
+|===
+| Written | Spoken
+
+| CNO
+| "see-en-oh"
+
+| OND
+| "oh-en-dee"
+
+| IsCNO
+| "is-see-en-oh"
+|===