Transition
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not define the full state set or tape alphabet of any concrete machine.
- Does not include initial configuration or halting condition.
- Does not prove equivalence to lambda calculus or other models.
- Does not embed J-cost or phi-ladder arithmetic.
formal statement (Lean)
57structure Transition where
58 currentState : ℕ
59 currentSymbol : ℕ
60 newState : ℕ
61 newSymbol : ℕ
62 moveRight : Bool -- True = right, False = left
63
64/-! ## Universal Turing Machine -/
65
66/-- A Universal Turing Machine (UTM) can simulate any other TM.
67
68 Given:
69 - Description of TM T (on tape)
70 - Input x
71
72 UTM computes T(x).
73
74 This is the foundation of programmable computers! -/
used by (16)
-
Enzyme -
alkali_low_ionization -
cohesiveEnergyProxy -
freeElectrons -
transition_cohesive_gt_alkali -
btfr_mass_velocity_relation -
ledger_follows_8tick -
utm_exists -
J_pos_of_ne_one -
J_transition -
J_transition_self -
confinementPredictions -
amplitude -
measurement_postulate_derived -
transition_at_zero -
transitionProbability