H_SATTMRuntime
plain-language theorem explainer
H_SATTMRuntime encodes the hypothesis that SAT evaluation on n variables and m clauses admits a Turing machine runtime T at most n times the cellular automaton evaluation time while returning a correct result. Researchers bounding simulation overhead in Recognition Science complexity models would cite it when converting CA parallelism into TM costs. The definition is an existential statement over the runtime bound that directly multiplies the precomputed sat_eval_time by n and conjoins a placeholder correctness predicate.
Claim. For $n,m$ natural numbers, $H(n,m)$ holds when there exists $T$ such that $T$ is at most $n$ times the cellular-automaton evaluation time for the SAT instance and the Turing-machine simulation of that automaton produces the correct satisfiability outcome.
background
The module builds local cellular-automaton gadgets for SAT using deterministic, reversible rules adapted from Rule 110. Variables are arranged to exploit three-dimensional-like parallelism on a one-dimensional tape, yielding the evaluation time defined upstream as the ceiling of $n^{1/3}$ times the logarithm of $n+m+2$. This supplies the base CA runtime that the present definition multiplies by $n$ to account for Turing-machine readout.
proof idea
The definition is a direct existential quantification: it asserts a natural number $T$ bounded above by the product of $n$ and sat_eval_time, then conjoins the still-undefined predicate IsCorrectTMResult. No tactics or lemmas are applied; the body is a literal encoding of the intended runtime hypothesis.
why it matters
The declaration supplies the interface for total TM runtime in the CA-based SAT solver, supporting the module's intended claim of O(n^{1/3} log n) CA time with an n-factor simulation overhead. It advances the P-versus-NP analysis inside the Recognition Science framework by formalizing the conversion from local CA steps to global TM cost. The module documentation flags the open task of proving the simulation bound once IsCorrectTMResult is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.