Runtime Semantics, State Machines, Recorders, and an Executable Reference Model

Converts the theory of Papers 00–07 into a first-version, implementable runtime specification. Defines the machine state (native graph, state map, certificate recorder, debt recorder, frontier, cut sets, obstruction cover, exhaustion, policy, ledger head, version); every theorem-level mutation must go through an atomic transaction. Fixes a three-tier runtime: L0, a canonical append-only event ledger (the source of truth); L1, the natively materialized closure state (must be reconstructible by replay); and L2, purpose-specific views (whose authority never exceeds L1’s). Core safety principle: no certificate path ⇒ no native theorem mutation. States explicitly that the runtime is implementation-agnostic — it makes no difference whether it is realized as an LLM, a theorem prover, a GUI, a web service, or a distributed database; what matters is deterministic semantics, the recorders, the ledger, PCOs, transactions, replay, querying, and consistency testing.