compAutomorphism_inv_left_toFun
plain-language theorem explainer
The left inverse property for composed recognition automorphisms states that applying an automorphism T followed by its inverse recovers the original configuration c. Researchers establishing group structure for gauge symmetries in recognition geometry cite this when verifying inverses under composition. The proof is a term reduction that unfolds the composition and applies the left inverse axiom of the automorphism structure directly.
Claim. Let $T$ be a recognition automorphism of recognizer $r$. For any configuration $c$, the toFun component of the composition of $T$ with its inverse satisfies $(T^{-1} circ T)(c) = c$.
background
RecognitionAutomorphism extends RecognitionPreservingMap to a bijective map on configurations that preserves events under the recognizer $r$, equipped with an explicit inverse function satisfying the left_inv axiom invFun (toFun c) = c and the right_inv axiom. Recognition-preserving maps are those transformations T such that R(T(c)) = R(c) for all c, inducing well-defined actions on the recognition quotient. The local setting in Recognition Geometry treats these as gauge-like redundancies invisible to the recognizer, with algebraic operations including composition defined via compAutomorphism.
proof idea
This is a term-mode proof. It applies simp to unfold the definitions of compAutomorphism, RecognitionAutomorphism.inv, and Function.comp_apply, then invokes exact on the left_inv field of the input T.
why it matters
This declaration is used directly by compAutomorphism_inv_left_eq_id to lift the pointwise equality to the full function identity (T^{-1} circ T) = id. It completes the inverse axioms for recognition automorphisms, supporting the module's physical interpretation of symmetries as gauge equivalences. In the Recognition Science framework it closes the algebraic structure needed for symmetries that preserve recognizable events, consistent with the core idea that such maps reflect redundancies invisible to the recognizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.