latticeEquivOfSameKernel
plain-language theorem explainer
If two primitive interfaces share the same kernel, their recognition lattices are canonically equivalent via the identity on representatives. Researchers in recognition geometry cite this to establish that lattice structure depends only on the indistinguishability relation. The construction lifts the identity through Quotient.map using the kernel equivalence for well-definedness, with both inverses obtained by quotient induction and reflexivity.
Claim. If primitive interfaces $I$ and $J$ on a carrier $K$ satisfy $I.kernel(x,y)leftrightarrow J.kernel(x,y)$ for all $x,y$, then the recognition lattices are canonically equivalent: RecognitionLattice$(I)≃$RecognitionLattice$(J)$.
background
The recognition lattice is the quotient of the carrier by the interfaceSetoid, which is the equivalence relation induced by the kernel of a primitive interface. A primitive interface on $K$ consists of a positive natural number $n$ and an observation map $K→$Fin $n$; the kernel declares two configurations indistinguishable exactly when they map to the same event. SameKernel is the proposition that two interfaces declare identical pairs indistinguishable.
proof idea
The definition constructs the equivalence by Quotient.map applied to the identity function. The forward map invokes SameKernel to confirm the map respects the quotient relation; the inverse map does likewise. Left and right inverses follow by Quotient.inductionOn on an arbitrary cell followed by reflexivity.
why it matters
This supplies the uniqueness clause inside recognitionLatticeCert, which assembles existence from nontrivial recognition, kernel equivalence, cell labeling, and the LogicNat interpretation. In the Recognition Science framework it confirms that the pre-spatial lattice is determined solely by the kernel, closing the step from any primitive recognizer to its lattice up to canonical equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Geometry rebuilt as a quotient of what measurements can distinguish
"Theorem 1: The induced map R̄ : C_R → E is injective. ... distinct observable states correspond to distinct events, and no further distinctions exist within C_R beyond those encoded by R"