RecognitionQuotient
plain-language theorem explainer
Recognition geometry begins with the quotient space obtained by collapsing configurations that produce identical outputs under a recognizer r : C → E. Researchers constructing charts, atlases, or composition maps on recognition data cite this as the base space C_R. The definition is realized by a direct application of the quotient constructor to the indistinguishability setoid.
Claim. For a recognizer $r : C → E$, the recognition quotient $C_R$ is the quotient set $C / ∼_r$, where $c_1 ∼_r c_2$ if and only if $r(c_1) = r(c_2)$.
background
The module constructs the recognition quotient as the space of equivalence classes under indistinguishability. Two configurations are identified precisely when the recognizer maps them to the same event in E. This rests on the upstream indistinguishability setoid, which supplies the equivalence relation and its reflexivity, symmetry, and transitivity properties.
proof idea
One-line wrapper that applies the Quotient constructor to the indistinguishableSetoid induced by the recognizer.
why it matters
This supplies the base space for atlas and chart constructions in recognition geometry. It is invoked by atlas_covers_quotient to guarantee covering, by chartOnQuotient to descend local coordinates, and by quotientMapLeft and quotientMapRight to project composite quotients. In the Recognition Science framework it enacts the collapse of states that cannot be told apart, consistent with the uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.