tm_simulation_bound
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the overall asymptotic bound O(n^{4/3} log n) for SAT evaluation.
- Does not prove the underlying cellular automaton runtime bound.
- Does not address reversibility or ledger compatibility properties beyond time accounting.
- Does not extend to multi-tape or non-linear TM models.
formal statement (Lean)
208theorem tm_simulation_bound (sim : TMSimulator) :
209 tm_simulation_time sim = sim.ca_steps * sim.tape_size := by
proof body
Term-mode proof.
210 simp only [tm_simulation_time, TMSimulator.time_per_step]
211
212/-- **HYPOTHESIS**: Turing Machine simulation of SAT evaluation via CA.
213
214 STATUS: SCAFFOLD — The total Turing time for SAT evaluation via CA is
215 predicted to be O(n^{4/3} log n), but this depends on the CA runtime bound.
216
217 TODO: Formally prove the simulation time bound. -/