Encyclopedia Action Action Hamiltonian Standard Hamiltonian

ARTICLE 3 claims 2 theorems 1 model

Action Hamiltonian Standard Hamiltonian

The standard Hamiltonian, p²/(2m) + V(q), is the energy of a particle, and in the framework it is derived, not assumed.

Verify this page

The standard Hamiltonian

In classical mechanics, the Hamiltonian is a function that gives the total energy of a system. For a single particle of mass m moving in a potential V(q), it is H(q, p) = p²/(2m) + V(q), where p is the momentum and q is the position. The first term is kinetic energy, the second is potential energy. This is the standard form taught in every mechanics course, and it is the object the framework's declaration standardHamiltonian defines.

The framework's machine-checked library of formal theorems derives this Hamiltonian, rather than assuming it. The derivation starts from a Lagrangian L(q, q̇) = ½ m q̇² − V(q), which is the small-strain limit of the framework's J-action. The conjugate momentum is defined as p = ∂L/∂q̇ = m q̇, and the Hamiltonian is obtained via the Legendre transform H = p q̇ − L, which yields exactly p²/(2m) + V(q). This is a definitional choice, not a proved theorem: the declaration simply sets the expression.

What is proved is the connection to Hamilton's equations. The theorem hamilton_equations_from_EL shows that if a trajectory satisfies the Euler–Lagrange equation, then it satisfies Hamilton's equations: q̇ = ∂H/∂p = p/m and ṗ = −∂H/∂q = −V'(q). The first is definitional, the second is the Euler–Lagrange equation itself. This establishes the equivalence of the Lagrangian and Hamiltonian formulations for the standard mechanics Lagrangian, under the usual differentiability assumptions on the potential and trajectory.

The framework also proves energy conservation. The theorem energy_conservation states that along a trajectory satisfying the Euler–Lagrange equation, the total energy E(t) = H(γ(t), p(t)) is constant in time. This is a concrete instance of Noether's theorem: time-translation invariance implies energy conservation. The proof uses the chain rule and the Euler–Lagrange equation, with the same regularity assumptions as Noether's theorem.

In Recognition Science, this is the bridge from the framework's cost function to standard mechanics. The J-action, which is forced by the framework's axioms, reduces to the standard Lagrangian in the small-strain limit, and from there the Hamiltonian and its conservation properties follow. The framework does not claim to derive the Hamiltonian from nothing: it derives it from the Lagrangian, which is a modeling choice. The declaration standardHamiltonian is a definition, not a theorem, and the conservation theorem is proved only under the stated differentiability conditions.

MODEL standardHamiltonian · IndisputableMonolith/Action/Hamiltonian.lean
standardHamiltonian · IndisputableMonolith/Action/Hamiltonian.lean:32 
/-- The standard mechanics Hamiltonian `H(q, p) = p²/(2m) + V(q)`,
    obtained as the Legendre transform of the standard Lagrangian
    `L(q, q̇) = ½ m q̇² - V(q)`. -/
noncomputable def standardHamiltonian (m : ℝ) (V : ℝ → ℝ) (q p : ℝ) : ℝ :=
  p ^ 2 / (2 * m) + V q
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 Hamiltonian is not derived from the framework's axioms alone; it is derived from the standard Lagrangian, which is a modeling choice. Energy conservation is proved only under the stated differentiability conditions on the potential and trajectory. The declaration does not prove that the standard Hamiltonian is the unique or only possible Hamiltonian.

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