RecognitionLattice
plain-language theorem explainer
The recognition lattice is the quotient of configurations under the indistinguishability kernel of a primitive interface. Foundational work on recognition geometry cites this construction to obtain the first discrete observer structure from finite-resolution events. The definition is a direct one-line quotient by the interface setoid.
Claim. Let $I$ be a primitive interface on carrier $K$, consisting of a positive integer $n$ and an observation map $K$ to Fin $n$. The recognition lattice is the quotient $K/!sim$, where $x !sim y$ if and only if the observation map assigns $x$ and $y$ the same label in Fin $n$.
background
A primitive interface on carrier $K$ is a finite-resolution recognizer: it consists of a positive integer $n$ together with an observation map from $K$ to Fin $n$. The interface kernel declares two configurations indistinguishable precisely when they receive the same observed label. The module documentation states that this construction turns the structural claim of Recognition Geometry into a Lean theorem: a recognizer's kernel-equivalence classes are the first recognition lattice. The lattice is pre-spatial; it is the quotient of the carrier by the primitive observer's indistinguishability kernel, inheriting finite resolution from the codomain Fin $n$.
proof idea
The definition is a one-line wrapper that applies the Quotient constructor directly to the setoid produced by interfaceSetoid I.
why it matters
This definition supplies the carrier for all subsequent lattice operations, including cell labels, neighborhoods, and interpretations of LogicNat. It realizes the module claim that kernel-equivalence classes form the first recognition lattice. Downstream results such as latticeEquivOfSameKernel and logicNat_interprets_into_lattice depend on it to establish uniqueness up to canonical equivalence and the existence of interpretations into the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.