energy_conservation_of_J_action
plain-language theorem explainer
The theorem asserts that total mechanical energy E(t) = ½m γ̇(t)² + V(γ(t)) remains constant along any trajectory γ obeying the Euler-Lagrange equation for a time-independent potential V. Researchers specializing the abstract Noether theorem to the J-cost functional in Recognition Science would cite it when deriving conservation laws from time-translation invariance. The proof is a direct one-line application of the energy conservation theorem in the Hamiltonian module.
Claim. Let $m>0$, $V:ℝ→ℝ$, and trajectory $γ:ℝ→ℝ$. Assume $V$ is differentiable along $γ$, $γ$ is twice differentiable, the derivative of total energy factors as $γ̇(t)·(m γ̈(t)+V'(γ(t)))$, and the Euler-Lagrange equation $m γ̈(t)+V'(γ(t))=0$ holds for all $t$. Then the total energy $E(t)=½m γ̇(t)² + V(γ(t))$ satisfies $E(t_1)=E(t_2)$ for all real $t_1,t_2$.
background
The Action.Noether module specializes the abstract Noether theorem from QFT.NoetherTheorem.noether_core to the J-cost functional. Key supporting definitions are totalEnergy, which returns the Hamiltonian value standardHamiltonian m V (γ t) (conjugateMomentum m γ t), and standardEL, the operator m·(second derivative of γ) + (derivative of V at γ(t)) that encodes Newton's second law for the Lagrangian ½m q̇² - V(q). The upstream theorem energy_conservation in Action.Hamiltonian states that if γ satisfies the EL equation then dE/dt = γ̇·standardEL = 0, so energy is conserved. The module documentation notes that time-translation invariance of the J-action is the hypothesis yielding this conservation, as a concrete corollary of the abstract result.
proof idea
The proof is a one-line wrapper that applies the energy_conservation theorem from IndisputableMonolith.Action.Hamiltonian, supplying the mass, potential, trajectory, differentiability hypotheses, factored derivative condition, and the assumption that standardEL vanishes identically.
why it matters
This declaration supplies the concrete energy-conservation corollary for the standard mechanical Lagrangian inside the J-action setting, directly feeding the noether_status definition that reports the overall status of Noether results in the module. It fills the time-translation case of the paper proposition on Noether conservation laws as corollaries (papers/RS_Least_Action.tex). In the Recognition Science framework it anchors the mechanical limit of the recognition Hamiltonian, consistent with the forcing chain steps that produce conserved quantities from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.