Action Hamiltonian Hamilton Pdot Equation

The second Hamilton equation

In classical mechanics, Hamilton's equations offer an alternative to Newton's laws. Instead of forces, they describe motion using a Hamiltonian, a function of position and momentum that often equals the total energy. The second Hamilton equation, often written as ṗ = -∂H/∂q, states that the rate of change of momentum equals the negative of the derivative of the Hamiltonian with respect to position. For a standard system with kinetic energy p²/(2m) and potential energy V(q), this becomes ṗ = -V'(q), meaning momentum decreases where the potential rises steeply.

The Recognition Science framework's machine-checked library of formal theorems includes a declaration, hamiltonPDotEquation, that encodes this second equation. The declaration defines the property that for all times t, the derivative of the momentum function p(t) equals the negative of the derivative of the potential V evaluated at the position γ(t). It is a definition, not a theorem: it states what the equation means, not that any particular motion satisfies it.

What the framework proves is a connection. Its theorem hamilton_equations_from_EL shows that if a trajectory γ satisfies the Euler-Lagrange equation for the standard Lagrangian L = ½m q̇² - V(q), and the momentum is defined as the conjugate momentum p = m q̇, then both Hamilton equations hold. The second equation, hamiltonPDotEquation, is not merely consistent with the Euler-Lagrange equation; it is the Euler-Lagrange equation in disguise. Since p = m q̇, the derivative ṗ equals m q̈, and the Euler-Lagrange equation says m q̈ = -V'(q), which is exactly Newton's second law.

The declaration itself does not claim that any physical system obeys this equation. It does not assert the existence of a trajectory, nor does it prove energy conservation. Those are separate results. The energy conservation theorem in the same module, which shows that total energy E(t) = p²/(2m) + V(q) is constant along a trajectory satisfying the Euler-Lagrange equation, relies on additional differentiability assumptions and a factored chain-rule identity supplied as a hypothesis. The hamiltonPDotEquation declaration is a building block: it fixes the meaning of the second Hamilton equation so that the framework can later prove when it holds.

/-- The Hamilton equation for `ṗ`: `ṗ = -∂H/∂q = -V'(q)`.

    For the standard Hamiltonian `H = p²/(2m) + V(q)`,
    `∂H/∂q = V'(q)`, so `ṗ(t) = -V'(γ(t))`. -/
def hamiltonPDotEquation (V : ℝ → ℝ) (γ : ℝ → ℝ) (p : ℝ → ℝ) : Prop :=
  ∀ t : ℝ, deriv p t = -(deriv V (γ t))

/-- **Hamilton's equations from the Euler–Lagrange equation.**

    Given a trajectory `γ` and conjugate momentum `p = m γ̇`, the EL
    equation for the standard Lagrangian implies Hamilton's equations:

    * `q̇ = p/m` is *definitional*: it just says `m γ̇ = p`, i.e., the
      momentum is what we said it is.
    * `ṗ = -V'(q)` is the EL equation itself, since
      `ṗ = d(m γ̇)/dt = m γ̈ = -V'(γ)` by Newton's second law.

    Therefore Hamilton's formulation and the Lagrangian formulation are
    equivalent for the standard mechanics Lagrangian. -/
theorem hamilton_equations_from_EL (m : ℝ) (hm : m ≠ 0) (V : ℝ → ℝ)
    (γ : ℝ → ℝ)
    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
    hamiltonQDotEquation m γ (conjugateMomentum m γ) ∧
    hamiltonPDotEquation V γ (conjugateMomentum m γ) := by
  constructor
  · -- q̇ = p/m where p = m γ̇
    intro t
    unfold conjugateMomentum
    field_simp
  · -- ṗ = -V'(γ): comes from EL ⇒ m γ̈ = -V'(γ)
    intro t
    have hEL_t := hEL t
    rw [QuadraticLimit.newton_second_law m V γ t] at hEL_t
    -- p(t) = m * deriv γ t, so deriv p t = m * deriv (deriv γ) t
    have hp_eq : deriv (conjugateMomentum m γ) t = m * deriv (deriv γ) t := by
      unfold conjugateMomentum
      rw [deriv_const_mul m (hγ_diff2 t)]
    rw [hp_eq, hEL_t]

/-- **Hamilton's equations from the Euler–Lagrange equation.**

    Given a trajectory `γ` and conjugate momentum `p = m γ̇`, the EL
    equation for the standard Lagrangian implies Hamilton's equations:

    * `q̇ = p/m` is *definitional*: it just says `m γ̇ = p`, i.e., the
      momentum is what we said it is.
    * `ṗ = -V'(q)` is the EL equation itself, since
      `ṗ = d(m γ̇)/dt = m γ̈ = -V'(γ)` by Newton's second law.

    Therefore Hamilton's formulation and the Lagrangian formulation are
    equivalent for the standard mechanics Lagrangian. -/
theorem hamilton_equations_from_EL (m : ℝ) (hm : m ≠ 0) (V : ℝ → ℝ)
    (γ : ℝ → ℝ)
    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
    hamiltonQDotEquation m γ (conjugateMomentum m γ) ∧
    hamiltonPDotEquation V γ (conjugateMomentum m γ) := by
  constructor
  · -- q̇ = p/m where p = m γ̇
    intro t
    unfold conjugateMomentum
    field_simp
  · -- ṗ = -V'(γ): comes from EL ⇒ m γ̈ = -V'(γ)
    intro t
    have hEL_t := hEL t
    rw [QuadraticLimit.newton_second_law m V γ t] at hEL_t
    -- p(t) = m * deriv γ t, so deriv p t = m * deriv (deriv γ) t
    have hp_eq : deriv (conjugateMomentum m γ) t = m * deriv (deriv γ) t := by
      unfold conjugateMomentum
      rw [deriv_const_mul m (hγ_diff2 t)]
    rw [hp_eq, hEL_t]

What this page does not claim

The declaration does not assert that any physical trajectory satisfies the second Hamilton equation. The declaration does not prove energy conservation; that is a separate theorem with additional hypotheses. The declaration does not establish the equivalence of Lagrangian and Hamiltonian mechanics beyond the standard Lagrangian with a scalar potential.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/Hamiltonian.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: