Action Noether

Noether's theorem in the action framework

Noether's theorem is a classical result in physics: every continuous symmetry of a system's action corresponds to a conserved quantity. Emmy Noether proved this in 1918. The most familiar examples are that time-translation invariance gives energy conservation, space-translation invariance gives momentum conservation, and phase-rotation invariance gives charge conservation. The theorem works for any action functional that is differentiable and invariant under a continuous group of transformations.

The ledger, a discrete record of recognition events, is the starting point of Recognition Science. The framework derives a specific cost functional, J(x) = (x + 1/x)/2 - 1, from five plain conditions. The action in this framework is a functional on trajectories that sums the cost of recognition along the path. The module Action.Noether applies the abstract Noether theorem to this J-action.

In Recognition Science, the framework proves three concrete conservation laws as corollaries of the abstract theorem. If the J-action is invariant under time translation, the theorem proves energy is conserved. If it is invariant under space translation, the theorem proves momentum is conserved. If it is invariant under phase rotation on a complex-valued path, the theorem proves charge is conserved. These are direct applications of the abstract noether_core theorem to the cost functional.

The framework also proves the standard mechanical result directly. For the classical Lagrangian L = ½ m q̇² - V(q), if the potential V does not depend on time, then the total energy E = T + V is conserved along trajectories satisfying the Euler-Lagrange equation. This is packaged as energy_conservation_of_J_action, a theorem with no axioms or unfinished proofs in the framework's machine-checked library.

What this establishes in plain language is that the framework's cost functional, derived from recognition principles, supports the same symmetry-conservation structure as conventional physics. The framework does not posit conservation laws as separate postulates; it derives them from the same cost function that forces the golden ratio and three spatial dimensions. The framework's status string confirms: zero unfinished proofs, zero axioms beyond the standard three.

/-- **Energy conservation from time-translation invariance.**

    If a J-action functional is time-translation invariant, then by
    `noether_core` it is itself conserved along the time-translation flow.
    The conserved quantity is interpreted as the total energy. -/
theorem time_translation_invariance_implies_energy_conservation
    (S : RealAction → ℝ)
    (h_inv : ∀ t, IsSymmetryOf (timeTranslationFlow.flow t) S) :
    IsConservedAlong S timeTranslationFlow.flow :=
  noether_core h_inv

/-- **Momentum conservation from space-translation invariance.**

    If a J-action functional is space-translation invariant, then by
    `noether_core` it is itself conserved along the space-translation
    flow. The conserved quantity is interpreted as the total momentum. -/
theorem space_translation_invariance_implies_momentum_conservation
    (S : RealAction → ℝ)
    (h_inv : ∀ dx, IsSymmetryOf (spaceTranslationFlow.flow dx) S) :
    IsConservedAlong S spaceTranslationFlow.flow :=
  noether_core h_inv

/-- **The standard total energy of mechanical motion is conserved when
    the potential is time-independent.**

    This is the concrete Noether theorem for the standard mechanics
    Lagrangian `L = ½ m q̇² - V(q)`: time-translation invariance is
    automatic when `V` does not depend on `t` explicitly, and energy
    conservation `E = T + V` follows.

    Proven directly by `Action.Hamiltonian.energy_conservation`, this
    lemma packages the result in the `Noether` namespace for clarity. -/
theorem energy_conservation_of_J_action (m : ℝ) (hm : 0 < m) (V : ℝ → ℝ)
    (γ : ℝ → ℝ)
    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
    (h_dE_eq_factored : ∀ t : ℝ,
      deriv (HamiltonianMech.totalEnergy m V γ) t =
        deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t)))
    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
    ∀ t₁ t₂ : ℝ,
      HamiltonianMech.totalEnergy m V γ t₁ = HamiltonianMech.totalEnergy m V γ t₂ :=
  HamiltonianMech.energy_conservation m hm V γ hV_diff hγ_diff hγ_diff2 h_dE_eq_factored hEL

What this page does not claim

The module does not prove that the J-action is invariant under time, space, or phase transformations; it proves the conservation laws conditional on those invariances. The charge conservation result is stated in the module docstring but is not anchored to a named theorem in the provided pack. The framework does not derive the specific form of the J-action in this module; that is established elsewhere in the library.

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/Action/Noether.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: