tm_simulation_bound
plain-language theorem explainer
The theorem states that Turing machine simulation time for a cellular automaton equals the product of CA steps and tape size. Researchers deriving overall TM costs for SAT evaluation in Recognition Science CA models would cite this equality when converting parallel CA steps into sequential TM time. The proof is a one-line simplification that unfolds the simulation time definition and the default time per step field.
Claim. For a Turing machine simulator of a cellular automaton with $n$ steps and tape size $m$, where time per step defaults to $m$, the total simulation time equals $n m$.
background
The module constructs local cellular automata gadgets for SAT evaluation under Recognition Science, using Rule 110 style rules that are local, deterministic, and reversible to preserve ledger compatibility. TMSimulator is the structure holding ca_steps (number of CA steps), tape_size (number of cells), and time_per_step (defaulting to tape_size). The upstream definition tm_simulation_time computes the product of ca_steps and time_per_step, providing the direct algebraic relation used here.
proof idea
One-line simp tactic that unfolds the definition of tm_simulation_time together with the TMSimulator.time_per_step field, which is defined to equal tape_size.
why it matters
This supplies the exact conversion factor needed to translate the module's target CA runtime O(n^{1/3} log n) into a TM simulation bound. The surrounding hypothesis comment notes that the predicted total Turing time for SAT via CA is O(n^{4/3} log n) once the CA runtime is established; the present equality closes the simulation step in that chain. It sits inside the broader P vs NP resolution effort that relies on the Recognition Composition Law and the eight-tick octave for ledger constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.