pith. machine review for the scientific record. sign in
def definition def or abbrev high

IsSymmetryOf

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  46def IsSymmetryOf {X : Type*} (T : X → X) (J : X → ℝ) : Prop :=

proof body

Definition body.

  47  ∀ x : X, J (T x) = J x
  48
  49/-- **THEOREM**: The identity is always a symmetry. -/

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.