Centre-of-momentum frame: $\sum_n E_n = Mc^2$

Proved

EnergyMomentum.centre_of_momentum_energy

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

mathematical-physicsspecial-relativity

Let $c>0$ and consider a finite system of particles indexed by a finite set $S$ , with masses $m_n>0$ and velocities $|\mathbf v_n|<c$ , energies $E_n$ , momenta $\mathbf p_n$ and four-momenta $\mathbf P_n$ as above. If the system is observed in its centre-of-momentum frame, i.e.

\sum_{n\in S}\mathbf p_n = \mathbf 0,

then the total energy equals the invariant mass $M$ of the total four-momentum times $c^2$ :

\sum_{n\in S} E_n = Mc^2 .

For instance, the internal kinetic energy of a gas in a container at rest is weighed as mass.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Centre-of-momentum frame: if `∑ 𝐩ₙ = 0` then `∑ Eₙ = M c²`. -/
theorem centre_of_momentum_energy {ι : Type} (s : Finset ι) (m : ι → ℝ) (v : ι → Vec3)
    (c : ℝ) (hc : 0 < c) (hm : ∀ n ∈ s, 0 < m n) (hv : ∀ n ∈ s, ‖v n‖ < c)
    (hcom : ∑ n ∈ s, momentum (m n) c (v n) = 0) :
    ∑ n ∈ s, energy (m n) c (v n)
      = invariantMass c (∑ n ∈ s, fourMomentum (m n) c (v n)) * c ^ 2 := by sorry

end EnergyMomentum

Source

Wikipedia, *Energy–momentum relation*, https://en.wikipedia.org/wiki/Energy%E2%80%93momentum_relation (PDF snapshot supplied by the proposer), §Many-particle systems → Centre-of-momentum frame.

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; reviewers should check it against the Lean code themselves (or replace it with a blind read-back).

For every type $\iota$ , finite set $S\subseteq\iota$ , functions $m:\iota\to\mathbb R$ , $\mathbf v:\iota\to\mathbb R^3$ and real $c$ , assuming $0<c$ , $0<m_n$ and $|\mathbf v_n|<c$ for all $n\in S$ , and assuming

\sum_{n\in S}\mathrm{momentum}(m_n,c,\mathbf v_n) = \mathbf 0 \in\mathbb R^3,

we have

\sum_{n\in S}\mathrm{energy}(m_n,c,\mathbf v_n) = \mathrm{invariantMass}\Big(c, \sum_{n\in S}\mathrm{fourMomentum}(m_n,c,\mathbf v_n)\Big)\cdot c^2 ,

with $\mathrm{energy} = \gamma_n m_n c^2$ , $\mathrm{momentum} = \gamma_n m_n\mathbf v_n$ , $\mathrm{fourMomentum} = (\mathrm{energy}/c,\mathrm{momentum})$ , $\mathrm{invariantMass}(c,P) = \sqrt{P^0P^0 - \mathbf P\cdot\mathbf P}/c$ . The zero-total-momentum hypothesis is satisfiable (e.g. $S$ empty, or all $\mathbf v_n = 0$ ). If $S$ is empty both sides are $0$ .

View graph

Centre-of-momentum frame: ∑nEn=Mc2\sum_n E_n = Mc^2∑n​En​=Mc2

Centre-of-momentum frame: $\sum_n E_n = Mc^2$