Total mass versus individual masses

Proved

EnergyMomentum.invariantMass_pairwise

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

mathematical-physicsspecial-relativity

Let $c>0$ and consider $N$ particles $n = 0,\dots,N-1$ with masses $m_n>0$ and velocities $|\mathbf v_n|<c$ , energies $E_n$ , momenta $\mathbf p_n$ , and let $M$ be the invariant mass of the total four-momentum $\sum_n\mathbf P_n$ . Then

\left(Mc^2\right)^2 - \sum_{n}\left(m_nc^2\right)^2 = 2\sum_{n<k}\left(E_nE_k - c^2\,\mathbf p_n\cdot\mathbf p_k\right).

Since $M$ and the $m_n$ are invariants, the right-hand side is invariant too, although each $E_n$ and $\mathbf p_n$ is measured in a particular frame.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Total mass versus individual masses:
`(M c²)² − ∑ₙ (mₙ c²)² = 2 ∑_{n<k} (Eₙ E_k − c² 𝐩ₙ · 𝐩_k)`. -/
theorem invariantMass_pairwise (N : ℕ) (m : Fin N → ℝ) (v : Fin N → Vec3)
    (c : ℝ) (hc : 0 < c) (hm : ∀ n, 0 < m n) (hv : ∀ n, ‖v n‖ < c) :
    (invariantMass c (∑ n, fourMomentum (m n) c (v n)) * c ^ 2) ^ 2
        - ∑ n, (m n * c ^ 2) ^ 2
      = 2 * ∑ n, ∑ k ∈ Finset.Ioi n,
          (energy (m n) c (v n) * energy (m k) c (v k)
            - c ^ 2 * inner ℝ (momentum (m n) c (v n)) (momentum (m k) c (v k))) := 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 → Relating total mass to individual masses (display after substituting the individual masses

m_n

into (2), and its rearranged form).

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 natural number $N$ , functions $m:\{0,\dots,N-1\}\to\mathbb R$ , $\mathbf v:\{0,\dots,N-1\}\to\mathbb R^3$ and real $c$ , assuming $0<c$ , $0<m_n$ for all $n$ and $|\mathbf v_n|<c$ for all $n$ :

\Big(\mathrm{invariantMass}\Big(c,\sum_{n}\mathrm{fourMomentum}(m_n,c,\mathbf v_n)\Big)\cdot c^2\Big)^2 - \sum_{n}(m_n c^2)^2 = 2\sum_{n}\ \sum_{k>n}\Big(E_nE_k - c^2\,\mathbf p_n\cdot\mathbf p_k\Big),

where all sums over $n$ run over $\{0,\dots,N-1\}$ , the inner sum runs over $k$ with $n<k\le N-1$ , $E_n = \mathrm{energy}(m_n,c,\mathbf v_n) = \gamma_n m_nc^2$ , $\mathbf p_n = \mathrm{momentum}(m_n,c,\mathbf v_n) = \gamma_n m_n\mathbf v_n$ , $\mathbf p_n\cdot\mathbf p_k$ is the Euclidean inner product, and $\mathrm{invariantMass}(c,P) = \sqrt{P^0P^0-\mathbf P\cdot\mathbf P}/c$ with the real square root ( $0$ on negative input). For $N=0$ both sides are $0$ .

View graph