ca_k_local
The declaration fixes the neighborhood radius of the one-dimensional cellular automaton at exactly 1. Researchers constructing SAT gadgets via local rules in the Recognition Science P vs NP argument would cite it to establish the dependency cone. The proof is a direct reflexivity step on the radius definition.
claimThe neighborhood radius of the cellular automaton is 1.
background
The module supplies cellular automata gadgets for SAT evaluation inside the Recognition Science framework. It adapts the Rule 110 universal model to produce local, deterministic, and reversible updates that evaluate Boolean circuits while preserving ledger compatibility. The upstream radius definition sets the neighborhood to cells at positions i-1, i, and i+1, fixing the interaction range to one cell on each side.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of radius.
why it matters in Recognition Science
This anchors the locality assumption required for the SAT evaluation pipeline, confirming that each update depends only on immediate neighbors. It supports the module claim that SAT can be evaluated by a CA with local rules and that computation time remains O(n^{1/3} log n) before readout. The result aligns with the framework emphasis on local update rules that exploit parallelism while the balanced-parity encoding still forces Ω(n) queries for the final answer.
scope and limits
- Does not establish universality of the chosen CA rule.
- Does not derive the O(n^{1/3} log n) time bound.
- Does not address the CA-to-TM simulation step.
- Does not quantify the dependency cone for arbitrary time steps.
formal statement (Lean)
105theorem ca_k_local : radius = 1 := rfl
proof body
Term-mode proof.
106
107/-- Dependency cone: after t steps, position i depends only on [i-t, i+t] -/