cell_mem_own_neighborhood
plain-language theorem explainer
The theorem shows that the equivalence class of any configuration x under a primitive interface I lies inside the set of classes sharing the label that I assigns to x. Researchers building the pre-spatial recognition quotient lattice cite this to confirm cells respect finite-resolution observations. The proof is a one-line simplification that unfolds the neighborhood definition.
Claim. Let $I$ be a primitive interface on carrier $K$ and let $x$ belong to $K$. Then the cell of $x$ under $I$ belongs to the neighborhood of the label $I$ assigns to $x$.
background
The module constructs the recognition lattice as the quotient of carrier $K$ by the kernel of a primitive interface $I$, where $I$ maps configurations to labels in a finite set Fin n. A primitive interface consists of a positive natural number n together with an observation map observe : K → Fin n; two configurations are indistinguishable precisely when they receive the same label. The operation cellOf forms the equivalence class of x under the induced setoid, while neighborhood(label) collects all cells whose label equals the given value.
proof idea
The proof is a one-line wrapper that applies the definition of neighborhood.
why it matters
This membership fact supports the module claim that kernel-equivalence classes form a recognition quotient lattice inheriting finite-resolution neighborhoods from any primitive observer. It supplies the basic consistency property required before the lattice can be used in later constructions such as nontrivial recognition forcing a lattice or canonical equivalence for same-kernel interfaces. The result stays within the pre-spatial stage of the Recognition Science framework and does not yet invoke the forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.