recognitionLatticeCert_inhabited
plain-language theorem explainer
RecognitionLatticeCert K is inhabited for any type K, establishing existence of a recognition lattice certificate from any primitive interface. Researchers formalizing Recognition Geometry cite this to ground the pre-spatial quotient lattice before metric or spatial structure. The proof is a one-line term that directly supplies the structure term recognitionLatticeCert K.
Claim. For any type $K$, the structure RecognitionLatticeCert($K$) is inhabited. Equivalently, there exists a certificate containing a map from non-trivial recognition to a primitive interface with non-empty lattice, the kernel equivalence relation on that interface, a labeling of every lattice cell by an element of Fin $I.n$, and uniqueness of the lattice up to same-kernel equivalence of interfaces.
background
The module RecognitionLatticeFromRecognizer turns the structural claim of Recognition Geometry into a Lean theorem: a recognizer's kernel-equivalence classes form the first recognition lattice. This lattice is the quotient of the carrier by the primitive observer's indistinguishability kernel; cells are equivalence classes of configurations the recognizer cannot distinguish. Finite resolution is inherited from the finite event codomain Fin $n$ of the interface. RecognitionLatticeCert $K$ packages four properties: existence from non-trivial recognition, kernel equivalence, cell labeling, and uniqueness under SameKernel. Upstream, LogicNat supplies the universal iteration object interpreted into lattice cells, while PrimitiveInterface and kernel constructions come from ObserverFromRecognition and PrimitiveDistinction.
proof idea
The proof is a one-line term that applies the structure constructor recognitionLatticeCert $K$ to witness Nonempty (RecognitionLatticeCert $K$). No tactics are used; the term directly assembles the four fields from the module's prior definitions of primitive interfaces, kernels, neighborhoods, and same-kernel uniqueness.
why it matters
This theorem confirms existence of the recognition quotient lattice, completing the chain non-trivial recognition to primitive interface to kernel equivalence to quotient cells to finite-resolution neighborhoods. It feeds the interpretation of LogicNat into the lattice and supplies the pre-spatial foundation for Recognition Geometry. In the broader framework it precedes the phi-ladder, eight-tick octave, and derivation of $D=3$, remaining strictly pre-metric and pre-spatial. The module summary explicitly lists this as the Lean bridge from observer to lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.