caTimeBound
plain-language theorem explainer
caTimeBound encodes the target runtime for cellular-automaton simulation of n-variable SAT as O(n^{1/3} log n). Researchers bounding embedding costs under locality and logarithmic depth in recognition-based models would cite the predicate when deriving simulation overhead. The definition is a direct existential statement: a positive constant c absorbs the product of side length and logical depth.
Claim. Let $M$ be a model whose side-length function satisfies the bound $c_1 n^{1/3} ≤ sideLength(n) ≤ c_2 n^{1/3}$ for positive constants $c_1, c_2$ and whose locality proposition holds. Let logicalDepth$(n)$ be the ceiling of log base 2 of $(n+1)$. Then caTimeBound$(M,n)$ asserts the existence of $c>0$ such that sideLength$(n) · logicalDepth$(n) ≤ c · n^{1/3} log$(n+2)$.
background
The module supplies abstract runtime parameters for embedding SAT instances into cellular automata. CARuntimeModel packages a side-length map together with its Θ(n^{1/3}) scaling assumption and an abstract locality proposition that constraints are realized by constant-diameter gadgets. logicalDepth is the ceiling of log base 2 of (n+1) and counts implication layers in the propagation graph.
proof idea
The declaration is a direct definition of the target inequality. It quantifies over a positive real c and asserts the product of the model's sideLength(n) and logicalDepth(n) is dominated by c n^{1/3} log(n+2). No lemmas are invoked; the body simply writes the desired bound.
why it matters
The predicate supplies the concrete scaling target for CA-to-TM simulation cost in the SAT runtime analysis. It sits inside the broader Recognition Science program that derives computational bounds from J-cost and multiplicative recognizers. No downstream theorems are recorded yet, leaving open the question of whether an explicit CA construction meets the bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.