RecognitionLatticeCert
plain-language theorem explainer
The RecognitionLatticeCert structure bundles five properties that certify the existence and basic features of the recognition lattice generated by any primitive interface on a carrier K. A researcher working on the Recognition Science foundation would cite it when confirming that kernel equivalence classes form a pre-spatial lattice with finite labels and admit an interpretation of the iteration object LogicNat. The declaration is a structure definition that directly lists the five field propositions, each supplied by a sibling lemma in thesame
Claim. A certificate for the recognition lattice on a carrier $K$ consists of: (1) nontrivial recognition on $K$ yields a primitive interface $I$ whose recognition lattice (the quotient by the kernel) is nonempty; (2) the kernel of every primitive interface is an equivalence relation; (3) every cell in the lattice of $I$ lies in the neighborhood of some label in $Fin(I.n)$; (4) interfaces with identical kernels have canonically isomorphic lattices; (5) for any primitive interface $I$, base point, and step function there exists a map from LogicNat into the lattice sending the identity to the base cell and each successor to the corresponding iterated cell.
background
The recognition lattice is the quotient of the carrier by the interface kernel, i.e., the set of equivalence classes of configurations that a primitive observer cannot distinguish. SameKernel holds precisely when two interfaces induce the same indistinguishability relation, which immediately yields canonically equivalent quotients. The module presents this quotient as the first recognition lattice: pre-spatial, inheriting finite resolution from the event codomain $Fin n$, and equipped with an interpretation of the universal iteration object LogicNat. LogicNat itself is the inductive type generated by an identity constructor and a successor constructor, representing the smallest orbit closed under the generator as forced by the Law of Logic.
proof idea
The declaration is a structure definition that packages five propositions as fields. No proof body is present; each field is a statement whose validity is supplied by separate sibling lemmas: nontrivial_recognition_forces_lattice for the first, kernel_is_equivalence for the second, every_cell_has_label for the third, latticeEquivOfSameKernel for the fourth, and logicNat_interprets_into_lattice for the fifth.
why it matters
This certificate completes the structural claim that a recognizer's kernel-equivalence classes constitute the first recognition lattice. It is instantiated by the definition recognitionLatticeCert, which supplies concrete witnesses for each field, and is shown to be inhabited by recognitionLatticeCert_inhabited. In the Recognition Science framework it marks the transition from the recognizer to the pre-spatial lattice stage, prior to the emergence of metric structure or the forcing chain that yields $D=3$. It leaves open how the finite lattice embeds into continuous space when resolution is increased.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.