Neighborhood
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not encode the update function or transition table.
- Does not impose finiteness or boundary conditions on the tape.
- Does not prove any locality or invariance properties of the triple.
- Does not relate the structure to the RecognitionLattice neighborhood set.
formal statement (Lean)
58structure Neighborhood where
59 left : CellState
60 center : CellState
61 right : CellState
62
63/-- Extract neighborhood from tape at position i -/