Norm of the four-momentum: $\langle \mathbf P,\mathbf P\rangle = (E/c)^2 - p^2 = (mc)^2$

Proved

EnergyMomentum.minkowski_norm_fourMomentum

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

mathematical-physicsspecial-relativity

Let $c>0$ , $m>0$ and $\mathbf v\in\mathbb R^3$ with $|\mathbf v|<c$ , and let $\mathbf P = (E/c, \mathbf p)$ be the four-momentum of the body, $E = \gamma mc^2$ , $\mathbf p = \gamma m\mathbf v$ . With the Minkowski inner product of signature $(+,-,-,-)$ ,

\langle \mathbf P, \mathbf P\rangle = \left(\frac{E}{c}\right)^2 - p^2 = (mc)^2 .

The Minkowski square of the four-momentum is thus fixed by the mass alone; rearranging gives (1).

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Norm of the four-momentum: `⟨P, P⟩ = (E / c)² − p² = (m c)²`. -/
theorem minkowski_norm_fourMomentum (m c : ℝ) (v : Vec3)
    (hc : 0 < c) (hm : 0 < m) (hv : ‖v‖ < c) :
    minkowskiInner (fourMomentum m c v) (fourMomentum m c v)
        = (energy m c v / c) ^ 2 - ‖momentum m c v‖ ^ 2 ∧
      minkowskiInner (fourMomentum m c v) (fourMomentum m c v) = (m * 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), §Norm of the four-momentum → Special relativity (displays computing

\langle \mathbf P,\mathbf P\rangle

with the Minkowski metric

\eta

, and

(mc)^2 = (E/c)^2 - p^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 all real $m, c$ and $\mathbf v\in\mathbb R^3$ with $0<c$ , $0<m$ , $|\mathbf v|<c$ , both of the following hold, where $\mathbf P = \mathrm{fourMomentum}(m,c,\mathbf v) = (\mathrm{energy}(m,c,\mathbf v)/c,\ \mathrm{momentum}(m,c,\mathbf v))$ and $\langle P, Q\rangle = P^0Q^0 - \mathbf P\cdot\mathbf Q$ :

$\langle \mathbf P,\mathbf P\rangle = \left(\dfrac{\mathrm{energy}(m,c,\mathbf v)}{c}\right)^2 - |\mathrm{momentum}(m,c,\mathbf v)|^2$ ;
$\langle \mathbf P,\mathbf P\rangle = (m c)^2$ .

Here $\mathrm{energy} = \gamma mc^2$ , $\mathrm{momentum} = \gamma m\mathbf v$ , $\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}$ . (Clause 1 holds by unfolding the definitions; clause 2 is the substantive part.)

View graph

Norm of the four-momentum: ⟨P,P⟩=(E/c)2−p2=(mc)2\langle \mathbf P,\mathbf P\rangle = (E/c)^2 - p^2 = (mc)^2⟨P,P⟩=(E/c)2−p2=(mc)2

Norm of the four-momentum: $\langle \mathbf P,\mathbf P\rangle = (E/c)^2 - p^2 = (mc)^2$