neighborhood
plain-language theorem explainer
The neighborhood collects all cells of the recognition lattice sharing one observed label from a primitive interface. Researchers modeling discrete observation or local rules on quotients cite it when extracting finite-resolution subsets. It is realized directly as the set of lattice cells whose label equals the input.
Claim. For a primitive interface $I$ on carrier $K$ with finite codomain of size $n$ and a label $l$ in the set of $n$ outcomes, the neighborhood of $l$ is the set of all equivalence classes $c$ in the recognition quotient lattice such that the label of $c$ equals $l$.
background
The module constructs the recognition lattice as the quotient of the carrier by the indistinguishability kernel of a primitive interface. A primitive interface consists of a positive natural number $n$ together with an observation map sending each configuration to an element of the finite set of $n$ outcomes. The recognition lattice is then the set of equivalence classes under the kernel of this map, yielding a pre-spatial structure whose cells inherit finite resolution from the event codomain.
proof idea
This is a one-line definition that directly forms the set of all cells in the recognition lattice whose label matches the given input label.
why it matters
This definition supplies the finite-resolution neighborhoods required by the recognition lattice construction, feeding directly into results such as cell membership in its own neighborhood and applications in cellular automata for local rules. It completes the module's claim that kernel-equivalence classes form the first recognition lattice with finite event labels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.