energy_conservation
plain-language theorem explainer
Energy is conserved along any trajectory obeying Newton's second law in the standard Hamiltonian formulation. Classical mechanicians and Noether-theorem users cite the result when confirming that time-translation invariance yields a constant total energy. The proof first substitutes the supplied chain-rule identity and the vanishing EL operator into a ring step to obtain zero derivative, verifies differentiability of the energy map from the conjugate-momentum definition, then invokes the zero-derivative-implies-constant lemma.
Claim. Let $m>0$, let $V:ℝ→ℝ$, and let $γ:ℝ→ℝ$ be twice differentiable. Suppose the Euler-Lagrange equation $mγ̈(t)+V'(γ(t))=0$ holds for all $t$, together with the chain-rule identity $dE/dt(t)=γ̇(t)·(mγ̈(t)+V'(γ(t)))$ where $E(t)=(mγ̇(t))²/(2m)+V(γ(t))$. Then $E(t₁)=E(t₂)$ for all real $t₁,t₂$.
background
The module extracts the Hamiltonian from the J-action in its small-strain Newtonian limit. The Lagrangian is $L=½m q̇²−V(q)$, the conjugate momentum is defined by $p(t)=mγ̇(t)$, and the total energy functional is $E(t)=p(t)²/(2m)+V(γ(t))$, which equals the Hamiltonian evaluated on the trajectory. The Euler-Lagrange operator reduces to $mγ̈(t)+V'(γ(t))$, whose zero set encodes Newton's second law. Upstream results supply the conjugate-momentum definition and the total-energy packaging; the module replaces the earlier scaffold-grade Hamiltonian in Foundation.Hamiltonian with concrete, sorry-free definitions. The local setting assumes the differentiability hypotheses required for the chain rule on $V∘γ$ and for the second derivative of $γ$.
proof idea
The tactic proof proceeds in three explicit steps. First, the derivative of totalEnergy is shown identically zero by rewriting via the supplied factored identity, unfolding standardEL, substituting the hypothesis that it vanishes, and simplifying by ring. Second, differentiability of the energy map is established by composing the given differentiability assumptions on $γ$ and $V$ with the conjugate-momentum definition and the algebraic operations of squaring, division, and addition. Third, the lemma is_const_of_deriv_eq_zero is applied directly to the pair of differentiability and zero-derivative facts to conclude constancy between arbitrary times.
why it matters
The theorem supplies the concrete energy-conservation statement for the standard Hamiltonian and is invoked by energyConservationCert, hamiltonian_status, energy_conservation_of_J_action, and space_translation_invariance_implies_momentum_conservation. It is also used by the foundational energy_conservation in Foundation.Hamiltonian. The doc-comment presents it as the explicit Noether theorem for time-translation invariance in the Newtonian limit of the J-action, matching the companion paper section on Hamiltonian Formulation as a Corollary. It closes the gap between the abstract Recognition framework and standard classical-mechanics conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.