Many-particle energy–momentum relation (2)

Proved

EnergyMomentum.system_energy_momentum_relation

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$ , particle $n$ having mass $m_n>0$ and velocity $\mathbf v_n$ with $|\mathbf v_n|<c$ , energy $E_n = \gamma_n m_n c^2$ , momentum $\mathbf p_n = \gamma_n m_n\mathbf v_n$ and four-momentum $\mathbf P_n = (E_n/c, \mathbf p_n)$ . Let $M$ be the invariant mass of the total four-momentum, $M = \sqrt{\langle \sum_n\mathbf P_n, \sum_n\mathbf P_n\rangle}/c$ . Then

\left(\sum_{n\in S} E_n\right)^2 = \left(\Big|\sum_{n\in S}\mathbf p_n\Big|\, c\right)^2 + \left(Mc^2\right)^2 .

The energies and momenta are frame-dependent while $M$ is not; $M$ is in general different from $\sum_n m_n$ .

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Many-particle energy–momentum relation (2):
`(∑ Eₙ)² = (|∑ 𝐩ₙ| c)² + (M c²)²`, where `M` is the invariant mass of the total four-momentum. -/
theorem system_energy_momentum_relation {ι : Type} (s : Finset ι) (m : ι → ℝ) (v : ι → Vec3)
    (c : ℝ) (hc : 0 < c) (hm : ∀ n ∈ s, 0 < m n) (hv : ∀ n ∈ s, ‖v n‖ < c) :
    (∑ n ∈ s, energy (m n) c (v n)) ^ 2
      = (‖∑ n ∈ s, momentum (m n) c (v n)‖ * c) ^ 2
        + (invariantMass c (∑ n ∈ s, fourMomentum (m n) c (v n)) * c ^ 2) ^ 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 → Addition of four-momenta, equation (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; reviewers should check it against the Lean code themselves (or replace it with a blind read-back).

For every type $\iota$ , every finite set $S\subseteq\iota$ , all functions $m:\iota\to\mathbb R$ and $\mathbf v:\iota\to\mathbb R^3$ , and every real $c$ , assuming

$0<c$ ,
$0<m_n$ for every $n\in S$ ,
$|\mathbf v_n|<c$ for every $n\in S$ ,

we have

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

where $\mathrm{energy} = \gamma_n m_n c^2$ , $\mathrm{momentum} = \gamma_n m_n\mathbf v_n$ , $\mathrm{fourMomentum} = (\mathrm{energy}/c, \mathrm{momentum})$ (sums of four-vectors are componentwise), and $\mathrm{invariantMass}(c,P) = \sqrt{P^0P^0 - \mathbf P\cdot\mathbf P}\,/\,c$ with the real square root (which returns $0$ on negative arguments). Nothing is assumed about the values of $m,\mathbf v$ outside $S$ . If $S$ is empty both sides are $0$ . Note that the statement is only true if the Minkowski square of the total four-momentum is $\ge 0$ ; this is not assumed but must be proved.

View graph