Prove2Me

Mass is not additive: ∑imi≤M\sum_i m_i \le M, with equality iff the constituents are mutually at rest

Proved
MassEnergyEquivalence.sum_mass_le_invariantMass

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

mathematical-physicsspecial-relativity

Let c>0c>0 and consider a finite system of free (non-interacting) particles i∈si\in s with rest masses mi≥0m_i\ge0 and velocities vi∈R3\mathbf v_i\in\mathbb R^3, ∣vi∣<c|\mathbf v_i|<c. Let MM be the invariant mass of the system. Then

∑i∈smi  ≤  M,\sum_{i\in s} m_i \;\le\; M ,

and, if every mi>0m_i>0, equality holds if and only if all the particles have the same velocity, i.e. they are at rest as observed from the centre-of-momentum frame.

Thus the mass of a system is in general not the sum of the masses of its parts: the kinetic energy of the constituents in the centre-of-momentum frame contributes to the rest mass, and the masses add up only if the constituents are at rest in that frame and do not interact.

Preamble
import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology
Formal statement
namespace MassEnergyEquivalence

theorem sum_mass_le_invariantMass {ι : Type*} (s : Finset ι) (c : ℝ) (m : ι → ℝ)
    (v : ι → Vec3) (hc : 0 < c) (hm : ∀ i ∈ s, 0 ≤ m i) (hv : ∀ i ∈ s, ‖v i‖ < c) :
    ∑ i ∈ s, m i ≤ invariantMass s c m v ∧
      ((∀ i ∈ s, 0 < m i) →
        (invariantMass s c m v = ∑ i ∈ s, m i ↔ ∀ i ∈ s, ∀ j ∈ s, v i = v j)) := 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 almost never additive … The rest mass of an object is the total energy of all the parts, including kinetic energy, as observed from the center of momentum frame … The masses add up only if the constituents are at rest (as observed from the center of momentum frame) and do not attract or repel".
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 type ι\iota, finite set s⊆ιs\subseteq\iota, real cc, m:ι→Rm:\iota\to\mathbb R, v:ι→R3\mathbf v:\iota\to\mathbb R^3 with c>0c>0, mi≥0m_i\ge0 and ∣vi∣<c|\mathbf v_i|<c for all i∈si\in s, writing

M=1c2(∑i∈sγimic2)2−c2∣∑i∈sγimivi∣2,γi=1/1−∣vi∣2/c2M = \frac{1}{c^2}\sqrt{\Big(\sum_{i\in s}\gamma_i m_i c^2\Big)^2 - c^2\Big|\sum_{i\in s}\gamma_i m_i\mathbf v_i\Big|^2},\qquad \gamma_i = 1/\sqrt{1-|\mathbf v_i|^2/c^2}

(truncated square root: a negative radicand would give 00), both of the following hold:

  1. ∑i∈smi≤M\sum_{i\in s} m_i \le M;
  2. if mi>0m_i>0 for every i∈si\in s, then M=∑i∈smiM = \sum_{i\in s} m_i holds if and only if vi=vj\mathbf v_i = \mathbf v_j for all i,j∈si,j\in s.

The empty system (M=0=∑miM=0=\sum m_i, condition vacuous) and one-particle systems are included. Particles interact in no way in this model (no potential energy term).

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