recognitionLatticeCert
plain-language theorem explainer
The definition constructs a bundled certificate for any carrier type K that asserts existence of a recognition lattice from nontrivial recognition, equivalence of kernels, finite labeling of every cell, canonical equivalence of lattices for same-kernel interfaces, and interpretation of the iteration object into the lattice. Foundation builders in Recognition Science cite it to access the full set of lattice properties at once. The construction is a direct structure definition that populates each field from a supporting theorem.
Claim. For any type $K$, define the certificate $C_K$ by the clauses: nontrivial recognition on $K$ yields a primitive interface $I$ whose recognition lattice is nonempty; the kernel of every primitive interface is an equivalence relation; every cell of the recognition lattice of $I$ carries a label in the finite set of size $I.n$ that places it in the corresponding neighborhood; interfaces sharing the same kernel have canonically equivalent recognition lattices; and, for any base point and successor map on $K$, the iteration object admits a map into the lattice sending the identity to the base cell and each successor step to the image cell.
background
The module converts the structural claim that a recognizer's kernel-equivalence classes form the first recognition lattice into a single certificate object. This lattice is the quotient of the carrier by the primitive observer's indistinguishability kernel and remains pre-spatial, inheriting finite resolution from the finite event codomain. PrimitiveInterface supplies the kernel relation together with the finite event count $n$; RecognitionLattice I is the quotient set; neighborhoods are the preimages under the labeling map to Fin I.n.
proof idea
The definition is a direct structure constructor. It assigns the from_nontrivial field to the theorem that nontrivial recognition forces a lattice, the kernel_equiv field to the theorem establishing that every kernel is an equivalence, the every_cell_labeled field to the theorem that every cell carries a finite label, the same_kernel_unique field to the definition of canonical equivalence for same-kernel interfaces, and the logicNat_interpretation field to the theorem supplying the interpretation map for the iteration object.
why it matters
The certificate collects the core lattice properties into one object and is used directly to prove that a RecognitionLatticeCert exists for every carrier. It realizes the module's claim that kernel-equivalence classes constitute the first recognition lattice, supplying the pre-spatial foundation before metric or dimensional structure appears. It supports the Recognition Composition Law by guaranteeing a well-defined quotient and the forcing chain by providing the lattice on which later steps (T5 uniqueness, T7 octave) can act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.