quotientMk_eq_iff
plain-language theorem explainer
The recognition quotient identifies two configurations precisely when they are indistinguishable by the recognizer. Researchers in recognition geometry cite this to equate quotient equality with the underlying indistinguishability relation in proofs of charts, composite maps, and the fundamental theorem. The proof is a one-line term that applies Quotient.eq to the indistinguishableSetoid.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. Let $C_R$ be the recognition quotient and let $c_1, c_2 : C$. Then the images of $c_1$ and $c_2$ under the canonical projection to $C_R$ are equal if and only if $c_1$ is indistinguishable from $c_2$ under $r$.
background
The Recognition Geometry module defines the recognition quotient as $C_R = C / {~}$, where the equivalence collapses configurations that cannot be told apart by the recognizer. The indistinguishability setoid is the setoid on $C$ whose relation is Indistinguishable $r$, which holds precisely when the recognizer assigns the same event to both inputs. The canonical projection is the map sending each configuration to its class via Quotient.mk on that setoid.
proof idea
The proof is a one-line term that invokes Quotient.eq instantiated at the indistinguishableSetoid $r$. This Mathlib lemma directly converts equality of quotient elements into membership in the underlying relation.
why it matters
This lemma supplies the explicit characterization used to define the fundamental theorem of recognition geometry, which equates quotient classes with identical events. It is applied in chart well-definedness, in the left and right quotient maps for composite recognizers, in the bijectivity result for separating recognizers, and in the extended fundamental theorem for composites. In the Recognition Science framework it anchors the construction of observable space as the quotient by indistinguishability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.