pointLattice
plain-language theorem explainer
The point lattice is the recognition quotient induced by a single distinguished point via its minimal two-outcome interface. Researchers constructing the pre-spatial layer of Recognition Science cite it as the base case showing that any primitive recognizer generates a lattice of kernel-equivalence classes. The definition is a direct one-line wrapper that feeds the pointInterface into the general RecognitionLattice quotient constructor.
Claim. Let $K$ be a carrier set and $x_0$ a distinguished element. The point lattice is the quotient $K / {sim}$, where two elements are equivalent precisely when the two-outcome recognizer that returns 1 if and only if its argument equals $x_0$ cannot distinguish them.
background
RecognitionLattice is the quotient of the carrier by the interface kernel (the indistinguishability relation induced by a PrimitiveInterface). pointInterface is the canonical two-outcome recognizer on $K$ that returns the label 1 exactly on the reference point $x_0$ and 0 otherwise; its finite event codomain is Fin 2. The module states that this construction yields the first recognition lattice: the quotient of configurations by the primitive observer's indistinguishability kernel, inheriting finite resolution from the event labels.
proof idea
One-line wrapper that applies the RecognitionLattice constructor directly to pointInterface x₀.
why it matters
This supplies the minimal lattice forced by any single named distinction and thereby realizes the module claim that a recognizer's kernel-equivalence classes form the first recognition lattice. It precedes metric or dimensional structure and supports the uniqueness-up-to-canonical-equivalence results appearing later in the same module. The construction remains pre-spatial, consistent with the forcing chain before T8 (D = 3) and before any appeal to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.