caTimeBound
plain-language theorem explainer
caTimeBound defines the target runtime scaling for a cellular automaton model of SAT instances as the existence of c > 0 such that side length times logical depth stays below c n^{1/3} log(n+2). Researchers bounding simulation costs in recognition-based complexity models would cite this when stating the O(n^{1/3} log n) envelope. The definition directly encodes the product of the model's sideLength function and the logarithmic depth function under the stated locality and scaling assumptions.
Claim. Let M be a CARuntimeModel whose sideLength function satisfies c_1 n^{1/3} ≤ sideLength(n) ≤ c_2 n^{1/3} for positive constants c_1, c_2 and whose locality assumption holds. Let logicalDepth(n) = ⌈log_2(n+1)⌉. Then the bound holds when there exists c > 0 such that sideLength(n) · logicalDepth(n) ≤ c · n^{1/3} · log(n+2).
background
CARuntimeModel packages the abstract assumptions for embedding SAT into a cellular automaton: sideLength maps input count n to grid side length with the explicit Θ(n^{1/3}) sandwich, and locality asserts that constraints are realized by constant-diameter gadgets. logicalDepth is defined as the ceiling of log base 2 of (n+1), capturing the number of implication layers. The module supplies abstract runtime parameters for the CA embedding, with upstream cost functions drawn from MultiplicativeRecognizerL4 and ObserverForcing that equate recognition cost to J-cost on positive ratios.
proof idea
One-line definition that directly states the target inequality by substituting the sideLength and logicalDepth projections from the CARuntimeModel structure.
why it matters
It supplies the concrete target scaling used by the sibling three_sat_runtime_prop and ca_to_tm_simulation_prop when analyzing SAT runtime inside the recognition framework. The definition closes the abstract runtime interface for the module without invoking the full forcing chain or phi-ladder constants. No downstream uses are recorded, leaving open how the bound will be discharged against concrete J-cost or inflaton-potential models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.