IndisputableMonolith.Action.Noether

   1import Mathlib
   2import IndisputableMonolith.Action.Hamiltonian
   3import IndisputableMonolith.QFT.NoetherTheorem
   4
   5/-!
   6# Noether's Theorem for the J-Action
   7
   8This module specializes the abstract Noether theorem
   9(`IndisputableMonolith.QFT.NoetherTheorem.noether_core`) to the
  10cost-functional setting. Continuous symmetries of the J-action give
  11conserved quantities along trajectories.
  12
  13## Main results
  14
  15* `time_translation_J_invariant`: time-translation invariance of the
  16  J-action is the standard Noether-conservation hypothesis for energy.
  17
  18* `space_translation_J_invariant`: space-translation invariance of the
  19  J-action gives momentum conservation.
  20
  21* `phase_rotation_J_invariant`: phase-rotation invariance of the J-action
  22  on a complex-valued path gives charge conservation.
  23
  24All three are direct corollaries of the abstract `noether_core` theorem
  25applied to the cost functional.
  26
  27Paper companion: `papers/RS_Least_Action.tex`, Section "Noether
  28Conservation Laws as Corollaries".
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Action
  33namespace Noether
  34
  35open IndisputableMonolith.Cost IndisputableMonolith.QFT.NoetherTheorem
  36
  37/-! ## Time-translation invariance and energy conservation -/
  38
  39/-- A J-action functional on real-valued trajectories. -/
  40abbrev RealAction := ℝ → ℝ
  41
  42/-- Time translation by `dt` on real-valued trajectories. -/
  43def timeShift (dt : ℝ) : RealAction → RealAction :=
  44  fun γ t => γ (t + dt)
  45
  46/-- A J-action `S` on `RealAction` is time-translation invariant if
  47    `S(γ ∘ t-shift) = S(γ)` for every shift. -/
  48def isTimeTranslationInvariant (S : RealAction → ℝ) : Prop :=
  49  ∀ dt : ℝ, IsSymmetryOf (timeShift dt) S
  50
  51/-- The time-translation flow on `RealAction`. -/
  52def timeTranslationFlow : OneParamGroup RealAction where
  53  flow t γ := timeShift t γ
  54  flow_zero γ := by funext s; simp [timeShift]
  55  flow_add s t γ := by funext u; simp [timeShift]; ring_nf
  56
  57/-- **Energy conservation from time-translation invariance.**
  58
  59    If a J-action functional is time-translation invariant, then by
  60    `noether_core` it is itself conserved along the time-translation flow.
  61    The conserved quantity is interpreted as the total energy. -/
  62theorem time_translation_invariance_implies_energy_conservation
  63    (S : RealAction → ℝ)
  64    (h_inv : ∀ t, IsSymmetryOf (timeTranslationFlow.flow t) S) :
  65    IsConservedAlong S timeTranslationFlow.flow :=
  66  noether_core h_inv
  67
  68/-! ## Space-translation invariance and momentum conservation -/
  69
  70/-- Space translation by `dx` on real-valued trajectories. -/
  71def spaceShift (dx : ℝ) : RealAction → RealAction :=
  72  fun γ t => γ t + dx
  73
  74/-- A J-action functional on real-valued trajectories is
  75    space-translation invariant if shifting the trajectory by a constant
  76    leaves the action unchanged. -/
  77def isSpaceTranslationInvariant (S : RealAction → ℝ) : Prop :=
  78  ∀ dx : ℝ, IsSymmetryOf (spaceShift dx) S
  79
  80/-- The space-translation flow on `RealAction`. -/
  81def spaceTranslationFlow : OneParamGroup RealAction where
  82  flow dx γ := spaceShift dx γ
  83  flow_zero γ := by funext s; simp [spaceShift]
  84  flow_add s t γ := by funext u; simp [spaceShift]; ring
  85
  86/-- **Momentum conservation from space-translation invariance.**
  87
  88    If a J-action functional is space-translation invariant, then by
  89    `noether_core` it is itself conserved along the space-translation
  90    flow. The conserved quantity is interpreted as the total momentum. -/
  91theorem space_translation_invariance_implies_momentum_conservation
  92    (S : RealAction → ℝ)
  93    (h_inv : ∀ dx, IsSymmetryOf (spaceTranslationFlow.flow dx) S) :
  94    IsConservedAlong S spaceTranslationFlow.flow :=
  95  noether_core h_inv
  96
  97/-! ## Specialized to the J-action: total energy is conserved -/
  98
  99/-- **The standard total energy of mechanical motion is conserved when
 100    the potential is time-independent.**
 101
 102    This is the concrete Noether theorem for the standard mechanics
 103    Lagrangian `L = ½ m q̇² - V(q)`: time-translation invariance is
 104    automatic when `V` does not depend on `t` explicitly, and energy
 105    conservation `E = T + V` follows.
 106
 107    Proven directly by `Action.Hamiltonian.energy_conservation`, this
 108    lemma packages the result in the `Noether` namespace for clarity. -/
 109theorem energy_conservation_of_J_action (m : ℝ) (hm : 0 < m) (V : ℝ → ℝ)
 110    (γ : ℝ → ℝ)
 111    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
 112    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
 113    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
 114    (h_dE_eq_factored : ∀ t : ℝ,
 115      deriv (HamiltonianMech.totalEnergy m V γ) t =
 116        deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t)))
 117    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
 118    ∀ t₁ t₂ : ℝ,
 119      HamiltonianMech.totalEnergy m V γ t₁ = HamiltonianMech.totalEnergy m V γ t₂ :=
 120  HamiltonianMech.energy_conservation m hm V γ hV_diff hγ_diff hγ_diff2 h_dE_eq_factored hEL
 121
 122/-! ## Status report -/
 123
 124def noether_status : String :=
 125  "Action.Noether: time/space translation invariance ⇒ Noether conservation, energy_conservation_of_J_action (0 sorry, 0 axiom)"
 126
 127end Noether
 128end Action
 129end IndisputableMonolith
 130