Prove2Me

Centre-of-momentum frame: invariant mass == total energy /c2/c^2

Proved
MassEnergyEquivalence.invariantMass_zero_momentum

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 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, with relativistic energies Ei=γimic2E_i=\gamma_im_ic^2 and momenta pi=γimivi\mathbf p_i=\gamma_im_i\mathbf v_i. If the total momentum vanishes, ∑i∈spi=0\sum_{i\in s}\mathbf p_i = 0 (centre-of-momentum frame), then the invariant mass of the system equals its total energy divided by c2c^2:

M=1c2∑i∈sEi.M = \frac{1}{c^2}\sum_{i\in s}E_i .

In particular the kinetic energy of the constituents (e.g. of the molecules of a gas in a container) contributes to the mass of the system.

Preamble
import Mathlib
import Definitions.Def_MassEnergyEquivalence_Defs

open MassEnergyEquivalence Filter Asymptotics Topology
Formal statement
namespace MassEnergyEquivalence

theorem invariantMass_zero_momentum {ι : Type*} (s : Finset ι) (c : ℝ) (m : ι → ℝ)
    (v : ι → Vec3) (hc : 0 < c) (hm : ∀ i ∈ s, 0 ≤ m i) (hv : ∀ i ∈ s, ‖v i‖ < c)
    (hp : ∑ i ∈ s, relMomentum c (m i) (v i) = 0) :
    invariantMass s c m v = (∑ i ∈ s, relEnergy c (m i) (v i)) / 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.), §Composite systems (p. 3): the invariant mass "is defined as the total energy (divided by c2c^2) in the center of momentum frame. The center of momentum frame is defined so that the system has zero total momentum"; container-of-gas example.
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, functions m:ι→Rm:\iota\to\mathbb R and v:ι→R3\mathbf v:\iota\to\mathbb R^3 such that c>0c>0, mi≥0m_i\ge0 and ∣vi∣<c|\mathbf v_i|<c for all i∈si\in s, and ∑i∈sγimivi=0\sum_{i\in s}\gamma_i m_i\mathbf v_i = \mathbf 0 (where γi=1/1−∣vi∣2/c2\gamma_i = 1/\sqrt{1-|\mathbf v_i|^2/c^2}):

1c2(∑i∈sγimic2)2−c2∣∑i∈sγimivi∣2=1c2∑i∈sγimic2.\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} = \frac{1}{c^2}\sum_{i\in s}\gamma_i m_i c^2 .

The empty system s=∅s=\emptyset is allowed (both sides 00). Nothing is assumed about mi,vim_i,\mathbf v_i for i∉si\notin s.

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