compAutomorphism_inv_right_toFun
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.