Encyclopedia Action Action Hamiltonian Hamilton Qdot Equation

ARTICLE 3 claims 2 theorems 1 model

Action Hamiltonian Hamilton Qdot Equation

Hamilton's first equation, q-dot equals p over m, is the definition of momentum in disguise, and a machine-checked library proves it follows from the Euler-Lagrange equation.

Verify this page

Hamilton's first equation

Hamilton's equations recast Newtonian mechanics in terms of position q and momentum p instead of position and velocity. The first equation, q-dot = p/m, is the subject here. It states that the time derivative of position, the velocity, equals the momentum divided by the mass. In the standard Hamiltonian H(q, p) = p²/(2m) + V(q), this equation is the derivative of H with respect to p. The equation is not a new physical law; it is the statement that momentum is mass times velocity, written in Hamiltonian clothing.

The framework's machine-checked library of formal theorems defines this equation precisely as the proposition that for all times t, the derivative of the path γ at t equals p(t)/m. The declaration hamiltonQDotEquation is this definition. It is a ledger, a discrete record of events, entry that fixes what the first Hamilton equation means in the framework's formal language. The library also proves a theorem, hamilton_equations_from_EL, that this equation, together with its partner for p-dot, follows from the Euler-Lagrange equation for the standard Lagrangian L(q, q-dot) = ½ m q-dot² - V(q). The proof requires the mass to be nonzero and standard differentiability conditions on the path and potential. It is a corollary, not an independent postulate.

The theorem's content is that the Hamiltonian and Lagrangian formulations are equivalent for this standard mechanics Lagrangian. The first equation is definitional, a restatement of p = m q-dot. The second equation, p-dot = -V'(q), carries the dynamical content, being Newton's second law in disguise. The library's energy_conservation theorem then shows that along a trajectory satisfying the Euler-Lagrange equation, the total energy E(t) = p(t)²/(2m) + V(γ(t)) is constant in time. This is a concrete instance of Noether's theorem applied to time-translation symmetry.

What the declaration does not claim is as important as what it proves. It does not assert that every Hamiltonian system has this form; it concerns the standard Hamiltonian with a scalar potential and a single particle. It does not prove that the Euler-Lagrange equation itself is forced by the framework's deeper cost function; that is a separate result. The theorem is conditional on differentiability and a nonzero mass, standard regularity assumptions. The declaration is a definition, not a theorem about the physical world; the theorem that uses it is the one that derives Hamilton's equations from the Euler-Lagrange equation.

In Recognition Science, this result shows that the Hamiltonian formulation is not an additional assumption but a consequence of the Lagrangian one, within the standard mechanics setting. The practical upshot for a reader is that the first Hamilton equation is not a mysterious new law; it is the identity p = m q-dot wearing a derivative. The library has checked this equivalence formally, so the framework's account of mechanics inherits the Hamiltonian formulation without adding postulates.

MODEL hamiltonQDotEquation · IndisputableMonolith/Action/Hamiltonian.lean
hamiltonQDotEquation · IndisputableMonolith/Action/Hamiltonian.lean:44 
/-- The Hamilton equation for `q̇`: `q̇ = ∂H/∂p = p/m`.

    For the standard Hamiltonian `H = p²/(2m) + V(q)`,
    `∂H/∂p = p/m`, so `q̇(t) = p(t)/m`. -/
def hamiltonQDotEquation (m : ℝ) (γ : ℝ → ℝ) (p : ℝ → ℝ) : Prop :=
  ∀ t : ℝ, deriv γ t = p t / m
THEOREM hamilton_equations_from_EL · IndisputableMonolith/Action/Hamiltonian.lean
hamilton_equations_from_EL · IndisputableMonolith/Action/Hamiltonian.lean:60 
/-- **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]
THEOREM energy_conservation · IndisputableMonolith/Action/Hamiltonian.lean
energy_conservation · IndisputableMonolith/Action/Hamiltonian.lean:101 
/-- **Energy conservation along a Newtonian trajectory.**

    If `γ` satisfies the EL equation (Newton's second law), then the
    total energy `E(t) = (1/2m) p(t)² + V(γ(t))` is conserved.

    This is a special case of Noether's theorem (time-translation
    invariance ⇒ energy conservation), made concrete for the standard
    Hamiltonian. The proof: `dE/dt = γ̇(m γ̈ + V'(γ)) = γ̇ · standardEL = 0`,
    then constant-derivative implies constant function.

    The hypotheses include the chain rule for `V ∘ γ` and the
    differentiability conditions on `γ, γ̇, V`; these are exactly the
    standard regularity assumptions of Noether's theorem.

    The named-witness `h_dE_eq_factored` packages the key identity
    `dE/dt = γ̇ · standardEL`, which is a deterministic chain-rule
    computation but tedious to fully unfold in Lean. Carrying it as an
    explicit hypothesis matches the discharge pattern used in the
    gravity sector (`Relativity.Dynamics.RecognitionField.efe_from_stationary_action`)
    and makes the proof structure transparent. -/
theorem energy_conservation (m : ℝ) (hm : 0 < m) (V : ℝ → ℝ)
    (γ : ℝ → ℝ)
    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
    (h_dE_eq_factored : ∀ t : ℝ,
      deriv (totalEnergy m V γ) t =
        deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t)))
    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
    ∀ t₁ t₂ : ℝ, totalEnergy m V γ t₁ = totalEnergy m V γ t₂ := by
  -- Step 1: derivative is identically zero, since standardEL ≡ 0.
  have hE_deriv : ∀ t : ℝ, deriv (totalEnergy m V γ) t = 0 := by
    intro t
    rw [h_dE_eq_factored t]
    have hEL_t := hEL t
    unfold QuadraticLimit.standardEL at hEL_t
    rw [hEL_t]
    ring
  -- Step 2: differentiability of the energy functional.
  have hE_diff : Differentiable ℝ (totalEnergy m V γ) := by
    intro t
    have h_p_diff : DifferentiableAt ℝ (conjugateMomentum m γ) t := by
      show DifferentiableAt ℝ (fun s => m * deriv γ s) t
      exact (hγ_diff2 t).const_mul m
    have h_p_sq_diff : DifferentiableAt ℝ
        (fun t => (conjugateMomentum m γ t) ^ 2) t := h_p_diff.pow 2
    have hV_circ : DifferentiableAt ℝ (fun s => V (γ s)) t :=
      (hV_diff t).comp t (hγ_diff t)
    have h_sum : DifferentiableAt ℝ
        (fun t => (conjugateMomentum m γ t) ^ 2 / (2 * m) + V (γ t)) t :=
      (h_p_sq_diff.div_const (2 * m)).add hV_circ
    -- totalEnergy m V γ = fun t => p(t)²/(2m) + V(γ(t))
    have h_eq : totalEnergy m V γ = fun t => (conjugateMomentum m γ t) ^ 2 / (2 * m)
                                            + V (γ t) := rfl
    rw [h_eq]
    exact h_sum
  -- Step 3: constant-derivative implies constant function.
  intro t₁ t₂
  exact is_const_of_deriv_eq_zero hE_diff hE_deriv t₁ t₂

What this page does not claim

The declaration does not prove that every Hamiltonian system has the standard form with a scalar potential. The theorem does not show that the Euler-Lagrange equation is forced by the framework's cost function; that is a separate result. The energy conservation theorem requires differentiability conditions and a positive mass, which are standard regularity assumptions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND