recognitionQuotientMk
plain-language theorem explainer
The canonical projection that sends each configuration c to its class in the quotient C_R under the recognizer's indistinguishability relation. Researchers building charts and composition maps on recognition spaces cite this to obtain well-defined maps on collapsed states. The definition is a direct one-line application of the Quotient.mk constructor to the setoid from indistinguishableSetoid.
Claim. The canonical projection map $C_R = C / {}_r$ sending each configuration $c$ to its equivalence class $[c]$ under the indistinguishability relation induced by recognizer $r$.
background
The recognition quotient is defined as $C_R = C / {}_r$ where two configurations are equivalent precisely when the recognizer maps them to the same event. RecognitionQuotient is the quotient type built from the indistinguishableSetoid, which packages the Indistinguishable relation together with its equivalence proof. The module sets the local context by collapsing configurations that cannot be distinguished, mirroring quotient constructions such as those for integers and rationals from logic pairs.
proof idea
One-line wrapper that applies Quotient.mk to the indistinguishableSetoid r and the input configuration c.
why it matters
This projection is the basic map feeding atlas_covers_quotient, chartOnQuotient, and the left and right quotient maps in composition. It realizes the core collapse step of the recognition geometry construction, allowing downstream results to treat classes rather than raw configurations. The definition closes the interface between the setoid and the quotient type used across the RecogGeom layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.