Energy in terms of momentum: $E = mc^2\sqrt{1 + (p/mc)^2}$

Proved

EnergyMomentum.energy_eq_sqrt_momentum

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

mathematical-physicsspecial-relativity

Let $c > 0$ , $m > 0$ and $\mathbf v\in\mathbb R^3$ with $|\mathbf v| < c$ . The total energy $E = \gamma mc^2$ and the momentum magnitude $p = |\gamma m \mathbf v|$ satisfy

E = mc^2\sqrt{1 + \left(\frac{p}{mc}\right)^2}.

Squaring both sides and rearranging yields the energy–momentum relation (1).

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Energy in terms of three-momentum: `E = m c² √(1 + (p / (m c))²)`. -/
theorem energy_eq_sqrt_momentum (m c : ℝ) (v : Vec3)
    (hc : 0 < c) (hm : 0 < m) (hv : ‖v‖ < c) :
    energy m c v = m * c ^ 2 * Real.sqrt (1 + (‖momentum m c v‖ / (m * c)) ^ 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), §Origins and derivation of the equation → Heuristic approach for massive particles; also §Classical correspondence (first display).

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

\mathrm{energy}(m,c,\mathbf v) = m c^2 \sqrt{1 + \left(\frac{|\mathrm{momentum}(m,c,\mathbf v)|}{m c}\right)^2},

where $\mathrm{energy}(m,c,\mathbf v) = \gamma m c^2$ , $\mathrm{momentum}(m,c,\mathbf v) = \gamma m \mathbf v$ , $\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}$ . No junk values occur under the hypotheses.

View graph

Energy in terms of momentum: E=mc21+(p/mc)2E = mc^2\sqrt{1 + (p/mc)^2}E=mc21+(p/mc)2​

Energy in terms of momentum: $E = mc^2\sqrt{1 + (p/mc)^2}$