compAutomorphism_inv_left_eq_id
plain-language theorem explainer
The theorem establishes that composing any recognition automorphism T with its inverse recovers the identity map on configurations. Researchers formalizing gauge symmetries within recognition geometry cite it to confirm two-sided inverses. The proof is a one-line term application of function extensionality followed by the left-inverse lemma for the composed map.
Claim. Let $T$ be a bijective recognition-preserving map (automorphism) of recognizer $r$. Then the function induced by the composition of $T$ with its inverse equals the identity: $(T^{-1} circ T).mathsf{toFun} = mathsf{id}$.
background
Recognition geometry treats symmetries as maps that preserve recognizable events, i.e., $R(T(c)) = R(c)$ for all configurations $c$. The structure RecognitionAutomorphism extends the preserving-map definition by adding an explicit inverse function together with the left-inverse and right-inverse axioms. The module develops the algebraic operations (composition, identity, inverses) on these maps so that they induce well-defined actions on the recognition quotient, mirroring gauge redundancies that leave observables unchanged.
proof idea
The term proof first applies function extensionality to convert the equality of functions into a pointwise statement. It then directly invokes the sibling lemma compAutomorphism_inv_left_toFun, which unfolds the definition of composition and applies the left-inverse property already present in the RecognitionAutomorphism structure.
why it matters
The result verifies that inverses act as left identities, completing the minimal algebraic requirements for the set of recognition automorphisms to behave like a group. It directly supports the module's physical reading that gauge-equivalent configurations are indistinguishable to the recognizer. No downstream theorems are recorded yet, but the lemma closes one of the basic closure properties needed before quotient actions or physical interpretations can be stated rigorously.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.