symmetryQuotientMap
plain-language theorem explainer
A recognition-preserving map induces a well-defined function on the recognition quotient of indistinguishable configurations. Researchers modeling gauge symmetries in recognition geometry cite this when descending transformations to observables. The definition constructs the map via Quotient.lift and discharges well-definedness by invoking symmetry_preserves_indistinguishable on the equivalence relation.
Claim. Let $T: C → C$ be a recognition-preserving map for recognizer $r$, so that $r.R(T(c)) = r.R(c)$ for all $c$. Then $T$ induces a map $C_R → C_R$ on the recognition quotient $C_R = C / ∼_r$ by sending the class $[c]$ to $[T(c)]$.
background
Recognition geometry starts from a recognizer $r$ with configuration space $C$ and event map $R$. RecognitionPreservingMap is the structure whose toFun component satisfies the event-preservation condition $r.R(T(c)) = r.R(c)$ for every $c$; this encodes the gauge-like redundancies invisible to the recognizer. The recognition quotient RecognitionQuotient r is the set $C_R$ obtained by quotienting $C$ by the indistinguishability relation, with canonical projection recognitionQuotientMk r. Upstream, quotientMk_eq_iff states that recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂ if and only if c₁ and c₂ are indistinguishable under r.
proof idea
The definition applies Quotient.lift to the function sending each configuration c to recognitionQuotientMk r (T c). The required equality condition on representatives is supplied directly by symmetry_preserves_indistinguishable T h, which converts an indistinguishability hypothesis into the corresponding equality of quotient classes.
why it matters
This definition supplies the action of symmetries on the quotient, which is invoked by the downstream results compSymmetry_quotient_action, idSymmetry_quotient_action and symmetryQuotientMap_mk. It realizes the gauge-symmetry interpretation stated in the module documentation: transformations that leave events unchanged descend to well-defined maps on observables. Within the Recognition Science framework it completes the algebraic structure needed before one can discuss automorphism groups or gauge equivalence classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.