H_SATTMRuntime
plain-language theorem explainer
H_SATTMRuntime packages the claim that SAT evaluation via cellular automaton can be simulated by a Turing machine in time at most n times the CA evaluation time. Complexity theorists examining the Recognition Science approach to P versus NP would cite this when bounding simulation overhead. The definition is a direct existential statement over the runtime bound conjoined with an undefined correctness predicate.
Claim. Let $H(n,m)$ be the proposition that there exists a natural number $T$ such that $T$ is at most $n$ times the cellular-automaton evaluation time for the SAT instance with $n$ variables and $m$ clauses, and the Turing-machine simulation of that automaton produces the correct output for the instance.
background
The module builds cellular automata gadgets for SAT evaluation using local rules adapted from Rule 110. Each gadget is local (depends only on neighbors within radius $r$), deterministic, and reversible to preserve ledger compatibility. The upstream definition sat_eval_time $n$ $m$ computes the CA runtime as the ceiling of $n^{1/3}$ times the logarithm of $n+m+2$, reflecting optimal 3D-like grid arrangement of variables and logarithmic depth for clause evaluation.
proof idea
The declaration is a direct definition that introduces an existential quantifier over runtime $T$ bounded by $n$ times sat_eval_time, conjoined with the correctness condition. No lemmas are applied. The predicate IsCorrectTMResult remains undefined, marking this as a scaffolding step.
why it matters
This definition supports the module goal of showing SAT evaluation by CA with local rules while the CA-to-TM simulation preserves the $O(n^{1/3} log n)$ bound, yielding an overall $O(n^{4/3} log n)$ Turing time. It contributes to the P versus NP infrastructure by separating computation time from the balanced-parity encoding that forces Omega(n) queries. The open question is to define the correctness predicate and prove the simulation bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.