Work–energy theorem: $\Delta(\tfrac12 m\|v\|^2) = \int \langle F, v\rangle\,dt$

Proved

ConservationLaws.work_energy_theorem

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

energymechanicswork

A particle of mass $m > 0$ moves in $\mathbb{R}^d$ under a continuous time-dependent force $F(t)$ , with $m\,\ddot x(t) = F(t)$ . Then for all times $t_0, t_1$ ,

\tfrac12 m\|v(t_1)\|^2 - \tfrac12 m\|v(t_0)\|^2 = \int_{t_0}^{t_1} \langle F(t), v(t)\rangle\,dt,

i.e. the change in kinetic energy equals the work done by the force.

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem work_energy_theorem
    {d : ℕ} (m : ℝ) (hm : 0 < m)
    (F : ℝ → EuclideanSpace ℝ (Fin d)) (hF : Continuous F)
    (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 = F t) :
    ∀ t₀ t₁, (1 / 2 : ℝ) * m * ‖v t₁‖ ^ 2 - (1 / 2 : ℝ) * m * ‖v t₀‖ ^ 2 =
      ∫ t in t₀..t₁, inner ℝ (F t) (v t) := by sorry

end ConservationLaws

Source

Wikipedia, "Conservation of energy" (uploaded PDF), https://en.wikipedia.org/wiki/Conservation_of_energy (energy transferred as work); Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Relation to force" (Newton's second law

F = m a

)

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 $F : \mathbb{R} \to \mathbb{R}^d$ be continuous. Let $x, v, a : \mathbb{R} \to \mathbb{R}^d$ with, for every $t$ : $x$ differentiable at $t$ with derivative $v(t)$ , $v$ differentiable at $t$ with derivative $a(t)$ , and $m\,a(t) = F(t)$ . Conclusion: for all real $t_0, t_1$ (in either order),

\tfrac12 m\|v(t_1)\|^2 - \tfrac12 m\|v(t_0)\|^2 = \int_{t_0}^{t_1} \langle F(t), v(t)\rangle\,dt,

where $\langle\cdot,\cdot\rangle$ is the Euclidean inner product and the integral is the oriented interval integral (equal to minus the integral over $[t_1,t_0]$ when $t_1 < t_0$ ). The position $x$ appears only through its derivative relation and plays no other role.

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

Work–energy theorem: Δ(12m∥v∥2)=∫⟨F,v⟩ dt\Delta(\tfrac12 m\|v\|^2) = \int \langle F, v\rangle\,dtΔ(21​m∥v∥2)=∫⟨F,v⟩dt

Work–energy theorem: $\Delta(\tfrac12 m\|v\|^2) = \int \langle F, v\rangle\,dt$