compSymmetry_assoc
plain-language theorem explainer
Composition of recognition-preserving maps is associative. Researchers formalizing the algebraic structure of symmetries in recognition geometry cite this to confirm that the maps form a monoid under the defined composition. The proof is a one-line wrapper that unfolds the composition definition and applies the associativity of function composition.
Claim. Let $T_1, T_2, T_3$ be recognition-preserving maps. Then the composition of the first two followed by the third equals the first composed with the composition of the second and third, where each composition is the pointwise function composition that preserves recognition events.
background
Recognition geometry treats symmetries as transformations of configurations that leave recognizable events unchanged. A recognition-preserving map consists of an underlying function $T: C → C$ together with the property that the recognizer's event map satisfies $R(T(c)) = R(c)$ for every configuration $c$ (RecognitionPreservingMap). The composition operation on two such maps is defined by composing their underlying functions and verifying that the event-preservation property holds by transitivity (compSymmetry). The module sets this structure in the context of gauge-like redundancies that are invisible to the recognizer, with the algebraic operations (composition, identity) mirroring the expected group-like behavior of physical symmetries.
proof idea
The proof is a one-line wrapper that applies simp to unfold compSymmetry and invoke the associativity of function composition.
why it matters
This theorem supplies the associativity axiom needed for the monoid of recognition-preserving maps, sitting alongside the identity map in the same module. It directly supports the physical reading of symmetries as transformations that induce well-defined maps on the recognition quotient while preserving observable events. In the Recognition Science framework it aligns with the requirement that structure-preserving operations respect the core recognition relation, providing a concrete algebraic layer for gauge redundancies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.