compAutomorphism_assoc_toFun
plain-language theorem explainer
Composition of recognition automorphisms is associative when restricted to their underlying action functions. Researchers formalizing gauge symmetries and quotient maps in recognition geometry cite this result to confirm the algebraic closure properties of the automorphism set. The proof is a one-line wrapper that reduces the claim directly to the definition of compAutomorphism and the associativity of function composition.
Claim. Let $T_1, T_2, T_3$ be bijective recognition-preserving maps (automorphisms) for a recognizer $r$. Then the underlying function of the composition $(T_1$ composed with $T_2)$ followed by $T_3$ equals the underlying function of $T_1$ followed by the composition of $T_2$ with $T_3$.
background
Recognition geometry equips a recognizer $r$ with transformations that preserve events, i.e., $R(T(c)) = R(c)$ for all configurations $c$. A RecognitionAutomorphism extends this to a bijective map equipped with an inverse that also preserves events, inducing well-defined actions on the recognition quotient. The module develops the algebraic operations on these maps, including composition and identity, to capture gauge-like redundancies invisible to the recognizer.
proof idea
This is a one-line wrapper proof. It applies simp only to the definition of compAutomorphism together with the standard associativity of function composition.
why it matters
The result supplies the associativity axiom for the composition operation on recognition automorphisms, completing the verification that these maps form a group. It directly supports the module's main results on symmetry-preserving maps and quotient actions, which interpret physical gauge symmetries as recognition equivalences. In the Recognition Science setting this step aligns with the forcing chain's self-similar fixed point and the eight-tick octave structure that generates discrete symmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.