tm_simulation_time
tm_simulation_time computes the total Turing machine steps to run a cellular automaton simulation as the product of the number of CA steps and the time cost per step. Researchers bounding simulation overhead for SAT evaluation via local CA rules in the Recognition Science framework cite it when closing the CA-to-TM accounting. The definition is a direct field multiplication from the TMSimulator structure with no additional lemmas.
claimFor a Turing machine simulator $sim$ of a cellular automaton, the total simulation time equals $ca_steps(sim) times time_per_step(sim)$, where $time_per_step$ defaults to the tape size.
background
The TMSimulator structure records the parameters for a Turing machine that emulates a cellular automaton: the number of CA steps to execute, the tape size in cells, and the time per step, which is defined to equal the tape size. This definition sits inside the Cellular Automata module whose module documentation states that SAT instances are evaluated by a one-dimensional cellular automaton with local rules based on Rule 110, that the CA computation time scales as $O(n^{1/3} log n)$, and that the CA-to-TM simulation must preserve this bound while maintaining reversibility for ledger compatibility.
proof idea
The definition is a one-line wrapper that multiplies the ca_steps field by the time_per_step field of the TMSimulator structure.
why it matters in Recognition Science
It supplies the concrete time expression used by the downstream tm_simulation_bound theorem, which asserts that the Turing machine time equals ca_steps times tape_size. The definition therefore closes the accounting step in the module's argument that local CA gadgets evaluate SAT while the simulation overhead remains linear in tape size, consistent with the Recognition Science claim that the CA-to-TM map preserves the sub-cubic bound.
scope and limits
- Does not establish the $O(n^{1/3} log n)$ bound claimed for the CA computation itself.
- Does not define or verify the local update rule or neighborhood radius.
- Does not incorporate Recognition Science constants such as the golden ratio or the eight-tick octave.
- Does not address reversibility preservation or balanced-parity readout.
Lean usage
theorem tm_simulation_bound (sim : TMSimulator) : tm_simulation_time sim = sim.ca_steps * sim.tape_size := by simp only [tm_simulation_time, TMSimulator.time_per_step]formal statement (Lean)
204def tm_simulation_time (sim : TMSimulator) : ℕ :=
proof body
Definition body.
205 sim.ca_steps * sim.time_per_step
206
207/-- Simulation bound: TM time is CA_steps × tape_size -/