ca_is_local
plain-language theorem explainer
The result shows that each cell's next state in the cellular automaton is computed exclusively from its radius-1 neighborhood via the local rule. Complexity theorists modeling SAT resolution through cellular automata would reference this locality property. The equality holds directly by unfolding the definition of the global step function.
Claim. For any tape configuration $τ : ℤ → CellState$ and position $i ∈ ℤ$, the successor state at $i$ equals the local update rule applied to the three-cell neighborhood centered at $i$.
background
The Tape type is defined as an infinite sequence of cell states indexed over the integers. extractNeighborhood pulls the left, center, and right cells from positions $i-1$, $i$, and $i+1$. localRule encodes the deterministic update based on those three states, and step applies the rule uniformly by mapping every position through the neighborhood extractor. The module documentation frames this infrastructure as the basis for local gadgets that evaluate SAT instances via a 1D cellular automaton with radius-1 rules.
proof idea
The proof is a one-line reflexivity wrapper that applies the definition of step, which is constructed exactly as the pointwise application of localRule to extractNeighborhood.
why it matters
This locality result supports the module claim that SAT can be evaluated by a CA with local rules while preserving the O(n^{1/3} log n) time bound. It supplies the deterministic local update needed for ledger compatibility in the Recognition Science model and feeds the construction of Boolean gadgets in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.