compSymmetry_toFun
plain-language theorem explainer
The declaration states that the underlying function of the composition of two recognition-preserving maps is exactly the ordinary composition of those functions. Researchers constructing the algebraic structure of symmetries in recognition geometry cite it when verifying that composed transformations act pointwise as expected on configurations. The proof is a one-line reflexivity that follows immediately from the definition of the composition operation.
Claim. Let $T_1$ and $T_2$ be recognition-preserving maps for a recognizer $r$. Then the underlying function of their composition satisfies $(T_1 ∘ T_2)(c) = T_1(T_2(c))$ for every configuration $c$.
background
Recognition geometry studies transformations of configurations that leave the recognizer's event assignment unchanged. A recognition-preserving map consists of a function toFun : C → C together with the property that the recognizer applied to the image equals the recognizer applied to the original configuration. The composition operation on these maps is defined by composing the underlying functions and checking that the result still satisfies the preservation property.
proof idea
The proof is a direct reflexivity. It holds because the composition is constructed precisely so that its toFun component equals the ordinary function composition of the two input maps.
why it matters
The result supplies the concrete action of the composition operation on the set of recognition-preserving maps, which is required before one can speak of a symmetry group or verify associativity. It sits inside the module that equips recognition geometry with its basic algebraic structure of symmetries, directly supporting the gauge-symmetry interpretation given in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.