tm_simulation_bound
plain-language theorem explainer
The equality states that Turing machine simulation time for a cellular automaton equals the product of CA steps and tape size. Researchers bounding simulation overheads for SAT evaluation in Recognition Science models would cite this identity when translating CA runtimes into TM costs. The proof is a direct simplification that unfolds the simulation time definition and substitutes the default time per step.
Claim. Let sim be a Turing machine simulator structure with fields ca_steps (number of cellular automaton steps) and tape_size (number of cells). Then the Turing machine simulation time of sim equals ca_steps multiplied by tape_size.
background
The TMSimulator structure consists of ca_steps, tape_size, and time_per_step (defaulting to tape_size). The function tm_simulation_time is defined as the product of ca_steps and time_per_step. This identity appears inside the module that supplies cellular automata gadgets for SAT evaluation, where local deterministic reversible rules based on Rule 110 are used to process Boolean circuits while preserving ledger compatibility.
proof idea
The proof is a one-line wrapper that applies simplification on the definitions of tm_simulation_time and the time_per_step field of TMSimulator.
why it matters
This identity supplies the basic accounting step inside the cellular automata module for the P versus NP resolution. It supports the module claim that CA to TM simulation preserves the O(n^{1/3} log n) computation time, though the overall predicted O(n^{4/3} log n) Turing time remains a scaffold pending a formal bound on ca_steps. The construction sits downstream of the Recognition Composition Law and the eight-tick octave but does not yet close the simulation overhead for the balanced-parity encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.