CARuntime
plain-language theorem explainer
Abstract runtime parameters for cellular automaton embeddings are packaged as a structure with volume and evolution step fields for use in SAT solver complexity bounds. Researchers deriving polynomial time bounds for 3-SAT via CA-to-TM reductions would reference this packaging. The definition consists of a direct structure declaration introducing the two natural number fields.
Claim. For a natural number $n$, a runtime structure is defined with fields volume and steps, both natural numbers, abstracting the parameters of a cellular automaton embedding.
background
In the Recognition Science framework, complexity analysis of SAT problems proceeds by embedding instances into cellular automata whose evolution is governed by J-cost minimization. The PhysicsComplexityStructure upstream result establishes that J-cost is convex with unique minimum at unity and that local updates affect at most eight neighbors per tick. SpectralEmergence supplies the underlying gauge and fermion structure that motivates the discrete dynamics. This module imports Mathlib and depends on several foundational structures: nuclear density tiers from NucleosynthesisTiers, LedgerFactorization for J calibration, PhiForcingDerived for J-cost, and the volume definition from BrainHolography as the cardinality of a vertex set. The local setting is an abstract packaging of runtime assumptions for the CA embedding into Turing machine simulations.
proof idea
As a structure definition, it directly declares the two fields without applying any lemmas or tactics.
why it matters
It supplies the runtime parameters consumed by the downstream simulation cost proposition, which asserts a polynomial bound on Turing machine steps in terms of volume and steps, ultimately targeting O(n^{11/3} log n) for 3-SAT. This fits the Recognition Science program of reducing computational complexity to the eight-tick octave and phi-ladder principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.