sat_eval_time
plain-language theorem explainer
Defines the evaluation time for a SAT instance with n variables and m clauses as the ceiling of n to the one-third power times the logarithm of n plus m plus two. Researchers addressing P versus NP via cellular automata in the Recognition Science setting would cite this expression. The definition directly encodes the claimed sublinear bound from parallel propagation on a 3D-embedded tape.
Claim. $t(n,m) = 2^{1/3} n^{1/3} (n+m+2) $ where $t$ denotes the number of steps for cellular-automaton evaluation of a SAT instance with $n$ variables and $m$ clauses.
background
The module constructs local cellular-automaton gadgets for Boolean operations to evaluate SAT instances. Each gadget is local (depends only on neighbors within fixed radius), deterministic, and reversible to preserve ledger compatibility. The setting exploits a 1D tape embedded in three dimensions so that clause evaluation propagates in parallel across a dependency cone whose width scales as the cube root of the variable count.
proof idea
One-line definition that applies the real power function to n with exponent one-third, multiplies by the natural logarithm of n plus m plus two, and takes the ceiling.
why it matters
Supplies the runtime expression referenced by H_SATCARuntime and H_SATTMRuntime, which in turn feed the broader claim that SAT evaluation via CA stays sublinear. It fills the O(n^{1/3} log n) slot in the P-versus-NP argument inside the Recognition Science framework. The formal counting of dependency-cone steps remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.