tm_simulation_time
plain-language theorem explainer
tm_simulation_time defines the total Turing machine steps required to simulate a cellular automaton execution as the product of the number of CA steps and the time cost per step. Researchers bounding simulation overhead in the CA-based SAT evaluation for P vs NP would cite this quantity when converting CA runtimes into TM runtimes. The definition is a direct field multiplication with no lemmas or tactics applied.
Claim. Let $S$ be a Turing machine simulator with $c$ cellular automaton steps, tape size $t$, and time per step $p$ (defaulting to $t$). The simulation time is $c p$.
background
The module builds local cellular automata gadgets, based on Rule 110, to evaluate SAT instances under Recognition Science. A TMSimulator records the CA steps to simulate, the tape size in cells, and the time per step (linear in tape size). The module doc states that the CA computes SAT in $O(n^{1/3} log n)$ time while TM readout still requires linear queries due to balanced-parity encoding.
proof idea
One-line definition that multiplies the ca_steps field by the time_per_step field of the TMSimulator structure.
why it matters
This definition supplies the time quantity used by the downstream theorem tm_simulation_bound, which equates TM time to ca_steps times tape_size. It supports the module claim that CA to TM simulation preserves the stated complexity bound for SAT evaluation. The construction contributes to the local-rule SAT evaluation step in the P vs NP argument via cellular automata.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.