Conservation of mechanical energy in a conservative force field

Proved

ConservationLaws.mechanical_energy_conservation

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

conservation-lawenergymechanics

A particle of mass $m > 0$ moves in $\mathbb{R}^d$ under a force derived from a differentiable potential $V : \mathbb{R}^d \to \mathbb{R}$ , i.e. $m\,\ddot x(t) = -\nabla V(x(t))$ . Then the mechanical energy

E(t) = \tfrac12 m\,\|\dot x(t)\|^2 + V(x(t))

is constant in time.

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem mechanical_energy_conservation
    {d : ℕ} (m : ℝ) (hm : 0 < m)
    (V : EuclideanSpace ℝ (Fin d) → ℝ) (hV : Differentiable ℝ V)
    (x v a : ℝ → EuclideanSpace ℝ (Fin d))
    (hx : ∀ t, HasDerivAt x (v t) t)
    (hv : ∀ t, HasDerivAt v (a t) t)
    (hnewton : ∀ t, m • a t = -gradient V (x t)) :
    ∀ t s, (1 / 2 : ℝ) * m * ‖v t‖ ^ 2 + V (x t) = (1 / 2 : ℝ) * m * ‖v s‖ ^ 2 + V (x s) := by sorry

end ConservationLaws

Source

Wikipedia, "Conservation of energy" (uploaded PDF), https://en.wikipedia.org/wiki/Conservation_of_energy, sections on kinetic and potential energy (vis viva, Galileo's interconversion of potential and kinetic energy); Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Relation to force"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as drafter, non-blind

Disclosure: NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent or blind testimony and must not be treated as such by any reviewer. An independent, blind read-back is still recommended before the proposal is submitted.

Fix a natural number $d$ and a real $m > 0$ . Let $V : \mathbb{R}^d \to \mathbb{R}$ be (Fréchet) differentiable at every point of Euclidean space $\mathbb{R}^d$ . Let $x, v, a : \mathbb{R} \to \mathbb{R}^d$ with: for every $t$ , $x$ is differentiable at $t$ with derivative $v(t)$ , and $v$ is differentiable at $t$ with derivative $a(t)$ . Assume for every $t$ :

m\,a(t) = -\nabla V(x(t)),

where $\nabla V(y)$ is the gradient of $V$ at $y$ (the vector representing the derivative of $V$ at $y$ via the Euclidean inner product). Conclusion: for all real $t, s$ ,

\tfrac12 m\|v(t)\|^2 + V(x(t)) = \tfrac12 m\|v(s)\|^2 + V(x(s)).

No continuity of $\nabla V$ is assumed beyond what differentiability of $V$ gives. Edge case $d = 0$ : $V$ is a constant and $v = 0$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph