idAutomorphism_comp_right_toFun
The theorem establishes that the identity automorphism is right-neutral under composition for the underlying function of any recognition automorphism T. Researchers formalizing the monoid structure of symmetries in recognition geometry cite this when confirming that composition with the identity leaves maps unchanged. The proof is a one-line term simplification that unfolds the definitions of compAutomorphism and idAutomorphism and invokes the standard function composition identity.
claimLet $T$ be a recognition automorphism. Then the function component of the composition of $T$ with the identity automorphism equals the function component of $T$.
background
Recognition geometry treats symmetries as bijective recognition-preserving maps. A RecognitionAutomorphism extends RecognitionPreservingMap by adding an inverse function together with left and right inverse properties that ensure bijectivity. The identity automorphism is defined by taking the identity function on configurations, with trivial event preservation and trivial inverses. Composition of two automorphisms is defined by composing their toFun components forward and their invFun components backward. An upstream result in CostAlgebra shows the analogous right-identity property for JAutomorphisms via direct extension.
proof idea
The proof is a one-line term wrapper that applies simp to the definitions of compAutomorphism, idAutomorphism, and the lemma Function.comp_id.
why it matters in Recognition Science
This result verifies the right unit property for the identity in the monoid of recognition automorphisms, completing the algebraic structure of composition, identity, and inverses described in the module. It supports the modeling of gauge symmetries as transformations invisible to the recognizer. The declaration sits inside the symmetry section that builds toward quotient maps and preservation theorems; no downstream uses are recorded yet.
scope and limits
- Does not establish the left identity property under composition.
- Does not prove event preservation for the composed map beyond the toFun equality.
- Does not address bijectivity or inverse properties of the result.
- Does not connect to the forcing chain, phi-ladder, or physical constants.
formal statement (Lean)
211theorem idAutomorphism_comp_right_toFun (T : RecognitionAutomorphism r) :
212 (compAutomorphism T idAutomorphism).toFun = T.toFun := by
proof body
Term-mode proof.
213 simp only [compAutomorphism, idAutomorphism, Function.comp_id]
214
215/-- Right inverse property (on toFun) -/