$E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}$

Proved

MassEnergyEquivalence.relEnergy_eq_sqrt

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

mathematical-physicsspecial-relativity

Let $c>0$ , $m_0\ge 0$ and $\mathbf v\in\mathbb R^3$ with $|\mathbf v|<c$ . With $E_{\mathrm{rel}}=\gamma m_0c^2$ , $\mathbf p=\gamma m_0\mathbf v$ and $p=|\mathbf p|$ ,

E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}.

This is the third form of the energy–momentum relation given in the article; it exhibits the relativistic energy as a function of rest mass and momentum, and reduces to $E_{\mathrm{rel}}=m_0c^2$ when $p=0$ .

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem relEnergy_eq_sqrt (c m : ℝ) (v : Vec3) (hc : 0 < c) (hm : 0 ≤ m) (hv : ‖v‖ < c) :
    relEnergy c m v = Real.sqrt ((m * c ^ 2) ^ 2 + (‖relMomentum c m v‖ * c) ^ 2) := 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 (p. 6), third display:

E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}

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\ge 0$ , $|\mathbf v|<c$ :

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

where the outer $\sqrt{\cdot}$ is the non-negative real square root (its argument is a sum of squares, hence non-negative). The left side is the defined relativistic energy, $|\gamma m \mathbf v|$ the Euclidean norm of the defined relativistic momentum.

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

Erel=(m0c2)2+(pc)2E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}Erel​=(m0​c2)2+(pc)2​

$E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}$