 157/-! ## Phase Rotation and Charge -/
 158
 159/-- Phase rotation on ℂ. -/
 160noncomputable def PhaseRotation : OneParamGroup ℂ where
 161  flow θ z := Complex.exp (θ * Complex.I) * z
 162  flow_zero z := by simp [Complex.exp_zero]
 163  flow_add s t z := by
 164    rw [← mul_assoc, ← Complex.exp_add]
 165    congr 1
 166    push_cast
 167    ring
 168
 169/-- **THEOREM**: Any phase-rotation-invariant function is conserved.
 170    (U(1) symmetry ⟹ Electric charge conserved) -/
 171theorem phase_invariance_implies_conservation {Q : ℂ → ℝ}
 172    (hinv : ∀ θ, IsSymmetryOf (PhaseRotation.flow θ) Q) :
 173    IsConservedAlong Q PhaseRotation.flow :=
 174  noether_core hinv
 175
 176/-! ## Concrete Example: Harmonic Oscillator -/
 177
 178/-- Phase space point (position, momentum). -/
 179structure PhasePoint where
 180  q : ℝ  -- position
 181  p : ℝ  -- momentum
 182
 183/-- Harmonic oscillator energy: H = p²/2m + kq²/2 -/
 184noncomputable def harmonicEnergy (m k : ℝ) (pt : PhasePoint) : ℝ :=
 185  pt.p^2 / (2 * m) + k * pt.q^2 / 2
 186
 187/-- Harmonic oscillator flow (exact solution). -/
 188noncomputable def harmonicFlow (m k : ℝ) (_hm : m > 0) (_hk : k > 0) : ℝ → PhasePoint → PhasePoint :=
 189  fun t pt =>
 190    let ω := Real.sqrt (k / m)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.