Qft Noether Theorem

Noether's theorem from cost stationarity

Noether's theorem, published by Emmy Noether in 1918, is a central result of modern physics. It states that every continuous symmetry of a physical system's action corresponds to a conserved quantity. Time translation symmetry gives energy conservation, space translation gives momentum, rotation gives angular momentum, and phase rotation gives electric charge. The theorem explains why these quantities remain constant in time and provides a unifying principle across classical and quantum physics.

The Recognition Science framework approaches this result from a different starting point. Instead of beginning with an action functional, it begins with a ledger, a discrete record of recognition events, and a cost function J that assigns a real number to each state of a system. The framework's central claim is that this cost function is forced by five plain conditions to take the unique form J(x) = (x + 1/x)/2 - 1. From this cost structure, the framework derives Noether's theorem as a consequence of what it calls cost stationarity: if a transformation leaves the cost unchanged, then the cost itself becomes the conserved quantity.

The machine-checked library of formal theorems proves this result directly. The core theorem, noether_core, states that if a one-parameter group of transformations G leaves the cost J invariant at every parameter value, then J is conserved along the flow of G. In plain language: if a transformation never changes the cost, then the cost function itself is the constant of motion. The library then applies this core theorem to concrete examples. It proves that time translation invariance implies conservation of energy, space translation invariance implies conservation of momentum, and phase rotation invariance implies conservation of the invariant quantity. The harmonic oscillator provides a worked example: the library defines the harmonic energy function and proves that it is conserved under the harmonic flow.

This derivation is not merely a restatement of Noether's classical result. The framework's theorem is more general in one respect: it does not require the action, the Lagrangian, or even differentiability. The only ingredients are a cost function and a one-parameter group of transformations that preserves it. The library also formalizes the standard symmetry group properties: the identity is a symmetry, symmetries compose, and the inverse of a bijective symmetry is a symmetry. The conservation statement comes in two equivalent forms, and the library proves their equivalence under the group property.

The framework also catalogues the standard model conservation laws in terms of their underlying symmetries: energy from time translation, momentum from space translation, angular momentum from rotation, electric charge from U(1) phase, color charge from SU(3), weak isospin from SU(2) (broken), and baryon and lepton numbers from approximate symmetries. It explicitly lists apparent violations and their resolutions: energy non-conservation in an expanding universe is resolved because time translation symmetry is broken by cosmological expansion, and baryon number violation in grand unified theories is resolved because U(1)_B is only an approximate symmetry. This honest accounting shows the framework's scope: it proves the theorem, and it names the conditions under which the theorem's assumptions fail.

/-- **THEOREM (Noether Core)**: If J is invariant under a 1-parameter group,
    then J itself is conserved along the flow.

    This is the heart of Noether's theorem: symmetry ⟹ conservation. -/
theorem noether_core {X : Type*} {G : OneParamGroup X} {J : X → ℝ}
    (hinv : ∀ t, IsSymmetryOf (G.flow t) J) :
    IsConservedAlong J G.flow := by
  intro x t₁ t₂
  rw [hinv t₁ x, hinv t₂ x]

/-- **THEOREM**: Any time-translation-invariant function is conserved.
    (Energy is time-translation invariant ⟹ Energy is conserved) -/
theorem time_invariance_implies_conservation {E : ℝ → ℝ}
    (hinv : ∀ t, IsSymmetryOf (TimeTranslation.flow t) E) :
    IsConservedAlong E TimeTranslation.flow :=
  noether_core hinv

/-- **THEOREM**: Any space-translation-invariant function is conserved.
    (Lagrangian invariant under space translation ⟹ Momentum conserved) -/
theorem space_invariance_implies_conservation {P : ℝ → ℝ}
    (hinv : ∀ dx, IsSymmetryOf (SpaceTranslation.flow dx) P) :
    IsConservedAlong P SpaceTranslation.flow :=
  noether_core hinv

/-- **THEOREM**: Energy is conserved along harmonic oscillator flow.

    This is an explicit verification of energy conservation for the
    harmonic oscillator, showing that Noether's theorem works. -/
theorem harmonic_energy_conserved (m k : ℝ) (hm : m > 0) (hk : k > 0) :
    ∀ pt t, harmonicEnergy m k (harmonicFlow m k hm hk t pt) = harmonicEnergy m k pt := by
  intro pt t
  simp only [harmonicEnergy, harmonicFlow]
  set ω := Real.sqrt (k / m) with hω_def
  have hω_pos : ω > 0 := Real.sqrt_pos.mpr (div_pos hk hm)
  have hω_sq : ω^2 = k / m := Real.sq_sqrt (le_of_lt (div_pos hk hm))
  have hcos_sin : Real.cos (ω * t)^2 + Real.sin (ω * t)^2 = 1 := Real.cos_sq_add_sin_sq (ω * t)
  have hmne : m ≠ 0 := ne_of_gt hm
  have hωne : ω ≠ 0 := ne_of_gt hω_pos
  -- After expansion, the energy terms reduce using ω² = k/m and cos²+sin²=1
  -- E' = (1/2m)[(p cos - mωq sin)² + k(q cos + p/(mω) sin)²]
  --    = (1/2m)[p² cos² + m²ω²q² sin² - 2mωpq sin cos
  --           + kq² cos² + kp²/(m²ω²) sin² + 2kpq/(mω) sin cos]
  -- Using k = mω²:
  --    = (1/2m)[p² cos² + m²ω²q² sin² + m²ω²q² cos² + p² sin²]
  --    = (1/2m)[p²(cos² + sin²) + m²ω²q²(sin² + cos²)]
  --    = (1/2m)[p² + k·m·q²] = p²/2m + kq²/2 = E
  have hmω_sq : m * ω^2 = k := by rw [hω_sq]; field_simp
  -- We prove the equality by direct calculation
  have key : ∀ (c s : ℝ), c^2 + s^2 = 1 →
      (pt.p * c - m * ω * pt.q * s)^2 / (2 * m) +
      k * (pt.q * c + pt.p / (m * ω) * s)^2 / 2 =
      pt.p^2 / (2 * m) + k * pt.q^2 / 2 := by
    intro c s hcs
    have h1 : k = m * ω^2 := hmω_sq.symm
    rw [h1]
    field_simp
    ring_nf
    -- After ring_nf, we need to show the coefficients match using c² + s² = 1
    have hs2 : s^2 = 1 - c^2 := by linarith [hcs]
    rw [hs2]
    ring
  exact key (Real.cos (ω * t)) (Real.sin (ω * t)) hcos_sin

/-- **THEOREM**: The identity is always a symmetry. -/
theorem id_is_symmetry {X : Type*} (J : X → ℝ) : IsSymmetryOf id J := by
  intro x
  rfl

/-- **THEOREM**: Composition of symmetries is a symmetry. -/
theorem symmetry_comp {X : Type*} {T₁ T₂ : X → X} {J : X → ℝ}
    (h₁ : IsSymmetryOf T₁ J) (h₂ : IsSymmetryOf T₂ J) :
    IsSymmetryOf (T₁ ∘ T₂) J := by
  intro x
  simp only [Function.comp_apply, h₂ x, h₁ (T₂ x)]

/-- **THEOREM**: Inverse of a bijective symmetry is a symmetry. -/
theorem symmetry_inv {X : Type*} [Nonempty X] {T : X → X} {J : X → ℝ}
    (hT : Function.Bijective T) (hsym : IsSymmetryOf T J) :
    IsSymmetryOf (Function.invFun T) J := by
  intro x
  have hinvr := Function.rightInverse_invFun hT.surjective
  rw [← hsym (Function.invFun T x)]
  congr 1
  exact hinvr x

What this page does not claim

This answer does not claim that the framework derives the specific form of the cost function J(x) = (x + 1/x)/2 - 1 within this module; that result lives in the separate functional equation file. This answer does not claim that the framework proves the standard model's full particle content or the specific values of its coupling constants. This answer does not claim that the framework's Noether theorem applies to approximate symmetries like baryon number; the library explicitly lists those as apparent violations with resolutions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/QFT/NoetherTheorem.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: