idSymmetry_comp_right
plain-language theorem explainer
The identity map is right-neutral under composition of recognition-preserving maps. Researchers formalizing gauge symmetries or monoid structures on event-preserving transformations would cite this when verifying algebraic closure. The proof is a one-line term simplification that unfolds the composition and identity definitions and applies the standard right-identity law for function composition.
Claim. For any recognition-preserving map $T$, the composition of $T$ with the identity map equals $T$.
background
Recognition geometry studies transformations on a configuration space $C$ equipped with a recognizer $r$ that extracts events. A recognition-preserving map is a function $T: C → C$ satisfying $r.R(T(c)) = r.R(c)$ for every configuration $c$, so that observable events remain unchanged. The module develops the induced algebraic structure on these maps, including composition and the identity element, in the setting where symmetries correspond to gauge redundancies invisible to the recognizer.
proof idea
The proof is a term-mode simplification that expands the definitions of composition and identity, then reduces via the library fact that right-composition with the identity function is the identity.
why it matters
This result supplies the right-unit axiom for the monoid of recognition-preserving maps, supporting the claim that symmetries form a monoid under composition. It directly implements the algebraic structure outlined in the module documentation for gauge-like transformations that preserve events. The theorem closes a basic requirement before quotient constructions or invertibility questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.