Encyclopedia Action Action Hamiltonian Conjugate Momentum

ARTICLE 3 claims 2 theorems 1 model

Action Hamiltonian Conjugate Momentum

In classical mechanics, momentum is mass times velocity; the framework's declaration makes that definition precise for any smooth path.

Verify this page

The conjugate momentum

In classical mechanics, the conjugate momentum is the quantity that pairs with a position coordinate in the Hamiltonian formulation. For a particle of mass m moving along a path γ(t), it is defined as p = ∂L/∂q̇ = m q̇, where L is the Lagrangian. This is the standard definition found in any mechanics textbook: momentum is mass times velocity. The framework's declaration conjugateMomentum (a definition in its machine-checked library of formal theorems) states exactly this: p = m * deriv γ t, where deriv γ t is the derivative of the path at time t.

The declaration is a definition, not a theorem. It does not prove that momentum is conserved, nor does it derive the Hamiltonian from first principles. What it does is fix the meaning of the term within the framework's formal system. The framework then uses this definition to state and prove Hamilton's equations. The theorem hamilton_equations_from_EL shows that if a path satisfies the Euler-Lagrange equation (Newton's second law), then with this definition of momentum, the two Hamilton equations follow: q̇ = p/m and ṗ = -V'(q). The first is definitional; the second is the Euler-Lagrange equation itself.

The framework also defines the total energy as the Hamiltonian evaluated along the path, E(t) = H(γ(t), p(t)). A separate theorem, energy_conservation, proves that this energy is constant along any trajectory satisfying the Euler-Lagrange equation, given standard differentiability conditions. This is a concrete instance of Noether's theorem: time-translation invariance implies energy conservation. The proof factors through the identity dE/dt = γ̇ · standardEL, which is a chain-rule computation.

What the declaration does not claim is broader. It does not claim that the Hamiltonian formulation is more fundamental than the Lagrangian one; the theorem states they are equivalent for this standard Lagrangian. It does not claim that momentum is always mass times velocity in every physical theory; it is a definition for the specific case of a particle with mass m in a potential V. It does not claim that energy is conserved in all circumstances; the theorem requires the path to satisfy the equations of motion and assumes differentiability. These are standard conditions, but they are conditions nonetheless.

MODEL conjugateMomentum · IndisputableMonolith/Action/Hamiltonian.lean
conjugateMomentum · IndisputableMonolith/Action/Hamiltonian.lean:38 
/-- The conjugate momentum from the Lagrangian: `p = ∂L/∂q̇ = m q̇`. -/
noncomputable def conjugateMomentum (m : ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=
  m * deriv γ t
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 momentum conservation. The declaration does not claim the Hamiltonian formulation is more fundamental than the Lagrangian one. The declaration does not define momentum for all physical theories, only for a particle of mass m in a potential V.

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