Energy–momentum relation $E^2 = (pc)^2 + (mc^2)^2$

Proved

EnergyMomentum.energy_momentum_relation

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

mathematical-physicsspecial-relativity

Let $c > 0$ be the speed of light and consider a free body of mass $m > 0$ moving with velocity $\mathbf v \in \mathbb R^3$ with $|\mathbf v| < c$ . Let $E = \gamma m c^2$ be its total energy and $\mathbf p = \gamma m \mathbf v$ its relativistic momentum, where $\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}$ . Then, with $p = |\mathbf p|$ ,

E^2 = (pc)^2 + (mc^2)^2 .

This is the relativistic dispersion relation; it expresses the energy through the momentum and the rest mass alone and extends $E_0 = mc^2$ to moving bodies.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Energy–momentum relation (1): `E² = (p c)² + (m c²)²` for a free massive body. -/
theorem energy_momentum_relation (m c : ℝ) (v : Vec3)
    (hc : 0 < c) (hm : 0 < m) (hv : ‖v‖ < c) :
    energy m c v ^ 2 = (‖momentum m c v‖ * c) ^ 2 + (m * c ^ 2) ^ 2 := 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), lead section, equation (1).

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 numbers $m, c$ and every vector $\mathbf v \in \mathbb R^3$ , assuming

$0 < c$ ,
$0 < m$ ,
$|\mathbf v| < c$ (Euclidean norm),

the following equality of real numbers holds:

\mathrm{energy}(m,c,\mathbf v)^2 = \big(|\mathrm{momentum}(m,c,\mathbf v)|\cdot c\big)^2 + (m c^2)^2 ,

where $\mathrm{energy}(m,c,\mathbf v) = \gamma m c^2$ , $\mathrm{momentum}(m,c,\mathbf v) = \gamma m\,\mathbf v$ and $\gamma = 1/\sqrt{1 - (|\mathbf v|/c)^2}$ . Under the hypotheses, $1 - (|\mathbf v|/c)^2 \in (0,1]$ , so $\gamma$ is the genuine (finite, $\ge 1$ ) Lorentz factor and no junk value of division or square root is reached. The hypotheses are jointly satisfiable (e.g. $c = 1$ , $m = 1$ , $\mathbf v = 0$ ). The case $\mathbf v = 0$ is included.

View graph

Energy–momentum relation E2=(pc)2+(mc2)2E^2 = (pc)^2 + (mc^2)^2E2=(pc)2+(mc2)2

Energy–momentum relation $E^2 = (pc)^2 + (mc^2)^2$