hamiltonPDotEquation
plain-language theorem explainer
The definition encodes the p-dot Hamilton equation as the assertion that the time derivative of conjugate momentum p equals the negative derivative of potential V along trajectory gamma. Researchers deriving the equivalence of Lagrangian and Hamiltonian forms from the J-action would cite it when moving from Euler-Lagrange to phase-space dynamics. It is a pure definitional abbreviation with no lemmas or reductions.
Claim. The p-dot equation asserts that for all real $t$, the derivative of $p$ satisfies $p'(t) = -V' (gamma(t))$, where $p$ is the conjugate momentum to trajectory $gamma$ and $V$ is the potential.
background
The module derives Hamiltonian mechanics from the J-action by taking the small-strain limit of the recognition Lagrangian, which reduces to the standard form $L(q, qdot) = (1/2) m qdot^2 - V(q)$. Conjugate momentum is introduced as $p = partial L / partial qdot = m qdot$, and the Hamiltonian follows from the Legendre transform as $H(q,p) = p^2/(2m) + V(q)$. Hamilton's equations then appear as direct corollaries of the Euler-Lagrange equation for this Lagrangian.
proof idea
This is a definition that directly encodes the mathematical content of the p-dot Hamilton equation: the derivative of p with respect to time equals the negative derivative of V at gamma(t). No lemmas are applied; it is a pure definitional abbreviation.
why it matters
This definition supplies the second Hamilton equation used in the downstream theorem hamilton_equations_from_EL to establish equivalence between the Euler-Lagrange formulation and Hamilton's equations. It fills the Hamiltonian formulation as a corollary in the paper companion RS_Least_Action.tex, Section Hamiltonian Formulation as a Corollary. The step connects the J-cost action through the Legendre transform to the standard mechanics limit, supporting the overall derivation of classical dynamics within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.