ca_to_tm_simulation_prop
plain-language theorem explainer
The declaration defines the proposition that a Turing machine can simulate a given cellular automaton runtime instance in quadratic time relative to input size n. Complexity theorists analyzing SAT solvers via CA embeddings would cite this property when establishing polynomial bounds. The definition is a direct existential assertion over a positive constant c with no auxiliary lemmas or reductions.
Claim. Let $rt$ be a runtime instance for a cellular automaton on parameter $n$, with volume $V$ and steps $T$. Then there exists a positive integer $c$ such that $V T ≤ c n^2$.
background
The module supplies abstract runtime parameters for the CA embedding. CARuntime n is the structure packaging two natural numbers: volume for spatial extent and steps for temporal duration. This definition encodes the simulation cost assumption that a Turing machine realizes the automaton in time proportional to the product of those quantities.
proof idea
This is a direct definition that encodes the simplified polynomial bound as an existential statement over a positive constant c. No lemmas are applied and no tactics are used; the body is the base assertion itself.
why it matters
This definition supplies the core simulation-cost hypothesis for bounding 3-SAT algorithms that proceed via cellular-automaton embeddings, with the module comment targeting an overall O(n^{11/3} log n) Turing-machine time. It sits inside the Complexity.SAT.Runtime module as a reusable Prop for later runtime arguments, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.