Classical correspondence: $E = mc^2 + \tfrac12 mv^2 + o(v^2)$

Proved

EnergyMomentum.classical_correspondence

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

mathematical-physicsspecial-relativity

Let $c>0$ and $m>0$ . For velocities $\mathbf v\in\mathbb R^3$ , the total energy $E(\mathbf v) = \gamma mc^2$ satisfies

\lim_{\mathbf v\to 0,\ \mathbf v\ne 0} \frac{E(\mathbf v) - mc^2 - \tfrac12 m|\mathbf v|^2}{|\mathbf v|^2} = 0 ,

that is, $E = mc^2 + \tfrac12 m|\mathbf v|^2 + o(|\mathbf v|^2)$ as $\mathbf v \to 0$ : to first order the energy is the rest energy plus the classical kinetic energy.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Classical correspondence: `E = m c² + ½ m v² + o(v²)` as `v → 0`. -/
theorem classical_correspondence (m c : ℝ) (hc : 0 < c) (hm : 0 < m) :
    Filter.Tendsto
      (fun v : Vec3 => (energy m c v - m * c ^ 2 - m * ‖v‖ ^ 2 / 2) / ‖v‖ ^ 2)
      (nhdsWithin 0 {0}ᶜ) (nhds 0) := by sorry

end EnergyMomentum

Source

Wikipedia, *Energy–momentum relation*, https://en.wikipedia.org/wiki/Energy%E2%80%93momentum_relation (PDF snapshot supplied by the proposer), §Special cases → Classical correspondence (expansion

E \approx mc^2 + \tfrac12 mv^2

for

v \ll c

Read-back

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

Disclosure — this is NOT a blind read-back. It was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent testimony and must not be mistaken for an independent audit; reviewers should check it against the Lean code themselves (or replace it with a blind read-back).

For all real $m, c$ with $0<c$ and $0<m$ : the real-valued function

\mathbf v \longmapsto \frac{\mathrm{energy}(m,c,\mathbf v) - m c^2 - m|\mathbf v|^2/2}{|\mathbf v|^2}, \qquad \mathbf v\in\mathbb R^3,

tends to $0$ as $\mathbf v$ tends to $0$ through nonzero vectors (limit along the punctured neighbourhood filter of $0$ in $\mathbb R^3$ ). Here $\mathrm{energy}(m,c,\mathbf v) = \gamma m c^2$ with $\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}$ ; for $|\mathbf v| \ge c$ this $\gamma$ would be the junk value $0$ , but only small $\mathbf v$ matter for the limit. The value at $\mathbf v = 0$ (where Lean's division gives $0$ ) is excluded by the filter and plays no role.

View graph

Classical correspondence: E=mc2+12mv2+o(v2)E = mc^2 + \tfrac12 mv^2 + o(v^2)E=mc2+21​mv2+o(v2)

Classical correspondence: $E = mc^2 + \tfrac12 mv^2 + o(v^2)$