standardHamiltonian
plain-language theorem explainer
The definition supplies the standard Hamiltonian H(q, p) = p²/(2m) + V(q) obtained via Legendre transform from the standard Lagrangian in the small-strain limit of the J-action. Researchers deriving Hamiltonian mechanics from the Recognition Science action framework would cite this when establishing energy conservation and Hamilton's equations. It is realized as the direct algebraic expression p²/(2m) + V(q).
Claim. The standard Hamiltonian is defined by $H(q, p) = p^2/(2m) + V(q)$, where $V$ is the potential function.
background
This module derives the Hamiltonian formulation from the J-action via the Legendre transform of the standard Lagrangian L(q, q̇) = ½ m q̇² - V(q) (the small-strain limit of the J-action). The conjugate momentum is p = ∂L/∂q̇ = m q̇, and the Hamiltonian is H(q, p) = p q̇ - L = p²/(2m) + V(q). Upstream results include the inflaton potential V(φ_inf) = Jcost(1 + φ_inf) from Cosmology.InflatonPotentialFromJCost and the vantage type V from RRF.Core.Glossary.
proof idea
The definition is the explicit algebraic expression p²/(2m) + V(q) realizing the Legendre transform of the standard Lagrangian. No lemmas are applied; it is the direct formula for the Hamiltonian.
why it matters
This definition feeds the totalEnergy and hamiltonian_status declarations, which establish energy conservation along Newtonian trajectories as a corollary of the EL equation. It fills the Hamiltonian Formulation as a Corollary section in the paper companion RS_Least_Action.tex, replacing earlier scaffold-grade code with real definitions and a real conservation theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.