Rest mass is frame-independent: $E^2 - c^2|\mathbf p|^2$ is boost-invariant

Proved

MassEnergyEquivalence.invariant_under_boost

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

mathematical-physicsspecial-relativity

Let $c>0$ and let $u$ be a speed with $|u|<c$ . For an energy $E$ and momentum $\mathbf p=(p_1,p_2,p_3)$ measured in one inertial frame, let $(E',\mathbf p')$ be the energy and momentum measured in a frame moving with velocity $u$ along the first axis:

E' = \gamma_u\,(E - u\,p_1),\qquad \mathbf p' = \Big(\gamma_u\big(p_1 - \tfrac{uE}{c^2}\big),\,p_2,\,p_3\Big),\qquad \gamma_u = \frac{1}{\sqrt{1-u^2/c^2}} .

Then

E'^2 - c^2|\mathbf p'|^2 = E^2 - c^2|\mathbf p|^2 .

Since by the energy–momentum relation $E^2-c^2|\mathbf p|^2 = (m_0c^2)^2$ , the rest (invariant) mass is the same for all inertial frames, independent of the motion of the observer; this holds equally for the total energy and momentum of a system of particles, whose invariant mass is the same for all observers.

Formalization Note Only boosts along the first coordinate axis are covered; together with rotations (which preserve $|\mathbf p|$ ) they generate all changes of inertial frame. $E$ and $\mathbf p$ are arbitrary, so the statement applies both to single particles and to system totals.

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem invariant_under_boost (c u E : ℝ) (p : Vec3) (hc : 0 < c) (hu : |u| < c) :
    boostEnergy c u E p ^ 2 - c ^ 2 * ‖boostMomentum c u E p‖ ^ 2 = E ^ 2 - c ^ 2 * ‖p‖ ^ 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.), §Mass in special relativity (p. 2): "The rest mass is the same for all inertial frames, as it is independent of the motion of the observer"; §Composite systems (p. 3): "the invariant mass of the system … is the same for all observers, even those in relative motion".

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, u, E$ and $\mathbf p=(p_1,p_2,p_3)\in\mathbb R^3$ with $c>0$ and $|u|<c$ , setting $\gamma_u = 1/\sqrt{1-u^2/c^2}$ , $E' = \gamma_u (E - u p_1)$ and $\mathbf p' = (\gamma_u(p_1 - uE/c^2), p_2, p_3)$ :

E'^2 - c^2\,|\mathbf p'|^2 = E^2 - c^2\,|\mathbf p|^2,

with $|\cdot|$ the Euclidean norm on $\mathbb R^3$ . No sign or other conditions on $E$ or $\mathbf p$ ; $u=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

Rest mass is frame-independent: E2−c2∣p∣2E^2 - c^2|\mathbf p|^2E2−c2∣p∣2 is boost-invariant

Rest mass is frame-independent: $E^2 - c^2|\mathbf p|^2$ is boost-invariant