quotientEventMap
The quotient event map is the function from the recognition quotient to the event space that sends each indistinguishability class to the common event value of its members. Researchers establishing the universal property of the recognition quotient or the injectivity of the induced observable map cite this construction to factor the recognizer through the quotient. The definition is a direct application of the standard quotient lift to the recognizer map, which is valid because the indistinguishability relation is exactly the kernel of that map
claimLet $r: C → E$ be a recognizer. The induced map $¯r: C_R → E$ on the recognition quotient $C_R = C / ∼_r$ is defined by $¯r([c]) = r(c)$, where $∼_r$ is the indistinguishability equivalence relation on configurations.
background
The recognition quotient is the set of equivalence classes of configurations under the indistinguishability relation induced by a recognizer $r: C → E$, where two configurations are equivalent precisely when they map to the same event. The module defines this quotient as the quotient type by the indistinguishable setoid of $r$, together with the canonical projection from $C$ to the quotient classes.
proof idea
The definition applies the standard Quotient.lift constructor directly to the recognizer map, supplying the trivial proof that equal events witness the equivalence relation. This produces a well-defined function on quotient classes without further computation.
why it matters in Recognition Science
This definition supplies the factored observable map whose injectivity is the content of Pillar 1 and the universal property theorem in the recognition geometry foundations. Those results establish that the recognition quotient is the coequalizer of the indistinguishability relation and the finest quotient through which any recognizer factors injectively. In the Recognition Science framework the construction realizes the collapse of indistinguishable configurations while preserving the event space, feeding the injectivity statements that identify the quotient with the image of the recognizer.
scope and limits
- Does not prove that the induced map is injective.
- Does not construct the indistinguishability relation or the quotient type itself.
- Does not address surjectivity of the projection onto the quotient.
- Does not treat composition of multiple recognizers.
formal statement (Lean)
56def quotientEventMap : RecognitionQuotient r → E :=
proof body
Definition body.
57 Quotient.lift r.R (fun _ _ h => h)
58
59/-- The quotient event map makes the diagram commute -/