Transition
plain-language theorem explainer
A record structure that encodes one step of a Turing machine by storing the current state and symbol, the successor state and symbol, and the head direction. Recognition Science researchers cite it when modeling ledger updates as computation steps. The declaration is a plain structure definition with five fields and no proof content.
Claim. A transition is a 5-tuple $(q, s, q', s', d)$ with $q, q' : ℕ$ (states), $s, s' : ℕ$ (symbols), and $d : Bool$ (true for right move, false for left).
background
The Information.ChurchTuring module derives the Church-Turing thesis from ledger universality in Recognition Science. The 8-tick structure supplies a universal gate set, so any computation becomes a sequence of ledger updates. Upstream results include the active edge count A per tick and structures for J-cost and phi-forcing that calibrate those updates.
proof idea
This is a structure definition that introduces the five fields for a TM transition. No lemmas are applied; the declaration simply assembles the components required by downstream constructions such as ledger_follows_8tick.
why it matters
The definition supplies the atomic step for universal Turing machines in the same module and appears in downstream results on enzyme catalysis and metallic bonding, where transitions model physical state changes. It fills the paper proposition on the physical basis of universal computation and connects directly to the eight-tick octave that forces universal gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.