hamiltonQDotEquation
plain-language theorem explainer
The definition encodes the first Hamilton equation dot gamma equals p over m for the standard Hamiltonian derived from the J-action. Researchers deriving classical mechanics from the recognition framework cite it when checking consistency with Newtonian trajectories. It is realized as a direct equational definition of the partial derivative of the Hamiltonian with respect to momentum.
Claim. For mass $m$, trajectory $gamma : mathbb{R} to mathbb{R}$, and conjugate momentum $p : mathbb{R} to mathbb{R}$, the first Hamilton equation holds: $forall t in mathbb{R}, dot{gamma}(t) = p(t)/m$.
background
The module derives Hamiltonian mechanics from the J-action via the Legendre transform of the standard Lagrangian $L(q, dot q) = frac{1}{2} m dot q^2 - V(q)$, the small-strain limit of the J-action. The conjugate momentum is $p = partial L / partial dot q = m dot q$, and the Hamiltonian is $H(q, p) = p^2/(2m) + V(q)$. Hamilton's equations are direct corollaries of the Euler-Lagrange equation, replacing earlier scaffold definitions with concrete ones per the module documentation referencing papers/RS_Least_Action.tex Section Hamiltonian Formulation as a Corollary.
proof idea
This definition directly asserts the universal quantification forall t, deriv gamma t = p t / m. It functions as a one-line wrapper capturing the content of partial H / partial p = p/m for the standard Hamiltonian.
why it matters
The definition supplies the first Hamilton equation to the theorem hamilton_equations_from_EL, which shows both Hamilton equations follow from the Euler-Lagrange equation under differentiability assumptions. It also appears in the EnergyConservationCert structure certifying energy conservation along trajectories. This realizes the Hamiltonian formulation as a corollary of the least-action principle within the Recognition Science framework, connecting the J-cost functional equation to classical mechanics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.