compAutomorphism
plain-language theorem explainer
Defines the composition of two recognition automorphisms by setting the forward map to the composition of their toFun functions and constructing the inverse and preservation properties from the inputs. Researchers modeling gauge symmetries in recognition geometry cite this to equip the set of automorphisms with a group operation. The definition is a direct structural construction that applies function composition and reuses the left and right inverse axioms of each input.
Claim. Let $T_1$ and $T_2$ be bijective recognition-preserving maps (automorphisms) for recognizer $r$. Their composition $T_1 circ T_2$ is the automorphism whose action on a configuration $c$ is $T_1(T_2(c))$, whose inverse action is $T_2^{-1} circ T_1^{-1}$, and which satisfies the left and right inverse identities by direct substitution of the corresponding identities for $T_1$ and $T_2$.
background
RecognitionAutomorphism extends RecognitionPreservingMap by adding an inverse function together with left_inv and right_inv axioms that enforce bijectivity while preserving events. In the Recognition Geometry module, such automorphisms represent symmetries: transformations of configurations that leave the recognizable structure (events) unchanged and therefore descend to well-defined maps on the recognition quotient, corresponding to gauge redundancies invisible to the recognizer. The construction draws on the Composition axiom (the multiplicative d'Alembert equation) and the comp_apply lemma for function composition in the underlying cost algebra.
proof idea
The definition is a direct structural construction. It sets toFun to the composition of the input toFun maps, invFun to the reverse composition, and then proves the three required fields by applying simp on Function.comp_apply followed by rewriting with the left_inv or right_inv axiom of the appropriate input automorphism.
why it matters
This supplies the binary operation that turns the collection of recognition automorphisms into a group, directly enabling the associativity theorem, the left and right inverse theorems, and the transitivity proof for gauge equivalence. It completes the algebraic layer of the symmetry theory in the module and aligns with the Recognition Composition Law by ensuring that composed symmetries remain recognition-preserving. The construction is used in gaugeEquivalent_trans to witness transitivity of equivalence by composing the witnessing automorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.