symmetryQuotientMap_mk
plain-language theorem explainer
Recognition-preserving maps descend to well-defined actions on the recognition quotient: the image of the class of c under the induced map equals the class of the image of c. Gauge symmetry modelers cite this when confirming invariance of recognition events under transformations. The equality holds by reflexivity on the quotient construction.
Claim. Let $T$ be a map from configurations to configurations that preserves recognition events under recognizer $r$. Then for any configuration $c$, the induced quotient map satisfies $T([c]_r) = [T(c)]_r$.
background
Recognition geometry treats symmetries as transformations preserving the recognizable structure of configurations. A RecognitionPreservingMap consists of a function toFun : C → C together with the property that the recognizer's event function R satisfies R(toFun c) = R c for all c. The module sets this as the foundation for gauge-like redundancies invisible to the recognizer, inducing maps on the quotient C_R.
proof idea
This is a one-line term-mode proof applying reflexivity to the definition of the symmetry quotient map, which is constructed precisely to satisfy the stated equality.
why it matters
The result confirms that symmetries act consistently on equivalence classes of configurations, supporting the physical view of gauge symmetries as recognition-preserving transformations. It completes the basic algebraic structure for symmetries in the Recognition Geometry module, linking to the core idea that such maps reflect redundancies in observable events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.