idSymmetry_comp_left
plain-language theorem explainer
Identity symmetry acts as a left neutral element under composition in recognition geometry. Researchers formalizing gauge-like redundancies or symmetry algebras would cite this when verifying monoid structure on recognition-preserving maps. The proof is a one-line simplification that unfolds the composition and identity definitions then invokes the standard function identity law.
Claim. Let $T$ be any recognition-preserving map. The left composition of the identity symmetry with $T$ equals $T$.
background
Recognition geometry treats symmetries as maps that preserve recognizable events. A recognition-preserving map is a transformation $T: C → C$ such that the recognizer applied to the image equals the recognizer applied to the original configuration for every input. The module develops the algebraic structure of these maps, including composition and identity, to capture gauge-like redundancies invisible to the recognizer. An upstream result in CostAlgebra establishes the analogous right-neutral identity law for a different automorphism type: comp f id = f.
proof idea
The proof is a one-line wrapper that applies simp to the definitions of compSymmetry, idSymmetry, and the standard Function.id_comp law.
why it matters
This result supplies the left-neutral property required for the monoid of recognition-preserving maps. It directly supports the algebraic structure section of the module, which lists composition, identity, and inverses as core results. In the Recognition Science setting it mirrors the role of the identity in the forcing chain and functional equations, where neutral elements ensure consistent composition of transformations that leave observable events unchanged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.