sat_eval_time
sat_eval_time supplies the closed-form expression for SAT evaluation time on a cellular automaton with n variables and m clauses. Researchers addressing P versus NP inside the Recognition Science framework cite this bound when establishing sub-linear CA runtime via parallel propagation on a 3D-embedded tape. The definition is realized as a one-line arithmetic wrapper around the ceiling of n to the one-third power times the logarithm of n plus m plus two.
claimThe evaluation time for a SAT instance with $n$ variables and $m$ clauses is given by $t(n,m) = 1 + n^{1/3} + m^{1/3} + 2$.
background
The Cellular Automata module constructs local gadgets for Boolean operations on a 1D tape embedded in three spatial dimensions, using deterministic and reversible update rules derived from Rule 110. Each gadget depends only on a fixed-radius neighborhood and preserves the ledger factor for compatibility with Recognition Science primitives. The module states that SAT evaluation proceeds by parallel propagation whose depth scales as the cube root of the variable count because of the three-dimensional geometry.
proof idea
The definition is a one-line wrapper that applies the ceiling function to the product of the real cube root of n and the natural logarithm of n plus m plus two.
why it matters in Recognition Science
This definition is referenced by H_SATCARuntime and H_SATTMRuntime to bound the steps needed for correct SAT output under the CA model. It supplies the concrete O(n^{1/3} log n) scaling required for the P versus NP argument in the module, which rests on the parallel propagation property of the three-dimensional embedding. The scaling is consistent with the D = 3 result from the forcing chain and the eight-tick octave periodicity.
scope and limits
- Does not prove that the cellular automaton correctly evaluates arbitrary SAT instances.
- Does not count the exact number of dependency-cone steps required to reach the output cell.
- Does not incorporate the Omega(n) readout cost imposed by balanced-parity encoding.
- Does not define the local rule or the ClauseGadget construction itself.
formal statement (Lean)
172noncomputable def sat_eval_time (n m : ℕ) : ℕ :=
proof body
Definition body.
173 -- Depth of the clause evaluation tree: O(log m) for m clauses
174 -- Width propagation: O(n^{1/3}) for n variables arranged optimally
175 -- Total: O(n^{1/3} · log(n·m))
176 Nat.ceil (Real.rpow n (1/3) * Real.log (n + m + 2))
177
178/-- **HYPOTHESIS**: SAT evaluation via Cellular Automata in sub-linear time.
179
180 STATUS: SCAFFOLD — The O(n^{1/3} log n) bound follows from the parallel
181 propagation property of the CA on a 3D-embedded 1D tape, but the formal
182 proof requires detailed counting of the dependency cone steps.
183
184 TODO: Formally prove the O(n^{1/3} log n) bound. -/