OneParamGroup

formal source

  96/-! ## Noether's Core Result -/
  97
  98/-- A 1-parameter group action (simplified model). -/
  99structure OneParamGroup (X : Type*) where
 100  /-- The flow φ(t, x) giving the transformed point. -/
 101  flow : ℝ → X → X
 102  /-- φ(0, x) = x -/
 103  flow_zero : ∀ x, flow 0 x = x
 104  /-- Group property: φ(s+t, x) = φ(s, φ(t, x)) -/
 105  flow_add : ∀ s t x, flow (s + t) x = flow s (flow t x)
 106
 107/-- **THEOREM (Noether Core)**: If J is invariant under a 1-parameter group,
 108    then J itself is conserved along the flow.
 109
 110    This is the heart of Noether's theorem: symmetry ⟹ conservation. -/
 111theorem noether_core {X : Type*} {G : OneParamGroup X} {J : X → ℝ}
 112    (hinv : ∀ t, IsSymmetryOf (G.flow t) J) :
 113    IsConservedAlong J G.flow := by
 114  intro x t₁ t₂
 115  rw [hinv t₁ x, hinv t₂ x]
 116
 117/-- The Noether charge is any function conserved by the flow. -/
 118def NoetherCharge {X : Type*} (G : OneParamGroup X) :=
 119  { Q : X → ℝ // IsConservedAlong Q G.flow }
 120
 121/-- **THEOREM**: Any invariant function is a Noether charge. -/
 122theorem invariant_is_noether_charge {X : Type*} {G : OneParamGroup X} {J : X → ℝ}
 123    (hinv : ∀ t, IsSymmetryOf (G.flow t) J) :
 124    ∃ Q : NoetherCharge G, Q.val = J :=
 125  ⟨⟨J, noether_core hinv⟩, rfl⟩
 126
 127/-! ## Time Translation and Energy -/
 128
 129/-- Time translation by dt. -/