TMSimulator
plain-language theorem explainer
TMSimulator packages the parameters for bounding Turing-machine simulation of a cellular-automaton computation on a finite tape. Researchers deriving time overheads for SAT evaluation via local CA rules in the Recognition Science framework cite this record when converting CA steps into TM steps. The declaration is a plain structure with three fields and one default value, carrying no proof obligations.
Claim. A structure consisting of a natural number $n_{ca}$ (number of CA steps), a natural number $n_{tape}$ (tape size), and a natural number $t_{step}$ (time per step, defaulting to $n_{tape}$).
background
The module supplies CA gadgets for SAT resolution under the Recognition Science model, employing a one-dimensional cellular automaton with local update rules derived from Rule 110. The tape is formalized as a function from integers to cell states, with finite windows extracted for neighborhood-based rules. Upstream structures calibrate J-cost and ledger factorization while the step operation applies the local rule globally to obtain the successor tape.
proof idea
The declaration is a structure definition whose only non-trivial content is the default value time_per_step := tape_size. No lemmas or tactics are invoked; the record simply aggregates the three natural-number parameters for later use.
why it matters
TMSimulator supplies the data carrier for tm_simulation_time and tm_simulation_bound, which establish that TM simulation time equals ca_steps times tape_size. It supports the module claim that CA evaluation of SAT instances runs in O(n^{1/3} log n) time while the simulation overhead remains linear in tape size, consistent with the eight-tick octave and local-rule reversibility required for ledger compatibility. The construction touches the open question of whether the resulting bound stays sub-polynomial in the original SAT instance size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.