compAutomorphism
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove associativity of the composition.
- Does not derive any numerical values or phi-ladder relations.
- Does not address continuous families of symmetries or Lie-algebra structure.
- Does not connect the construction to specific physical constants such as alpha or G.
Lean usage
obtain ⟨T₁, hT₁⟩ := h₁; obtain ⟨T₂, hT₂⟩ := h₂; use compAutomorphism T₂ T₁formal statement (Lean)
180def compAutomorphism (T₁ T₂ : RecognitionAutomorphism r) : RecognitionAutomorphism r where
181 toFun := T₁.toFun ∘ T₂.toFun
proof body
Definition body.
182 preserves_event := fun c => by
183 simp only [Function.comp_apply]
184 rw [T₁.preserves_event, T₂.preserves_event]
185 invFun := T₂.invFun ∘ T₁.invFun
186 left_inv := fun c => by
187 simp only [Function.comp_apply]
188 -- Goal: T₂.invFun (T₁.invFun (T₁.toFun (T₂.toFun c))) = c
189 have h1 : T₁.invFun (T₁.toFun (T₂.toFun c)) = T₂.toFun c := T₁.left_inv _
190 rw [h1, T₂.left_inv]
191 right_inv := fun c => by
192 simp only [Function.comp_apply]
193 -- Goal: T₁.toFun (T₂.toFun (T₂.invFun (T₁.invFun c))) = c
194 have h1 : T₂.toFun (T₂.invFun (T₁.invFun c)) = T₁.invFun c := T₂.right_inv _
195 rw [h1, T₁.right_inv]
196
197/-! ## Algebraic Properties of Automorphisms -/
198
199/-- Composition of automorphisms is associative (on toFun) -/