H_SATCARuntime
plain-language theorem explainer
The declaration defines the hypothesis that a SAT instance encoded as a SATGadget admits cellular-automaton evaluation in time at most the precomputed sat_eval_time bound. Complexity theorists examining sublinear SAT solvers inside the Recognition Science model would reference this construction. The definition consists of an existential quantifier over the step count together with a placeholder correctness predicate that has not yet been formalized.
Claim. Let $sg$ be a SAT instance encoded as a gadget with $n$ variables and $m$ clauses. Then $H_{SATCA Runtime}(sg)$ asserts that there exists a natural number $t$ with $t ≤ τ(n,m)$ such that the cellular automaton on $sg$ produces the correct satisfiability outcome after $t$ steps, where $τ(n,m)$ is the evaluation-time function.
background
In the Cellular Automata module, SAT instances are represented by the SATGadget structure, which packages the number of variables $n$, the number of clauses $m$, a list of ClauseGadget objects, variable positions on the tape, and an output cell. The module establishes that SAT can be evaluated by a one-dimensional cellular automaton with local deterministic rules derived from Rule 110, exploiting parallelism to achieve faster computation than sequential methods.
proof idea
The definition directly asserts the existence of a suitable runtime $t$ bounded above by sat_eval_time sg.n sg.m together with the predicate IsCorrectSATResult sg t. Because IsCorrectSATResult remains undefined, the construction functions as a scaffold rather than a completed theorem; no lemmas are applied beyond the direct reference to the time bound.
why it matters
This definition supplies the runtime hypothesis required for the CA-to-TM simulation section of the P versus NP argument in Recognition Science. It encodes the claim that the O(n^{1/3} log n) bound arising from parallel propagation on the three-dimensional lattice can be realized by a local cellular automaton. The open task is to replace the placeholder IsCorrectSATResult with a concrete predicate and to discharge the bound via dependency-cone counting, which would close the scaffold toward the full simulation theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.