sat_computation_time
plain-language theorem explainer
sat_computation_time asserts that the cellular-automaton evaluation time for an n-variable SAT instance satisfies an O(n^{1/3} log n) upper bound. Workers on the Recognition Science P-vs-NP argument cite it to separate parallel computation depth from output readout cost. The bound is obtained by substituting the explicit ceiling expression for evaluation time and applying the elementary inequality ceil(x) <= x + 1 together with log(n + n + 2) <= 2 log n for n > 1.
Claim. For every positive integer $n$ there exists a positive real $c$ such that the SAT evaluation time on $n$ variables and $n$ clauses is at most $c n^{1/3} log n$.
background
The module builds one-dimensional cellular automata whose local update rules (radius-bounded, deterministic, reversible) embed Boolean clause gadgets, following the Rule-110 universal-computation model. Evaluation time is supplied by the sibling definition that returns the ceiling of $n^{1/3}$ times the logarithm of the total size; the present theorem merely records that this quantity is bounded by a constant multiple of the displayed monomial. Upstream lemmas on balanced ledgers and ledger factorization supply the reversibility needed for compatibility with the global ledger constraint.
proof idea
One-line wrapper that applies the explicit formula of the evaluation-time definition together with the standard real-analysis bound on the ceiling function and the monotonicity of the logarithm.
why it matters
The declaration supplies the parallel-computation half of the module's claimed separation between evaluation time and readout time. It sits inside the larger Cellular Automata construction whose goal is to exhibit an O(n^{1/3} log n) SAT procedure while the balanced-parity encoding forces Omega(n) queries to read the answer. No downstream theorems are recorded, indicating the result remains preparatory for the lower-bound argument sketched in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.