Encyclopedia Action Action Hamiltonian

ARTICLE 3 claims 2 theorems 1 model

Action Hamiltonian

The Hamiltonian, the classical engine of mechanics, emerges here as a corollary of a deeper action principle.

Verify this page

The Hamiltonian from the J-action

The Hamiltonian is a function that encodes the total energy of a system, expressed in terms of position and momentum. For a particle of mass m moving in a potential V(q), it takes the familiar form H(q, p) = p²/(2m) + V(q), where p is the momentum. This is the standard starting point for Hamilton's equations, which describe how position and momentum evolve in time.

The classical derivation begins with the Lagrangian L(q, q̇) = ½ m q̇² - V(q), the difference between kinetic and potential energy. The conjugate momentum is defined as p = ∂L/∂q̇ = m q̇, and the Hamiltonian is obtained through a Legendre transform: H = p q̇ - L. This transform swaps the velocity variable for the momentum variable, a move that often simplifies the analysis of a system's dynamics.

In Recognition Science, this standard structure is not assumed but derived. The framework's cost function, the J-action, reduces to the standard Lagrangian in the small-strain limit, and from that starting point the Hamiltonian formulation follows as a theorem. The machine-checked library of formal theorems in the module Action.Hamiltonian proves that the Euler-Lagrange equation, Newton's second law, implies Hamilton's equations. The first, q̇ = p/m, is definitional; the second, ṗ = -V'(q), is the Euler-Lagrange equation itself.

The module also establishes energy conservation. Along a trajectory satisfying the Euler-Lagrange equation, the total energy E(t) = H(γ(t), p(t)) is constant. This is a concrete instance of Noether's theorem, which links time-translation symmetry to the conservation of energy. The proof relies on the chain rule to show that the time derivative of the energy is zero, a fact that follows directly from the equation of motion.

What this means in plain terms: the framework does not merely borrow the Hamiltonian from textbook mechanics; it rebuilds it from a more fundamental action principle. The result is a formal guarantee that the Hamiltonian formulation is a consequence of the J-action, not an independent postulate. This is a step toward showing that the framework's single cost function contains the structure of classical mechanics within it.

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

This does not claim the Hamiltonian formulation is derived from the full J-action, only from its small-strain limit. This does not claim the J-action itself is the only possible action principle. This does not claim the Hamiltonian is defined for all possible potentials V(q).

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