sat_eval_time
plain-language theorem explainer
sat_eval_time supplies an explicit formula for the runtime of SAT evaluation on a cellular automaton given n variables and m clauses. Researchers analyzing the Recognition Science treatment of P versus NP would cite this expression when bounding parallel steps on a 3D-embedded tape. The definition is a direct closed-form implementation of the claimed O(n^{1/3} log(n+m)) scaling with no supporting lemmas.
Claim. The evaluation time for a SAT instance with $n$ variables and $m$ clauses is $t(n,m) = 2^{1/3} n^{1/3} (n+m+2)$ (ceiling applied).
background
The Cellular Automata module builds local gadgets for Boolean operations on a 1D tape using Rule 110 dynamics. Each gadget is required to be local (fixed radius), deterministic, and reversible to preserve ledger compatibility. The module doc states that the CA exploits parallelism for sublinear evaluation while output extraction remains linear due to balanced-parity encoding.
proof idea
One-line definition that directly encodes the target bound via Real.rpow and Real.log followed by Nat.ceil. No upstream lemmas are invoked; the body is the formula itself.
why it matters
The definition is referenced by H_SATCARuntime and H_SATTMRuntime, which assert the sublinear CA runtime and the resulting TM simulation bound. It supplies the computational step toward the P vs NP claim in Recognition Science, drawing on the D=3 spatial embedding for the n^{1/3} factor. The module comment flags that a formal dependency-cone proof remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.