Power series $E = m_0c^2\big[1 + \tfrac12(v/c)^2 + \tfrac38(v/c)^4 + \tfrac5{16}(v/c)^6 + \cdots\big]$

Proved

MassEnergyEquivalence.relEnergy_hasSum

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

mathematical-physicsspecial-relativity

Let $c>0$ , $m_0\ge0$ and $\mathbf v\in\mathbb R^3$ with speed $v=|\mathbf v|<c$ . The relativistic energy $E=\gamma m_0c^2$ is the sum of the convergent power series

E = m_0c^2\sum_{n=0}^{\infty}\frac{1}{4^n}\binom{2n}{n}\Big(\frac{v}{c}\Big)^{2n} = m_0c^2\left[1+\frac12\Big(\frac vc\Big)^2+\frac38\Big(\frac vc\Big)^4+\frac5{16}\Big(\frac vc\Big)^6+\cdots\right].

This is the expansion used in the article to compare the relativistic energy with its Newtonian approximation.

Formalization Note The article writes only the first four coefficients followed by " $\cdots$ "; the general coefficient $\binom{2n}{n}/4^n$ (the binomial series of $(1-x)^{-1/2}$ ) is the standard one and agrees with $1,\tfrac12,\tfrac38,\tfrac5{16}$ . Convergence is expressed as unconditional summability (HasSum), which for these non-negative terms is ordinary convergence.

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem relEnergy_hasSum (c m : ℝ) (v : Vec3) (hc : 0 < c) (hm : 0 ≤ m) (hv : ‖v‖ < c) :
    HasSum (fun n : ℕ => m * c ^ 2 * ((Nat.centralBinom n : ℝ) / 4 ^ n) * (‖v‖ / c) ^ (2 * n))
      (relEnergy c m v) := 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), first display:

E = m_0c^2[1 + \tfrac12(v/c)^2 + \tfrac38(v/c)^4 + \tfrac5{16}(v/c)^6 + \dots]

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 all real $c, m$ and $\mathbf v\in\mathbb R^3$ with $c>0$ , $m\ge0$ , $|\mathbf v|<c$ : the series

\sum_{n=0}^{\infty} m c^2\cdot\frac{\binom{2n}{n}}{4^n}\cdot\Big(\frac{|\mathbf v|}{c}\Big)^{2n}

is (unconditionally) summable with sum $\gamma m c^2$ , where $\gamma = 1/\sqrt{1-|\mathbf v|^2/c^2}$ . Here $\binom{2n}{n}$ is the central binomial coefficient ( $1,2,6,20,\dots$ ), so the coefficients $\binom{2n}{n}/4^n$ are $1,\tfrac12,\tfrac38,\tfrac5{16},\dots$ ; the $n=0$ term is $mc^2$ .

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

Power series E=m0c2[1+12(v/c)2+38(v/c)4+516(v/c)6+⋯]E = m_0c^2\big[1 + \tfrac12(v/c)^2 + \tfrac38(v/c)^4 + \tfrac5{16}(v/c)^6 + \cdots\big]E=m0​c2[1+21​(v/c)2+83​(v/c)4+165​(v/c)6+⋯]

Power series $E = m_0c^2\big[1 + \tfrac12(v/c)^2 + \tfrac38(v/c)^4 + \tfrac5{16}(v/c)^6 + \cdots\big]$