recognition_lattice
plain-language theorem explainer
For any kernel label type, a recognition-lattice certificate exists: the kernel classes of a recognizer form the first recognition lattice. Cite this when working at the T0/T4 recognizer layer and needing the lattice induced by kernel equivalence. The public name is a one-line alias of the inhabitedness theorem that packages that certificate.
Claim. For every type $K$, the type of recognition-lattice certificates on $K$ is nonempty. Equivalently, a recognizer induces a recognition lattice whose classes are the recognizer's kernel classes (same-kernel interfaces yield canonically equivalent lattices).
background
Recognition Core aggregates the T0/T4 layer of the forcing chain: the recognizer, its indistinguishability quotient, the full recognition signature, and the completeness condition under which the signature fixes all physically relevant states. The module's stance is that a single Boolean observable is atomic, not complete; physical content sits in the admitted recognizer family.
A recognizer partitions states by what it can distinguish. Kernel classes are the equivalence classes of states that the recognizer cannot separate. The recognition lattice is the lattice structure on those classes: the first discrete geometry of recognition acts, before finer signature or gauge structure is imposed.
Upstream, recognitionLatticeCert_inhabited states that for every type $K$ the certificate type RecognitionLatticeCert K is nonempty, witnessed by the explicit constructor recognitionLatticeCert K. This abbrev re-exports that inhabitedness as the public citation name.
proof idea
One-line public alias. The body is exactly the upstream theorem that, for any type $K$, RecognitionLatticeCert K is nonempty, proved by exhibiting the canonical certificate recognitionLatticeCert K. No extra tactics or lemmas are applied at this layer.
why it matters
Listed among the module's public citation targets: a recognizer's kernel classes are the first recognition lattice, and same-kernel interfaces give canonically equivalent lattices. It anchors the lattice side of the recognizer/signature story at T0/T4, beside forced quotient, gauge-from-indistinguishability, signature completeness, recognizer refinement, and the induced logic.
In the forcing chain this is pre-geometry infrastructure: before J-uniqueness (T5), phi (T6), the eight-tick octave (T7), or D = 3 (T8), one needs a lattice of recognition classes. The declaration packages that existence so later geometry and composition results can treat the lattice as given rather than re-derived. No downstream edges are recorded yet; the value is as a stable public handle into the Foundation lattice certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.