IsSymmetryOf
plain-language theorem explainer
A map T on space X preserves the cost function J exactly when J(T x) equals J x at every point. Researchers deriving Noether theorems from Recognition Science cost stationarity cite this to encode invariance of the action. The definition is a direct universal quantification with no auxiliary lemmas.
Claim. A transformation $T : X → X$ is a symmetry of the cost function $J : X → ℝ$ if $J(T(x)) = J(x)$ for all $x ∈ X$.
background
The QFT.NoetherTheorem module derives Noether's theorem from cost stationarity in Recognition Science. Symmetry of J means invariance under T, which then yields conserved charges along flows. This rests on upstream notions such as the identity event at the J-cost minimum and the period T from Breath1024.
proof idea
Direct definition. The body is the single universal quantification expressing pointwise invariance of J under T; no lemmas or tactics are invoked.
why it matters
This definition is the base for downstream results in Action.Noether, including isSpaceTranslationInvariant and isTimeTranslationInvariant, which feed into theorems that space-translation invariance implies momentum conservation and time-translation invariance implies energy conservation. It realizes the module's target of obtaining Noether from ledger balance under symmetry and connects to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.