Energy–momentum relation: $E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4$

Proved

MassEnergyEquivalence.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, let $m_0\ge 0$ be the rest mass of a body, and let $\mathbf v\in\mathbb R^3$ be its velocity, with $|\mathbf v|<c$ . With Lorentz factor $\gamma=1/\sqrt{1-|\mathbf v|^2/c^2}$ , relativistic energy $E_{\mathrm{rel}}=\gamma m_0c^2$ and relativistic momentum $\mathbf p=\gamma m_0\mathbf v$ ,

E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4 .

This is the extension of Einstein's formula $E=mc^2$ to systems in motion (the energy–momentum relation): the relativistic energy depends on both the rest mass and the momentum, and it reduces to $E_{\mathrm{rel}}=m_0c^2$ when the momentum vanishes.

Formalization Note The body is modelled by its rest mass and velocity; energy and momentum are the derived quantities $\gamma m_0c^2$ and $\gamma m_0\mathbf v$ from the mission's definition file.

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem energy_momentum_relation (c m : ℝ) (v : Vec3) (hc : 0 < c) (hm : 0 ≤ m)
    (hv : ‖v‖ < c) :
    relEnergy c m v ^ 2 - ‖relMomentum c m v‖ ^ 2 * c ^ 2 = m ^ 2 * c ^ 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.), §Extension for systems in motion (pp. 5–6), first display:

E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4

; with

E=\gamma mc^2

from §Low-speed approximation (p. 6).

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$ , every real $m$ and every $\mathbf v\in\mathbb R^3$ such that $c>0$ , $m\ge 0$ and $|\mathbf v|<c$ :

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

Here $\gamma m c^2$ is the defined relativistic energy and $\gamma m \mathbf v$ the defined relativistic momentum. Because $|\mathbf v|<c$ and $c>0$ , the radicand $1-|\mathbf v|^2/c^2$ lies in $(0,1]$ , so no junk value of the square root or of division occurs. The case $m=0$ is included (both sides are $0$ ); $\mathbf v=0$ is included.

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

Energy–momentum relation: Erel2−∣p∣2c2=m02c4E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4Erel2​−∣p∣2c2=m02​c4

Energy–momentum relation: $E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4$