idAutomorphism_comp_left_toFun
The identity automorphism acts as left neutral under composition, so that the toFun of idAutomorphism composed with any recognition automorphism T equals T's own toFun. Workers formalizing the monoid of symmetries in recognition geometry cite this when verifying neutral elements. The proof is a one-line simp that unfolds the composition definition and applies the standard function identity lemma.
claimLet $T$ be a bijective recognition-preserving map (automorphism). Then the function component of the composition of the identity automorphism with $T$ satisfies $(idAutomorphism ∘ T).toFun = T.toFun$.
background
Recognition geometry treats symmetries as bijective recognition-preserving maps on configurations that leave recognizable events unchanged. The structure RecognitionAutomorphism extends RecognitionPreservingMap with an inverse function satisfying the usual left and right inverse axioms. The module sets up composition of such maps to induce well-defined actions on the recognition quotient, mirroring gauge redundancies in physics. An upstream analogue appears in CostAlgebra.id_comp, which states that composing any JAut with the identity on the right recovers the original map.
proof idea
One-line wrapper that applies simp to the definitions of compAutomorphism and idAutomorphism, then reduces via the standard Function.id_comp lemma on function composition.
why it matters in Recognition Science
The result supplies the left-neutral property needed for the monoid of recognition automorphisms, pairing with the right-neutral companion and associativity lemmas in the same module. It directly supports the algebraic closure of symmetries under composition, consistent with the module's interpretation of gauge-like transformations. No downstream uses are recorded yet, but the lemma closes a basic identity axiom in the symmetry algebra.
scope and limits
- Does not prove associativity of automorphism composition.
- Does not establish that the composition preserves the inverse structure.
- Does not address physical interpretations or links to forcing chain steps.
- Does not quantify over the recognizer parameter r beyond the given T.
formal statement (Lean)
206theorem idAutomorphism_comp_left_toFun (T : RecognitionAutomorphism r) :
207 (compAutomorphism idAutomorphism T).toFun = T.toFun := by
proof body
Term-mode proof.
208 simp only [compAutomorphism, idAutomorphism, Function.id_comp]
209
210/-- Identity is right neutral for automorphisms (on toFun) -/