symmetry_comp
Symmetries of the J-cost compose: if T1 and T2 each preserve J, then so does T1 composed with T2. Workers on cost-derived Noether theorems cite this to close the set of symmetries under group operations. The proof is a one-line term that applies the definition of composition to the invariance conditions.
claimIf $T_1,T_2:X→X$ satisfy $J(T_1(x))=J(x)$ and $J(T_2(x))=J(x)$ for all $x$, then $J((T_1∘T_2)(x))=J(x)$ for all $x$.
background
In the QFT-006 module, Noether's theorem is derived from cost stationarity: a symmetry is any transformation that leaves the J-cost invariant. The referenced definition states that T is a symmetry of J precisely when J(T x) equals J x for every x in X. This local setting connects continuous symmetries to conserved charges via ledger balance under transformations. The result relies on the algebraic property of function composition, where successive application satisfies comp g f x = g (f x).
proof idea
The proof is a term-mode one-liner: introduce arbitrary x, then rewrite J((T1 ∘ T2) x) by the composition rule followed by the two symmetry hypotheses in sequence.
why it matters in Recognition Science
This closes the symmetry relation under composition, a prerequisite for forming symmetry groups in the Noether framework. It feeds into the core noether_core theorem by allowing chains of symmetries to be treated as single transformations. Within Recognition Science it supports the emergence of conserved quantities from cost stationarity, as targeted by the module's derivation of Noether from ledger structure.
scope and limits
- Does not assume continuity or differentiability of the transformations.
- Does not derive the explicit conserved charge associated to the symmetry.
- Does not extend to infinite or Lie-group compositions.
formal statement (Lean)
55theorem symmetry_comp {X : Type*} {T₁ T₂ : X → X} {J : X → ℝ}
56 (h₁ : IsSymmetryOf T₁ J) (h₂ : IsSymmetryOf T₂ J) :
57 IsSymmetryOf (T₁ ∘ T₂) J := by
proof body
Term-mode proof.
58 intro x
59 simp only [Function.comp_apply, h₂ x, h₁ (T₂ x)]
60
61/-- **THEOREM**: Inverse of a bijective symmetry is a symmetry. -/