Encyclopedia Action Action Hamiltonian Hamiltonian Status

ARTICLE 4 claims 3 theorems 1 model

Action Hamiltonian Hamiltonian Status

A machine-checked library reports that its Hamiltonian mechanics module contains real definitions and proofs, with no unproved axioms.

Verify this page

Hamiltonian status

The Hamiltonian is a function that gives the total energy of a system in terms of position and momentum. For a particle of mass m moving in a potential V, it is H(q, p) = p²/(2m) + V(q). The two Hamilton equations, q̇ = ∂H/∂p and ṗ = -∂H/∂q, describe how position and momentum change over time. This formulation is equivalent to Newton's second law and to the Lagrangian approach, which uses a function L(q, q̇) = ½ m q̇² - V(q) instead.

The standard derivation starts with the Lagrangian and defines the conjugate momentum as p = ∂L/∂q̇ = m q̇. The Hamiltonian is then the Legendre transform H = p q̇ - L, which gives p²/(2m) + V(q). The first Hamilton equation, q̇ = p/m, is just the definition of momentum. The second, ṗ = -V'(q), is Newton's second law m q̈ = -V'(q) written in terms of momentum. This equivalence between the Lagrangian and Hamiltonian pictures was established by William Rowan Hamilton in the 1830s.

In Recognition Science, the framework models physical laws through a cost function that measures the cost of recognition events. Its library contains a machine-checked collection of formal theorems. Within this framework, the module Action.Hamiltonian derives the Hamiltonian formulation from the J-action, which is the framework's cost function, by taking the small-strain limit to recover the standard Lagrangian. The declaration hamiltonian_status is a simple string that reports the module contains the standard Hamiltonian, the statement that Hamilton's equations follow from the Euler-Lagrange equation, and a statement of energy conservation, with zero unproved axioms.

The statement hamilton_equations_from_EL proves that if a trajectory satisfies the Euler-Lagrange equation, then it satisfies both Hamilton equations. The statement energy_conservation proves that the total energy E(t) = H(q(t), p(t)) is constant along such a trajectory. This is a special case of Noether's theorem, which says time-translation invariance implies energy conservation. The proofs require standard regularity assumptions: the potential V and trajectory γ must be differentiable, and the trajectory must have a second derivative.

The status declaration does not claim that the J-action itself is the only possible action, nor that the small-strain limit is the only way to connect the framework to classical mechanics. It does not claim that the Hamiltonian formulation is derived from the framework's axioms alone; it starts from the standard Lagrangian. The declaration is a bookkeeping device that records what has been proved, not a new physical law.

THEOREM 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₂
MODEL hamiltonian_status · IndisputableMonolith/Action/Hamiltonian.lean
hamiltonian_status · IndisputableMonolith/Action/Hamiltonian.lean:163 
def hamiltonian_status : String :=
  "Action.Hamiltonian: standardHamiltonian, hamilton_equations_from_EL, energy_conservation (0 sorry, 0 axiom)"

What this page does not claim

The J-action is the only possible action from which the standard Lagrangian can be derived. The Hamiltonian formulation is derived solely from the framework's axioms without starting from the standard Lagrangian. The status declaration proves any new physical law beyond what is contained in the standard Hamiltonian mechanics.

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