`time_invariance_implies_conservation`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.NoetherTheorem
domain: QFT
line: 137 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.NoetherTheorem on GitHub at line 137.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 134
 135/-- **THEOREM**: Any time-translation-invariant function is conserved.
 136    (Energy is time-translation invariant ⟹ Energy is conserved) -/
 137theorem time_invariance_implies_conservation {E : ℝ → ℝ}
 138    (hinv : ∀ t, IsSymmetryOf (TimeTranslation.flow t) E) :
 139    IsConservedAlong E TimeTranslation.flow :=
 140  noether_core hinv
 141
 142/-! ## Space Translation and Momentum -/
 143
 144/-- Space translation by dx. -/
 145def SpaceTranslation : OneParamGroup ℝ where
 146  flow dx x := x + dx
 147  flow_zero x := by ring
 148  flow_add s t x := by ring
 149
 150/-- **THEOREM**: Any space-translation-invariant function is conserved.
 151    (Lagrangian invariant under space translation ⟹ Momentum conserved) -/
 152theorem space_invariance_implies_conservation {P : ℝ → ℝ}
 153    (hinv : ∀ dx, IsSymmetryOf (SpaceTranslation.flow dx) P) :
 154    IsConservedAlong P SpaceTranslation.flow :=
 155  noether_core hinv
 156
 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

papers checked against this theorem

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