Lorentz invariance of the Minkowski square under a boost

Proved

EnergyMomentum.minkowskiInner_boostX

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

mathematical-physicsspecial-relativity

Let $c>0$ and let $u$ be a real velocity with $|u|<c$ . For every four-vector $P = (P^0, P^x, P^y, P^z)$ , let $\Lambda_u P = (\gamma_u(P^0 - \beta P^x),\ \gamma_u(P^x - \beta P^0),\ P^y,\ P^z)$ be its Lorentz boost along the $x$ -axis, $\beta = u/c$ , $\gamma_u = 1/\sqrt{1-\beta^2}$ . Then

\langle \Lambda_u P, \Lambda_u P\rangle = \langle P, P\rangle ,

where $\langle\cdot,\cdot\rangle$ is the Minkowski inner product of signature $(+,-,-,-)$ . Hence $\langle\mathbf P,\mathbf P\rangle$ — and so the mass — is independent of the inertial frame.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Lorentz invariance of `⟨P, P⟩` under a boost along the `x`-axis with speed `|u| < c`. -/
theorem minkowskiInner_boostX (c u : ℝ) (P : FourVec)
    (hc : 0 < c) (hu : |u| < c) :
    minkowskiInner (boostX c u P) (boostX c u P) = minkowskiInner P P := 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: "This is a Lorentz invariant quantity, and therefore independent of the frame of reference" (boost along one axis as the representative Lorentz transformation; see also the figure caption on hyperbolic rotations).

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 $c, u$ and every $P = (P^0,\mathbf P) \in \mathbb R\times\mathbb R^3$ , assuming $0<c$ and $|u|<c$ :

\langle \mathrm{boostX}(c,u,P), \mathrm{boostX}(c,u,P)\rangle = \langle P, P\rangle ,

where $\langle Q, R\rangle = Q^0R^0 - \mathbf Q\cdot\mathbf R$ and $\mathrm{boostX}(c,u,P)$ is the four-vector with time component $g(P^0 - (u/c)P_0)$ and spatial coordinates $\big(g(P_0 - (u/c)P^0),\ P_1,\ P_2\big)$ , with $g = 1/\sqrt{1-(u/c)^2}$ and $P_0,P_1,P_2$ the coordinates of $\mathbf P$ . Under the hypotheses $1-(u/c)^2 \in (0,1]$ , so $g$ is finite and positive (no junk). No condition is placed on $P$ .

View graph