sat_computation_time
plain-language theorem explainer
The theorem asserts an upper bound on the steps needed for a one-dimensional cellular automaton to evaluate a Boolean satisfiability instance of size n. Complexity theorists examining parallel computation in physical models would reference this bound to support claims of sub-cubic scaling. It arises directly from the formula defining the automaton's evaluation time as roughly n to the one-third power times the logarithm of n.
Claim. For every natural number $n > 0$, there exists a positive real $c$ such that the cellular-automaton evaluation time for a SAT instance with $n$ variables and $n$ clauses satisfies $t(n,n) ≤ c · n^{1/3} · log n$.
background
The module supplies cellular-automaton infrastructure for a P-versus-NP argument. It equips a one-dimensional automaton with local deterministic rules (radius-bounded neighborhoods, reversible updates) to evaluate Boolean circuits. The evaluation time for n variables and m clauses is defined explicitly as the ceiling of n to the power 1/3 multiplied by the logarithm of n plus m plus two; this expression encodes the optimal width of variable propagation and the logarithmic depth of clause aggregation.
proof idea
No proof body is supplied. The claim is a direct algebraic consequence of the closed-form definition of evaluation time. It invokes the real-power and logarithm functions, absorbs the ceiling and additive constants inside the logarithm by enlarging c, and specializes the general (n,m) expression to the square case m = n.
why it matters
The bound realizes the module's stated goal that SAT evaluation by local cellular-automaton rules runs in O(n^{1/3} log n) steps. It supplies one half of the complexity claim needed for the CA-to-TM simulation that preserves the time bound. The surrounding documentation flags the complementary linear lower bound arising from balanced-parity output encoding, leaving the full recognition-time picture as a TODO.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.