Glossary

Glossary

Term	Definition
CNO	Certified Null Operation. A program that compiles + runs and is formally proven to have zero net computational effect — no state change, no I/O, no entropy.
Identity morphism	In category theory, the morphism id_X : X → X that leaves X unchanged. CNOs are identity morphisms in the category of computational states (ADR-001).
Observational reversibility (=st=)	The weakened reversibility property used after ADR-008. State equality modulo program-counter bookkeeping; PC is not observable, so two states with different PC but same observable content are =st=.
Landauer bound	Lower thermodynamic cost of erasing one bit (kT ln 2). CNOs erase nothing, so any logically-reversible CNO can in principle be thermodynamically reversible too. Formalised in StatMech.v (axiom) + derived in LandauerDerivation.v (ADR-002).
Postulate / Axiom	Asserted, unproven proposition. In Coq: Axiom. In Lean: axiom. In Idris2 0.8.0: name = believe_me () (the postulate keyword was removed). Every estate-wide axiom is tracked in AUDIT.adoc or descriptiles/META.a2ml.
HasAlignment t n	Idris2 type asserting that type t has byte alignment n. The constructor AlignProof is information-free — the obligation sits on the producer to construct it only for the genuinely-correct n.
alignedSize	(size, align) ↦ smallest multiple of align that is ≥ size. Core ABI primitive; correctness proved (via believe_me, pending discharge) in Proofs.DivMod.
BoJ	Brain of Jonathan — the estate's cross-repo automation cartridge layer. ECHIDNA invocations route through echidna-llm-mcp BoJ.
ECHIDNA	Estate-wide neurosymbolic prover gateway. 105 prover backends, 66,674-proof corpus, ML tactic suggestion. Lives in a separate repo; called via BoJ.
PMPL-1.0	Palimpsest-MPL 1.0. Former project licence (see the archived licence audit); the project licence is MPL-2.0 — see LICENSE.
RSR	Rhodium Standard Repository — the estate-wide taxonomy convention defined by hyperpolymath/rsr-template-repo. Conformance tracked in RSR_COMPLIANCE.adoc.
ADR	Architectural Decision Record. Forward-looking design choice. Recorded in descriptiles/META.a2ml.
AUDIT-ID	Backward-looking trust event (discharged axiom, deleted unsound code, license correction). Format AUDIT-YYYY-MM-DD-<seq-or-PR>. Recorded in AUDIT.adoc.
descriptiles	The .a2ml machine-readable format under .machine_readable/descriptiles/. Successor to the older .scm (Guile Scheme) format; the side-by-side .scm set was removed by the estate standardization (2026-06).
Trust escape	An axiom or believe_me use that lets you bypass the type system. Hunted by the estate-wide cross-trust-escape sweep.