compSymmetry
plain-language theorem explainer
Composition of two recognition-preserving maps yields another such map by applying the underlying functions in sequence. Gauge symmetry researchers in recognition geometry cite this when constructing the monoid of symmetries. The definition directly supplies the composed function and verifies event preservation by rewriting the individual preservation properties.
Claim. Let $T_1$ and $T_2$ be recognition-preserving maps for recognizer $r$. Their composition is the map sending each configuration $c$ to $T_1(T_2(c))$, which preserves the recognizer's events.
background
Recognition geometry treats symmetries as transformations that leave the recognizer's events unchanged. A recognition-preserving map is a structure consisting of a function toFun from configurations to configurations together with a proof that the recognizer's event predicate R satisfies R(toFun c) = R c for every c. Such maps induce well-defined actions on the recognition quotient C_R, as described in the module documentation on gauge-like redundancies invisible to the recognizer.
proof idea
The definition constructs the RecognitionPreservingMap structure by setting toFun to the function composition T₁.toFun ∘ T₂.toFun. The preserves_event field is discharged by applying simp to unfold the composition and then rewriting with the preservation hypotheses of T₁ and T₂.
why it matters
This definition supplies the binary operation that turns the collection of recognition-preserving maps into a monoid. It is invoked by compSymmetry_assoc to establish associativity, by compSymmetry_quotient_action to show compatibility with the quotient map, and by the identity-neutrality lemmas. In the Recognition Science framework it realizes the gauge symmetry structure described in the module documentation, where transformations invisible to the recognizer form the symmetry group acting on configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.