CARuntimeModel
plain-language theorem explainer
CARuntimeModel packages the assumptions needed to bound the runtime of a cellular automaton simulation of SAT problems. Researchers working on complexity bounds in Recognition Science would cite it when deriving time complexities for CA embeddings. The structure is a straightforward record definition with no computational content.
Claim. A CARuntimeModel consists of a function $s: ℕ → ℕ$ (grid side length) such that there exist positive reals $c_1, c_2$ with $c_1 n^{1/3} ≤ s(n) ≤ c_2 n^{1/3}$ for all $n ∈ ℕ$, together with a proposition asserting that constraints are realized by gadgets of $O(1)$ diameter.
background
The module supplies abstract runtime parameters for the CA embedding. The sideLength field maps input size $n$ to grid dimension, while sideLength_bound encodes the cubic-root scaling that follows from three spatial dimensions. Locality remains an abstract Prop standing for constant-diameter constraint gadgets.
proof idea
This is a structure definition with no proof body. It directly records the sideLength function, the existential scaling bound, and the locality proposition as fields of a single record type.
why it matters
The declaration supplies the input record to caTimeBound, which targets an $O(n^{1/3} log n)$ runtime under locality and logarithmic logical depth. It interfaces the complexity analysis with the Recognition Science forcing chain at the step that fixes $D=3$ spatial dimensions and the eight-tick octave. The structure closes a packaging gap for embedding SAT instances into the phi-ladder without introducing extra cost factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.