Relativistic mass: $m_{\mathrm{rel}} = m_0 + E_k/c^2 \ge m_0$ , with equality only at rest

Proved

MassEnergyEquivalence.relMass_properties

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

mathematical-physicsspecial-relativity

Let $c>0$ , $m_0\ge0$ and $\mathbf v\in\mathbb R^3$ with $|\mathbf v|<c$ . Let $m_{\mathrm{rel}}=E_{\mathrm{rel}}/c^2$ be the relativistic mass and $E_k=E_{\mathrm{rel}}-m_0c^2$ the kinetic energy. Then:

$m_{\mathrm{rel}} = m_0 + \dfrac{E_k}{c^2}$ (the relativistic mass exceeds the rest mass by the mass associated with the kinetic energy);
$m_0 \le m_{\mathrm{rel}}$ (the rest mass is the smallest possible value of the relativistic mass);
if $m_0>0$ , then $m_{\mathrm{rel}} = m_0$ if and only if $\mathbf v = 0$ (a moving massive object has strictly larger relativistic mass than at rest).

m_0 \le m_{\mathrm{rel}} = m_0 + \frac{E_k}{c^2}.

Preamble

import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology

Formal statement

namespace MassEnergyEquivalence

theorem relMass_properties (c m : ℝ) (v : Vec3) (hc : 0 < c) (hm : 0 ≤ m) (hv : ‖v‖ < c) :
    relMass c m v = m + kineticEnergy c m v / c ^ 2 ∧ m ≤ relMass c m v ∧
      (0 < m → (relMass c m v = m ↔ v = 0)) := 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 smallest possible value of the relativistic mass of the object"; §Relativistic mass (p. 2): "The relativistic mass of a moving object is larger than the relativistic mass of an object at rest … greater than the rest mass by an amount equal to the mass associated with the kinetic energy of the object";

m_{\mathrm{rel}} = E/c^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\ge0$ , $|\mathbf v|<c$ , writing $\gamma = 1/\sqrt{1-|\mathbf v|^2/c^2}$ , $m_{\mathrm{rel}} = \gamma m c^2/c^2$ and $E_k = \gamma m c^2 - m c^2$ , the following three facts hold simultaneously:

$m_{\mathrm{rel}} = m + E_k/c^2$ ;
$m \le m_{\mathrm{rel}}$ ;
if additionally $m>0$ , then $m_{\mathrm{rel}} = m \iff \mathbf v = \mathbf 0$ .

For $m=0$ only items 1–2 carry content (both sides are $0$ ).

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

Relativistic mass: mrel=m0+Ek/c2≥m0m_{\mathrm{rel}} = m_0 + E_k/c^2 \ge m_0mrel​=m0​+Ek​/c2≥m0​, with equality only at rest

Relativistic mass: $m_{\mathrm{rel}} = m_0 + E_k/c^2 \ge m_0$ , with equality only at rest