radius
plain-language theorem explainer
The definition fixes the neighborhood radius of the one-dimensional cellular automaton to the natural number 1. Researchers constructing SAT gadgets or local update rules in the Recognition Science P-vs-NP argument cite this constant when specifying three-cell interactions. The assignment is immediate from the constant declaration and matches the left-center-right structure required by the local rule.
Claim. The neighborhood radius $r$ of the cellular automaton is defined by $r = 1$.
background
The module supplies cellular automata infrastructure for encoding SAT instances as local computations. The sibling Neighborhood structure packages three CellState values (left, center, right) that occupy positions $i-1$, $i$, $i+1$. The radius constant supplies the fixed distance used by extractNeighborhood and localRule. The upstream neighborhood definition from RecognitionLatticeFromRecognizer denotes the set of all cells sharing a given observed label.
proof idea
Direct constant definition that assigns the value 1.
why it matters
The constant is referenced by forty downstream declarations, including the atomic-radii lemmas in Chemistry.AtomicRadii that depend on the three-cell neighborhood size. It anchors the CA model whose local rules evaluate SAT in $O(n^{1/3} log n)$ time while preserving ledger compatibility, as stated in the module documentation. The choice of radius 1 implements the minimal neighborhood for Rule 110 universality inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.