hamiltonPDotEquation
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assume any specific functional form for V beyond differentiability at gamma(t).
- Does not derive the equation from the J-action; it only names the standard form.
- Does not include the q-dot Hamilton equation or the full set of equations.
- Does not address relativistic corrections or quantum extensions.
formal statement (Lean)
55def hamiltonPDotEquation (V : ℝ → ℝ) (γ : ℝ → ℝ) (p : ℝ → ℝ) : Prop :=
proof body
Definition body.
56 ∀ t : ℝ, deriv p t = -(deriv V (γ t))
57
58/-! ## EL ↔ Hamilton's equations -/
59
60/-- **Hamilton's equations from the Euler–Lagrange equation.**
61
62 Given a trajectory `γ` and conjugate momentum `p = m γ̇`, the EL
63 equation for the standard Lagrangian implies Hamilton's equations:
64
65 * `q̇ = p/m` is *definitional*: it just says `m γ̇ = p`, i.e., the
66 momentum is what we said it is.
67 * `ṗ = -V'(q)` is the EL equation itself, since
68 `ṗ = d(m γ̇)/dt = m γ̈ = -V'(γ)` by Newton's second law.
69
70 Therefore Hamilton's formulation and the Lagrangian formulation are
71 equivalent for the standard mechanics Lagrangian. -/