UniversalTM
plain-language theorem explainer
A Universal Turing Machine is a Turing machine equipped with a flag asserting it can simulate every other TM: given a description of T and an input x, it computes T(x). Anyone formalizing programmable computation or the Church–Turing thesis in this module cites this carrier type. It is a plain structure definition with a defaulted Boolean field, not a proved existence claim.
Claim. A universal Turing machine is a pair consisting of a Turing machine $M$ (with positive state count and alphabet size) together with a Boolean mark that $M$ can simulate every other Turing machine: on input $\langle T, x\rangle$ it computes $T(x)$.
background
The module aims to derive the Church–Turing thesis from Recognition Science ledger universality: any effectively computable process is a sequence of ledger updates, and the eight-tick structure supplies a universal gate set. The classical thesis equates Turing machines, lambda calculus, recursive functions, and register machines in computational power; it remains a thesis because “effectively computable” is informal.
The base type is a Turing machine configuration: a positive number of states and a positive tape alphabet size. Universality is the classical property that one fixed machine, given an encoding of any other machine $T$ and an input $x$, reproduces $T(x)$. That property is the foundation of programmable computers and is the object this structure packages for later RS arguments about ledger simulation.
proof idea
No proof: this is a structure definition. It packages a TuringMachine field base and a Boolean field universal defaulting to true, documenting the simulation capability. Existence of such a machine is deferred to the sibling claim that constructs an explicit UTM (classical small machines such as 2 states/18 symbols or 7 states/4 symbols).
why it matters
This carrier sits at the start of the INFO-009 line that links ledger universality to the Church–Turing thesis. Downstream siblings (existence of a UTM, ledger computers that follow the eight-tick cadence, a universal gate set on eight ticks, and the physical CT thesis) are meant to treat computation as ledger updates rather than an external axiom. In the RS primer the eight-tick octave (T7) is the natural discrete clock; the module claims that clock yields a universal gate set, so programmable simulation is forced by the same forcing chain that fixes period $2^3$. The structure itself does not prove universality or the thesis; it only names the classical UTM object so those later statements have a typed subject. No used_by edges are recorded yet, so its framework role is still prospective scaffolding for the paper target “Physical Basis of Universal Computation.”
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.