TMSimulator
plain-language theorem explainer
TMSimulator packages the parameters needed to bound the Turing machine resources required to run a cellular automaton simulation of a SAT instance. Complexity theorists working on the Recognition Science P vs NP argument would cite this record when establishing the linear simulation overhead. The definition is a plain structure with three natural-number fields and a single default value.
Claim. A record type whose fields are three natural numbers: the number of cellular-automaton steps to execute, the number of cells on the tape, and the Turing-machine time cost per cellular-automaton step (defaulting to the tape length).
background
The module constructs one-dimensional cellular automata with local update rules to evaluate SAT instances, exploiting parallelism while preserving ledger compatibility. The Tape type is an infinite map from integers to cell states, although only finite windows are used in practice. The step function applies the local rule to every cell to produce the successor tape. Upstream structures supply the J-cost, ledger factorization, and spectral emergence data that calibrate the underlying physical model.
proof idea
The declaration is a structure definition that simply declares the three fields and supplies the default for the third field.
why it matters
TMSimulator supplies the input type for the two downstream definitions tm_simulation_time and tm_simulation_bound, which together establish that Turing-machine simulation time equals ca_steps times tape_size. This closes one link in the chain that converts the O(n^{1/3} log n) cellular-automaton evaluation bound into a Turing-machine resource bound for the SAT problem inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.