TMSimulator
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not define the local rule or cell-state alphabet.
- Does not prove any simulation-time bound.
- Does not address reversibility or sigma-zero preservation.
- Does not reference the phi-ladder or J-uniqueness.
Lean usage
def sim : TMSimulator := { ca_steps := 100, tape_size := 64 }formal statement (Lean)
195structure TMSimulator where
196 /-- Number of CA steps to simulate -/
197 ca_steps : ℕ
198 /-- Tape size (number of cells) -/
199 tape_size : ℕ
200 /-- TM time per CA step (linear in tape size) -/
201 time_per_step : ℕ := tape_size
proof body
Definition body.
202
203/-- TM time to simulate CA -/