compAutomorphism_inv_right_eq_id
plain-language theorem explainer
Recognition automorphisms satisfy the right inverse law under composition, so that T composed with its inverse induces the identity function on configurations. Researchers modeling gauge redundancies or quotient spaces in recognition geometry cite this to confirm that automorphisms form a group under composition. The proof reduces the functional equality to pointwise identity via extensionality and invokes the dedicated inverse-action lemma.
Claim. Let $T$ be a recognition automorphism. Then the function component of the composition of $T$ with its inverse equals the identity map: $(T ∘ T^{-1}).toFun = id$.
background
Recognition geometry treats symmetries as maps that preserve recognizable events $R(T(c)) = R(c)$. The structure RecognitionAutomorphism extends RecognitionPreservingMap by adding an inverse function together with the left-inverse and right-inverse axioms, making the map bijective on the configuration space $C$. The module develops the algebraic operations of composition, identity, and inversion on these maps to capture gauge-like redundancies invisible to the recognizer.
proof idea
The proof is a term-mode wrapper. Function extensionality reduces the equality of functions to pointwise equality on configurations. The resulting goal is discharged directly by the lemma compAutomorphism_inv_right_toFun, which applies the right-inverse axiom of the automorphism.
why it matters
The result verifies the right-inverse law required for the algebraic structure of recognition automorphisms, supporting their interpretation as gauge symmetries that leave observable events unchanged. It belongs to the module's development of composition and inverses, which parallels the physical notion that such transformations induce well-defined maps on the recognition quotient. No open questions are resolved here, but the identity law is a prerequisite for any group-theoretic treatment of symmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.