quotientEventMap_spec
plain-language theorem explainer
The theorem asserts that the lifted event map on the recognition quotient recovers the original recognition function R after applying the quotient projection to any configuration. Researchers in recognition geometry cite this commutativity to justify replacing the configuration space with its quotient while preserving event data. The proof is a direct reflexivity because the lift is defined via Quotient.lift to enforce the equality by construction.
Claim. Let $R : C → E$ be a recognition map. Let $π : C → C_R$ be the canonical projection onto the recognition quotient $C_R = C / ∼$, where $c_1 ∼ c_2$ iff $R(c_1) = R(c_2)$. The lifted event map $¯R : C_R → E$ satisfies $¯R(π(c)) = R(c)$ for every $c ∈ C$.
background
The recognition quotient $C_R$ is formed by collapsing configurations in $C$ that are indistinguishable under the recognition map $R : C → E$, i.e., $c_1 ∼ c_2$ precisely when $R(c_1) = R(c_2)$. The quotient event map is the unique map $¯R$ induced by $R$ on the quotient, obtained by lifting through the universal property of quotients. This construction lives in the Recognition Geometry module, whose module documentation states that the quotient collapses configurations that cannot be told apart by the recognizer while preserving the event structure.
proof idea
The proof is a one-line reflexivity. The definition of quotientEventMap as Quotient.lift r.R (fun _ _ h => h) is constructed exactly so that the diagram commutes, making the equality hold definitionally without further lemmas.
why it matters
This commutativity is the defining property that lets the quotient serve as a faithful replacement for the original space in event-based reasoning. It is invoked directly in the downstream construction of quotient_equiv_image, which establishes that the quotient is isomorphic to the image of R. Within the Recognition Science framework the result confirms that the recognition quotient respects the event map, supporting the broader derivation of geometry from recognition without loss of observable structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.