tm_simulation_time
plain-language theorem explainer
The definition computes total Turing machine steps to simulate a cellular automaton run as the product of automaton step count and time per step. Researchers bounding the overhead when mapping cellular automata SAT evaluation to Turing machines in the Recognition Science model would cite this quantity. It is realized as a direct multiplication of two fields from the simulator structure.
Claim. For a simulator $s$ of a cellular automaton, the total Turing machine simulation time is $ca_steps(s) times time_per_step(s)$.
background
The module supplies cellular automata gadgets with local deterministic rules for SAT evaluation, based on Rule 110, and states that the automata compute in $O(n^{1/3} log n)$ time while remaining reversible for ledger compatibility. A Turing machine simulator is the structure holding the number of cellular automaton steps, the tape size in cells, and the time per step (defaulting to tape size).
proof idea
One-line definition that returns the product of the ca_steps and time_per_step fields of the simulator structure.
why it matters
It supplies the time quantity used by the downstream simulation bound theorem, which equates the value to ca_steps times tape_size. This supports the module claim that the cellular automaton to Turing machine simulation preserves the $O(n^{1/3} log n)$ bound for SAT evaluation and contributes to the P versus NP argument by quantifying simulation overhead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.