compAutomorphism_inv_right_toFun
Recognition automorphisms satisfy a right inverse property under composition: for any such T and configuration c, composing T with its inverse recovers c exactly. This result supports the construction of symmetry groups in recognition geometry and would be cited in proofs establishing that automorphisms form a group under composition. The short proof unfolds the composition definition and invokes the built-in right inverse axiom of the automorphism.
claimLet $T$ be a recognition automorphism of recognizer $r$. For every configuration $c$, the toFun component of the composition of $T$ with its inverse satisfies $(T ∘ T^{-1})(c) = c$.
background
Recognition geometry treats symmetries as maps preserving recognizable events on configurations. A RecognitionAutomorphism is a bijective recognition-preserving map equipped with an inverse function invFun together with left_inv and right_inv axioms ensuring bijectivity. The compAutomorphism operation composes two such automorphisms by composing their toFun maps while preserving the event condition via the underlying RecognitionPreservingMap structure. Upstream results include the definition of compAutomorphism itself and the comp_apply lemma from CostAlgebra that handles function composition in this setting.
proof idea
The proof is a one-line term-mode wrapper. It applies simp to unfold compAutomorphism, RecognitionAutomorphism.inv, and Function.comp_apply, then directly invokes the right_inv field of T on the input c.
why it matters in Recognition Science
This theorem is invoked by compAutomorphism_inv_right_eq_id to establish that the composition of an automorphism with its inverse acts as the identity map on toFun. It completes the algebraic closure for recognition automorphisms, confirming they form a group under composition. The result aligns with the module's treatment of gauge-like redundancies in recognition geometry, where such inverses ensure transformations remain invisible to the recognizer.
scope and limits
- Does not prove the corresponding left inverse property for the composition.
- Does not address specific physical interpretations or links to constants such as phi or alpha.
- Does not extend beyond the toFun component to the full structure equality.
- Does not depend on or reference the forcing chain or mass ladder constructions.
Lean usage
theorem compAutomorphism_inv_right_eq_id (T : RecognitionAutomorphism r) : (compAutomorphism T T.inv).toFun = id := by ext c; exact compAutomorphism_inv_right_toFun T cformal statement (Lean)
216theorem compAutomorphism_inv_right_toFun (T : RecognitionAutomorphism r) (c : C) :
217 (compAutomorphism T T.inv).toFun c = c := by
proof body
Term-mode proof.
218 simp only [compAutomorphism, RecognitionAutomorphism.inv, Function.comp_apply]
219 exact T.right_inv c
220
221/-- Left inverse property (on toFun) -/