UniversalTM
plain-language theorem explainer
UniversalTM packages a Turing machine with a boolean flag that asserts the machine can simulate any other TM. Researchers deriving the Church-Turing thesis from ledger universality in Recognition Science cite this structure when reducing computations to sequences of ledger updates. The definition is a direct structure declaration that defaults the universality flag to true.
Claim. A universal Turing machine consists of a Turing machine $M$ (with positive number of states and alphabet size) together with a boolean flag set to true asserting that $M$ can simulate any other Turing machine on any input.
background
The Information.ChurchTuring module derives the Church-Turing thesis from Recognition Science by showing that ledger universality follows from the eight-tick structure, which supplies a universal gate set for any physical process. A TuringMachine is the sibling structure recording numStates : ℕ and alphabetSize : ℕ together with the two positivity conditions. Upstream results supply the active-edge count A (equal to 1) from IntegrationGap, Masses.Anchor, and Modal.Actualization; these fix the per-tick mechanics that the ledger updates rely on.
proof idea
The declaration is a structure definition that directly encodes the universal property as a defaulted boolean field on top of the TuringMachine base.
why it matters
This supplies the computational object required for the physical Church-Turing thesis (physical_ct_thesis in the same module), which rests on the eight-tick octave (T7) providing universal gates. It therefore bridges the abstract Turing model to the Recognition Science ledger without invoking external computation models. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.