UniversalTM
UniversalTM is a structure that pairs a base Turing machine with a universal flag set to true, encoding a simulator able to run any other machine on any input. Researchers deriving the Church-Turing thesis from Recognition Science ledger rules would cite it when grounding universal computation in physical 8-tick updates. The declaration is introduced by direct reference to Turing's 1936 explicit construction of small machines with 2 states and 18 symbols or 7 states and 4 symbols.
claimA universal Turing machine is a structure consisting of a base Turing machine $T$ (with positive number of states and alphabet size) together with a Boolean flag indicating that $T$ can simulate the computation of any other Turing machine on any input tape.
background
The Information.ChurchTuring module derives the Church-Turing thesis from Recognition Science ledger universality: the ledger simulates any physical process, every computation is a sequence of ledger updates, and the 8-tick structure supplies a universal gate set. TuringMachine is the sibling structure requiring numStates > 0 and alphabetSize > 0. Upstream constants include the active-edge count A (equal to 1) from IntegrationGap and Masses.Anchor, which enforces the phi-power balance identity at D = 3.
proof idea
The declaration is a plain structure definition with a defaulted universal field. The attached comment states existence by explicit construction from Turing 1936 and lists the minimal state-symbol counts for known small UTMs. No lemmas or tactics are invoked; the entry functions as a named wrapper around the classical result.
why it matters in Recognition Science
UniversalTM supplies the formal object needed to state the Church-Turing thesis inside the Recognition Science ledger framework, directly supporting the paper proposition on the physical basis of universal computation. It rests on the eight-tick octave (T7) that furnishes the universal gate set and on the general ledger simulation principle. No downstream theorems yet consume it, leaving open its precise linkage to the phi-ladder mass formula or the J-uniqueness forcing chain.
scope and limits
- Does not encode the simulation function or transition table inside the structure.
- Does not prove the Church-Turing thesis; only posits the UTM object.
- Does not specify tape contents or halting behavior.
- Does not connect the universal flag to J-cost or defectDist.
- Does not derive the 8-tick gate set from first principles.
formal statement (Lean)
75structure UniversalTM where
76 base : TuringMachine
77 /-- Can simulate any other TM -/
78 universal : Bool := true
proof body
Definition body.
79
80/-- **THEOREM**: A UTM exists.
81
82 Proof: Construct explicit UTM (Turing 1936).
83 Small UTM: (2 states, 18 symbols) or (7 states, 4 symbols). -/