Third-order approximation: $E = m_0c^2 + \tfrac12m_0v^2\big(1 + \tfrac{3v^2}{4c^2}\big) + O(v^6)$

Proved

MassEnergyEquivalence.relEnergy_third_term

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

mathematical-physicsspecial-relativity

Let $c>0$ and $m_0\ge0$ . Keeping the first three terms of the power series of $E=\gamma m_0c^2$ gives an approximation that is accurate to sixth order in the speed: as $\mathbf v\to0$ ,

E = m_0c^2 + \frac12 m_0v^2\left(1+\frac{3v^2}{4c^2}\right) + O(v^6),\qquad v = |\mathbf v| .

Compared with the Newtonian approximation $E\approx m_0c^2+\tfrac12m_0v^2$ , the relative correction to the kinetic term is $\tfrac{3v^2}{4c^2}$ .

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem relEnergy_third_term (c m : ℝ) (hc : 0 < c) (hm : 0 ≤ m) :
    (fun v : Vec3 => relEnergy c m v
        - (m * c ^ 2 + 1 / 2 * m * ‖v‖ ^ 2 * (1 + 3 * ‖v‖ ^ 2 / (4 * c ^ 2)))) =O[𝓝 0]
      (fun v : Vec3 => ‖v‖ ^ 6) := 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.), §Low-speed approximation (p. 6): "adding in the third term yields

E \approx m_0c^2 + \tfrac12 m_0v^2\left(1 + \tfrac{3v^2}{4c^2}\right)

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\ge 0$ : 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|\gamma(\mathbf v)\, m c^2 - \Big(m c^2 + \tfrac12 m|\mathbf v|^2\Big(1+\frac{3|\mathbf v|^2}{4c^2}\Big)\Big)\Big| \le C\,|\mathbf v|^6,

with $\gamma(\mathbf v) = 1/\sqrt{1-|\mathbf v|^2/c^2}$ (big- $O$ along the neighbourhood filter of $\mathbf 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

Third-order approximation: E=m0c2+12m0v2(1+3v24c2)+O(v6)E = m_0c^2 + \tfrac12m_0v^2\big(1 + \tfrac{3v^2}{4c^2}\big) + O(v^6)E=m0​c2+21​m0​v2(1+4c23v2​)+O(v6)

Third-order approximation: $E = m_0c^2 + \tfrac12m_0v^2\big(1 + \tfrac{3v^2}{4c^2}\big) + O(v^6)$