Rest frame: $\mathbf p = 0$ and $E = E_0 = mc^2$

Proved

EnergyMomentum.rest_frame

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

mathematical-physicsspecial-relativity

For a body of mass $m$ at rest ( $\mathbf v = 0$ ) and any value of the constant $c$ , the relativistic momentum vanishes and the total energy equals the rest energy:

\mathbf p = 0, \qquad E = E_0 = mc^2 .

This is the centre-of-momentum frame of a single particle, in which (1) reduces to mass–energy equivalence.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Centre-of-momentum frame of one particle: at rest, `p = 0` and `E = E₀ = m c²`. -/
theorem rest_frame (m c : ℝ) :
    momentum m c 0 = 0 ∧ energy m c 0 = restEnergy m c ∧ restEnergy m c = 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), §Special cases → Centre-of-momentum frame (one particle).

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$ and $c$ (no sign or nonvanishing conditions), with $\mathbf v = 0 \in \mathbb R^3$ , the following three equalities hold simultaneously:

$\mathrm{momentum}(m,c,0) = 0$ (the zero vector);
$\mathrm{energy}(m,c,0) = \mathrm{restEnergy}(m,c)$ ;
$\mathrm{restEnergy}(m,c) = m c^2$ .

Here $\mathrm{momentum}(m,c,\mathbf v) = \gamma m\mathbf v$ , $\mathrm{energy}(m,c,\mathbf v) = \gamma m c^2$ , with $\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}$ ; at $\mathbf v = 0$ , $|\mathbf v|/c = 0$ for every $c$ (including $c = 0$ , by the convention $x/0 = 0$ ), so $\gamma = 1$ . Clause 3 is true by definition of $\mathrm{restEnergy}$ .

View graph

Rest frame: p=0\mathbf p = 0p=0 and E=E0=mc2E = E_0 = mc^2E=E0​=mc2

Rest frame: $\mathbf p = 0$ and $E = E_0 = mc^2$