Action Noether Energy Conservation Of J Action

Energy conservation

In classical mechanics, the connection between symmetries and conservation laws is Noether's theorem. It states that a continuous symmetry of a system's action, the integral that defines its dynamics, corresponds to a conserved quantity. Time-translation invariance, the fact that the laws do not change from one moment to the next, gives conservation of energy. Space-translation invariance gives conservation of momentum, and phase rotation in quantum mechanics gives conservation of charge.

The standard textbook result is that for a particle of mass m moving in a potential V(q), the total energy E = T + V is conserved when the potential does not depend explicitly on time. Here T is kinetic energy and V is potential energy. This is a direct consequence of Noether's theorem applied to the standard Lagrangian L = ½ m q̇² - V(q).

In Recognition Science, the framework models physical laws through a cost functional, a rule that assigns a number to a trajectory, and its library contains a machine-checked proof of this classical result. The declaration energy_conservation_of_J_action establishes that for a particle with positive mass in a time-independent potential, the total energy is the same at any two times along a trajectory that satisfies the Euler-Lagrange equation. The proof is a direct corollary of the abstract Noether theorem applied to the cost functional.

The theorem does not claim that energy is always conserved in every physical situation. It requires the potential to be time-independent and the trajectory to satisfy the equations of motion. It also does not derive the form of the cost functional from first principles; it takes the standard mechanical Lagrangian as a given. The result is a formalization of a known classical result within the framework's language, not a new physical prediction.

/-- **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 theorem does not claim energy conservation holds for time-dependent potentials. It does not derive the cost functional from first principles. It does not claim to be a new physical prediction beyond classical mechanics.

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: