TuringMachine
plain-language theorem explainer
Structure declaring a Turing machine via positive integers for state count and alphabet size. Researchers formalizing computation from Recognition Science ledger updates cite this when constructing universal simulators. As a definition it introduces the type with no proof obligations.
Claim. A Turing machine consists of a positive natural number of states $Q > 0$ and a positive natural number alphabet size $S > 0$.
background
The Information.ChurchTuring module targets derivation of the Church-Turing thesis from Recognition Science ledger universality, where any computation is a sequence of ledger updates and the eight-tick structure supplies a universal gate set. Upstream, the tape definition supplies an infinite sequence of cells for computation, while LedgerFactorization and PhiForcingDerived calibrate J-cost structures for physical processes. SpectralEmergence supplies the gauge and fermion content that may bound computational models, and IntegrationGap.A fixes the active edge count at 1 for the D=3 balance.
proof idea
This declaration is a structure definition with four fields and no proof body or lemmas applied.
why it matters
It supplies the base type for UniversalTM, which asserts that a universal Turing machine exists and can simulate any other. This supports the module target of grounding the Church-Turing thesis in Recognition Science via ledger universality and the eight-tick octave (T7). It touches the open question of mapping physical J-cost bounds to formal computation models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.