hamilton_equations_from_EL
plain-language theorem explainer
The theorem shows that if a trajectory satisfies the Euler-Lagrange equation for the standard Lagrangian, then it satisfies the two Hamilton equations with conjugate momentum p = m gamma-dot. A researcher deriving classical mechanics from the J-action or verifying equivalence of formulations would cite this step. The proof splits the conjunction with constructor, treats the velocity relation by direct unfolding and simplification, and obtains the momentum relation by rewriting the given EL condition through Newton's second law.
Claim. Let $m$ be a nonzero real, $V : ℝ → ℝ$, and $γ : ℝ → ℝ$ a trajectory. Assume the stated differentiability conditions on $V$ and $γ$ together with its first derivative. If the Euler-Lagrange equation $m γ̈(t) + V'(γ(t)) = 0$ holds for every $t$, and if $p(t) := m γ̇(t)$, then $γ̇(t) = p(t)/m$ and $ṗ(t) = -V'(γ(t))$ for all $t$.
background
The module Action.Hamiltonian derives the Hamiltonian picture from the J-action by taking the small-strain (quadratic) limit of the standard Lagrangian $L(q, q̇) = ½ m q̇² - V(q)$. The conjugate momentum is the partial derivative $p = ∂L/∂q̇ = m q̇$. Hamilton's equations then read $q̇ = ∂H/∂p = p/m$ and $ṗ = -∂H/∂q = -V'(q)$, where $H = p²/(2m) + V(q)$ is the Legendre transform of $L$ (see the sibling definitions hamiltonQDotEquation and hamiltonPDotEquation).
proof idea
The tactic proof opens with constructor to split the conjunction of the two Hamilton equations. The first conjunct is discharged by introducing t, unfolding conjugateMomentum, and applying field_simp. The second conjunct obtains the EL instance at t, rewrites it via the upstream theorem newton_second_law to replace the EL condition by m γ̈ = -V'(γ), proves that the time derivative of p equals m times the second derivative of γ using the supplied differentiability hypothesis and the derivative rule for constant multiplication, then substitutes to finish.
why it matters
The result supplies the explicit equivalence between Lagrangian and Hamiltonian descriptions inside the Recognition Science derivation of mechanics from the J-cost. It is invoked by energyConservationCert to certify that energy is conserved along solutions of Newton's law, and it populates the summary hamiltonian_status. The module documentation identifies the statement as the concrete replacement for an earlier scaffold and points to the paper companion RS_Least_Action.tex, Section Hamiltonian Formulation as a Corollary. It thereby closes one link in the passage from the Recognition Composition Law to classical conservation statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.