Neighborhood
plain-language theorem explainer
The local neighborhood structure is a triple of adjacent cell states on a one-dimensional tape, capturing the configuration at positions i-1, i and i+1. Researchers constructing cellular-automaton gadgets for SAT evaluation in the Recognition Science P-vs-NP argument would cite this record when defining local update rules. It is introduced as a direct three-field record with no computation or proof obligations.
Claim. A neighborhood is a triple $(s_{i-1}, s_i, s_{i+1})$ where each $s_j$ belongs to the finite set of cell states consisting of Zero, One, Signal, Gate, Wire and Blank.
background
The module builds cellular-automaton infrastructure for encoding SAT instances as local Boolean gadgets. CellState is the inductive type whose constructors are Zero, One, Signal, Gate, Wire and Blank; these label tape cells that carry Boolean values, propagating signals or gate markers. The module imports a general neighborhood construction from RecognitionLatticeFromRecognizer that returns the set of lattice cells sharing an observed label, and a distinction axiom from PrimitiveDistinction that supplies the underlying recognizer interface.
proof idea
The declaration is a plain record definition whose three fields are each typed by the CellState inductive. No tactics or lemmas are applied; the structure is introduced directly to serve as the domain of the subsequent extractNeighborhood and localRule definitions.
why it matters
This record supplies the input type for extractNeighborhood and localRule, which together implement the deterministic local update rule used to evaluate SAT clauses in linear time on the tape. It therefore sits inside the O(n^{1/3} log n) CA computation claimed in the module and feeds the LocalConfigSpace structure in RecogGeom.Locality that formalizes RG1. The construction adapts the Rule 110 universal CA to Recognition Science's balanced-parity encoding while preserving reversibility for ledger compatibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.