Correspondence principle: $E_k = \tfrac12 m_0v^2 + O(v^4)$

Proved

MassEnergyEquivalence.kineticEnergy_low_speed

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

mathematical-physicsspecial-relativity

Let $c>0$ and $m_0\ge0$ . The relativistic kinetic energy $E_k = m_0c^2(\gamma-1)$ of a body moving with velocity $\mathbf v\in\mathbb R^3$ agrees with the Newtonian kinetic energy up to fourth order in the speed: as $\mathbf v\to 0$ ,

E_k = m_0c^2\left(\frac{1}{\sqrt{1-v^2/c^2}}-1\right) = \frac12 m_0v^2 + O(v^4),\qquad v=|\mathbf v| .

Subtracting the rest energy $m_0c^2$ is what makes the energy of a slowly moving body agree with classical mechanics (correspondence principle); equivalently, for low speeds all but the first two terms of $E\approx m_0c^2+\tfrac12m_0v^2$ can be ignored.

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem kineticEnergy_low_speed (c m : ℝ) (hc : 0 < c) (hm : 0 ≤ m) :
    (fun v : Vec3 => kineticEnergy c m v - 1 / 2 * m * ‖v‖ ^ 2) =O[𝓝 0]
      (fun v : Vec3 => ‖v‖ ^ 4) := by sorry

end MassEnergyEquivalence

Source

Wikipedia, *Mass–energy equivalence*, https://en.wikipedia.org/wiki/Mass%E2%80%93energy_equivalence (PDF snapshot supplied by the proposer, 25 pp.), §History → Mass–velocity relationship (pp. 10–11):

E_k = m_0c^2(\gamma-1)

and "for small velocities …

E_k = \tfrac12 m_0v^2 + \cdots

"; §Low-speed approximation (p. 6):

E \approx m_0c^2 + \tfrac12 m_0v^2

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; it was produced and uploaded at the proposer's explicit request. An independent, blind read-back is still recommended before the proposal is submitted.

For every real $c>0$ and every real $m\ge0$ : there exist a constant $C$ and a neighbourhood $U$ of $\mathbf 0$ in $\mathbb R^3$ such that for all $\mathbf v\in U$ ,

\Big|\big(\gamma(\mathbf v)\, m c^2 - m c^2\big) - \tfrac12 m |\mathbf v|^2\Big| \le C\,|\mathbf v|^4,\qquad \gamma(\mathbf v)=1/\sqrt{1-|\mathbf v|^2/c^2}.

(This is the big- $O$ statement $f = O(|\mathbf v|^4)$ along the neighbourhood filter of $\mathbf 0$ .) The function is defined on all of $\mathbb R^3$ , including $|\mathbf v|\ge c$ where $\gamma$ takes the junk value $0$ , but only behaviour near $\mathbf 0$ matters.

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

Correspondence principle: Ek=12m0v2+O(v4)E_k = \tfrac12 m_0v^2 + O(v^4)Ek​=21​m0​v2+O(v4)

Correspondence principle: $E_k = \tfrac12 m_0v^2 + O(v^4)$