latticeEquivOfSameKernel_cell
plain-language theorem explainer
If two primitive interfaces share the same kernel, the canonical map between their recognition lattices sends the cell generated by any configuration in the first interface to the cell generated by the same configuration in the second. Researchers formalizing the pre-spatial quotient lattice in Recognition Science cite this when showing that the lattice depends only on the indistinguishability kernel. The proof is a one-line reflexivity that follows directly from the cellwise definition of the equivalence.
Claim. Let $I$ and $J$ be primitive interfaces on a carrier $K$ such that $I$ and $J$ induce identical kernel relations on $K$. For any configuration $x$ in $K$, the canonical equivalence between the two recognition lattices maps the cell of $I$ containing $x$ to the cell of $J$ containing $x$.
background
SameKernel holds when two primitive interfaces make exactly the same distinctions invisible, i.e., their kernel relations coincide on every pair of configurations. The recognition lattice is the quotient of the carrier by this kernel; its cells are the equivalence classes of configurations that the interface cannot separate. The module constructs this quotient for any primitive interface and shows that the resulting lattice is independent of the choice of interface once the kernel is fixed.
proof idea
The proof is a direct reflexivity step. The canonical equivalence latticeEquivOfSameKernel is defined to act cellwise on configurations, so applying it to cellOf I x yields cellOf J x by construction whenever the kernels agree.
why it matters
This result supplies the uniqueness clause for the recognition quotient lattice: lattices arising from interfaces with identical kernels are canonically equivalent. It completes the structural claim in the module that kernel-equivalence classes form the first recognition lattice before metric or spatial structure is imposed. The theorem therefore anchors the pre-spatial stage of the Recognition Geometry construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.