Encyclopedia Action Action Hamiltonian Total Energy

ARTICLE 3 claims 2 theorems 1 model

Action Hamiltonian Total Energy

In classical mechanics, the total energy of a moving particle is the sum of its kinetic and potential energy, a quantity that stays constant along any physical trajectory.

Verify this page

Total energy

The total energy of a particle is the sum of its kinetic energy, the energy of motion, and its potential energy, the energy of position. For a particle of mass m moving along a path q(t) under a potential V(q), the total energy is E = p²/(2m) + V(q), where p is the momentum. This is the standard Hamiltonian of classical mechanics, the function that generates the equations of motion. The Recognition Science declaration totalEnergy defines exactly this quantity: it evaluates the standard Hamiltonian at the particle's position and conjugate momentum at a given time.

The declaration's real content is a conservation theorem. The framework's machine-checked library proves that if a trajectory satisfies the Euler-Lagrange equation, which is Newton's second law, then the total energy is constant in time: E(t₁) = E(t₂) for any two times t₁ and t₂. This is a special case of Noether's theorem, which ties energy conservation to time-translation invariance. The proof requires the standard regularity conditions: the potential and trajectory must be differentiable, and the trajectory must have a second derivative. The theorem is a formal derivation, checked by the Lean kernel with no axioms beyond the standard three.

The definition itself is a choice, not a discovery. It selects the standard Hamiltonian for a particle in a potential, the small-strain limit of the framework's more general J-action. The conservation theorem, by contrast, is a proved result: it derives a physical law from the Euler-Lagrange equation. The framework's library also derives Hamilton's equations from the same starting point, showing that the position velocity equals p/m and the momentum change equals minus the force, both as corollaries of the Euler-Lagrange equation.

What the declaration does not claim is broader. It does not claim that this Hamiltonian is the only possible one, nor that the J-action itself is the unique action principle. It does not claim that energy conservation holds for systems with explicit time dependence, where Noether's theorem does not apply. And it does not claim that the standard Hamiltonian is derived from the framework's cost function; it is taken as the small-strain limit, a modeling choice with a proved consequence.

THEOREM totalEnergy · IndisputableMonolith/Action/Hamiltonian.lean
totalEnergy · IndisputableMonolith/Action/Hamiltonian.lean:97 
/-- The total energy of a trajectory: `E(t) = H(γ(t), p(t))`. -/
noncomputable def totalEnergy (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=
  standardHamiltonian m V (γ t) (conjugateMomentum m γ 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 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

What this page does not claim

The declaration does not claim that the standard Hamiltonian is the unique or fundamental action principle. It does not claim that energy is conserved for time-dependent potentials. It does not claim that the J-action itself is derived from the cost function.

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