tm_simulation_bound
plain-language theorem explainer
The theorem states that the total Turing machine time to simulate a cellular automaton equals the product of the number of CA steps and the tape size. Researchers deriving overall simulation costs for SAT evaluation in Recognition Science models would cite this equality when converting CA runtimes into TM bounds. The proof is a one-line simplification that unfolds the time definition and the simulator structure field.
Claim. For any Turing machine simulator $sim$ of a cellular automaton, the total simulation time equals the number of cellular automaton steps multiplied by the tape size: $t(sim) = c · w$, where $c$ is the number of steps and $w$ is the tape size.
background
The module constructs local cellular automaton gadgets for SAT evaluation under Recognition Science, using deterministic, reversible rules adapted from Rule 110 to achieve O(n^{1/3} log n) CA time while preserving ledger compatibility. TMSimulator is the structure that records ca_steps (number of CA steps to simulate), tape_size (number of cells), and time_per_step (defaulting to tape_size, reflecting linear TM cost per CA step). The upstream definition tm_simulation_time computes the product sim.ca_steps * sim.time_per_step, which this theorem specializes by substituting the default.
proof idea
The proof is a one-line wrapper that applies simp only on tm_simulation_time and the TMSimulator.time_per_step field, directly substituting the default value tape_size to obtain the stated equality.
why it matters
This equality closes the CA-to-TM simulation accounting step in the module's P versus NP infrastructure, ensuring the Turing machine cost inherits the cellular automaton runtime directly. It supports the module's claim that the CA-to-TM simulation preserves the O(n^{1/3} log n) bound for SAT evaluation via local gadgets. The result sits inside the broader Recognition Science complexity analysis that links cellular automata to the phi-ladder and ledger factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.