$E = mc^2$ in the rest frame

Proved

MassEnergyEquivalence.rest_frame_energy

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

mathematical-physicsspecial-relativity

Let $c>0$ and let $m\ge0$ be the rest mass of a body. In its rest frame (velocity $\mathbf v=0$ ) the body has zero relativistic momentum, and its relativistic energy equals its mass times the speed of light squared:

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

This is Einstein's formula, which defines the energy of a particle in its rest frame as the product of its mass with the speed of light squared.

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem rest_frame_energy (c m : ℝ) (hc : 0 < c) (hm : 0 ≤ m) :
    relMomentum c m 0 = 0 ∧ relEnergy c m 0 = m * 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.), lead section and §The formula (p. 1): "

E=mc^2

… defines the energy

E

of a particle in its rest frame as the product of mass

m

with the speed of light squared

c^2

"; §Description (p. 1): in the rest frame the object has no momentum.

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>0$ and every real $m\ge 0$ : the defined relativistic momentum at velocity $\mathbf 0\in\mathbb R^3$ , namely $(\gamma(\mathbf 0)\,m)\cdot\mathbf 0$ , equals the zero vector, and the defined relativistic energy at velocity $\mathbf 0$ , namely $\gamma(\mathbf 0)\, m\, c^2$ with $\gamma(\mathbf 0)=1/\sqrt{1-0/c^2}$ , equals $m c^2$ . No other hypotheses.

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

E=mc2E = mc^2E=mc2 in the rest frame

$E = mc^2$ in the rest frame