CARuntime
The CARuntime structure packages volume and steps as abstract parameters for a cellular automaton embedding in n dimensions. Researchers bounding Turing-machine simulation costs for SAT instances in Recognition Science would cite it to interface CA dynamics with polynomial-time claims. It is introduced as a bare structure definition with no proof obligations or computational content.
claimLet $n$ be a natural number. The structure CARuntime$(n)$ consists of two natural numbers: volume (the number of vertices in the configuration) and steps (the number of evolution ticks).
background
Recognition Science organizes computational and physical quantities through J-cost minimization, where J(x) = (x + 1/x)/2 - 1 is strictly convex with minimum at x = 1, and through phi-ladders that assign discrete tiers to densities and fluxes. Upstream structures supply nuclear densities in phi-tiers, ledger factorization for the multiplicative group, spectral emergence forcing SU(3) x SU(2) x U(1) with three generations, and J-cost convexity together with eight-tick local dynamics. The present module imports these to model SAT runtime via cellular-automaton embeddings.
proof idea
The declaration is a direct structure definition. No lemmas are applied and no tactics are used; it simply packages the two Nat fields for later use in propositions.
why it matters in Recognition Science
CARuntime supplies the interface required by ca_to_tm_simulation_prop, which states that TM time is O(volume * steps) and targets an overall O(n^{11/3} log n) bound for 3-SAT. It thereby connects the phi-forcing and information-complexity structures to concrete complexity claims inside the Recognition framework.
scope and limits
- Does not assign concrete numerical values to volume or steps.
- Does not prove any runtime bound by itself.
- Does not encode dimension-specific geometry beyond the parameter n.
- Does not impose positivity or monotonicity constraints on the fields.
Lean usage
def ca_to_tm_simulation_prop {n} (rt : CARuntime n) : Prop := ∃ c : Nat, c > 0 ∧ rt.volume * rt.steps ≤ c * n^2formal statement (Lean)
8structure CARuntime (n : Nat) where
9 volume : Nat
10 steps : Nat
11
12/-- Abstract packaging of the CA runtime bound assumptions. -/