Special-relativistic kinematics: Lorentz factor, energy, momentum, four-momentum, Minkowski form, invariant mass, boosts

Definition

EnergyMomentum_basic

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

mathematical-physicsspecial-relativity

Basic objects of special-relativistic kinematics in flat spacetime, with an explicit speed of light $c$ .

Spatial vectors live in $\mathbb R^3$ with Euclidean norm $|\cdot|$ and dot product; four-vectors are pairs $P = (P^0, \mathbf P) \in \mathbb R \times \mathbb R^3$ of contravariant components. For a body of mass $m$ moving with velocity $\mathbf v$ :

Lorentz factor $\gamma(\mathbf v) = \dfrac{1}{\sqrt{1 - (|\mathbf v|/c)^2}}$ ;
total energy $E = \gamma m c^2$ ;
relativistic momentum $\mathbf p = \gamma m\,\mathbf v$ ;
rest energy $E_0 = mc^2$ and kinetic energy $E_K = E - E_0$ ;
four-momentum $\mathbf P = (E/c, \mathbf p)$ .

On four-vectors:

the Minkowski inner product of signature $(+,-,-,-)$ , $\langle P, Q\rangle = P^0 Q^0 - \mathbf P \cdot \mathbf Q$ ;
the invariant mass of a four-momentum $P$ , $M = \sqrt{\langle P, P\rangle}/c$ , so that $\langle P,P\rangle = (Mc)^2$ when $\langle P,P\rangle\ge 0$ , $c>0$ ;
the Lorentz boost along the $x$ -axis with velocity $u$ : $(P^0, P^x, P^y, P^z) \mapsto (\gamma_u(P^0 - \beta P^x),\ \gamma_u(P^x - \beta P^0),\ P^y,\ P^z)$ , where $\beta = u/c$ , $\gamma_u = 1/\sqrt{1-\beta^2}$ .

These definitions are the shared model for every statement of the mission.

Formalization Note Spatial vectors are EuclideanSpace ℝ (Fin 3) with coordinates 0, 1, 2 for $x, y, z$ . Division and square root are total in Lean: for $|\mathbf v| \ge c$ (or $|u|\ge c$ ) the Lorentz factor evaluates to $0$ , and for $c = 0$ divisions by $c$ evaluate to $0$ ; theorems therefore assume $c>0$ and $|\mathbf v|<c$ explicitly.

Definition code

import Mathlib

/-!
# Energy–momentum relation: basic special-relativistic quantities

Spatial vectors (velocities, three-momenta) live in `EuclideanSpace ℝ (Fin 3)`;
coordinates `0, 1, 2` are the `x, y, z` components.
Four-vectors are pairs `(P⁰, 𝐏) : ℝ × EuclideanSpace ℝ (Fin 3)` of contravariant components.
-/

namespace EnergyMomentum

/-- Three-dimensional Euclidean space of spatial vectors. -/
abbrev Vec3 := EuclideanSpace ℝ (Fin 3)

/-- Four-vectors `(P⁰, 𝐏)` (contravariant components). -/
abbrev FourVec := ℝ × Vec3

/-- The Lorentz factor `γ = 1 / √(1 - (|v|/c)²)` of a body moving with velocity `v`
when the speed of light is `c`. (Only meaningful for `|v| < c`.) -/
noncomputable def lorentzFactor (c : ℝ) (v : Vec3) : ℝ :=
  1 / Real.sqrt (1 - (‖v‖ / c) ^ 2)

/-- Total (relativistic) energy `E = γ m c²` of a body of mass `m` moving with velocity `v`. -/
noncomputable def energy (m c : ℝ) (v : Vec3) : ℝ :=
  lorentzFactor c v * m * c ^ 2

/-- Relativistic three-momentum `𝐩 = γ m 𝐯` of a body of mass `m` moving with velocity `v`. -/
noncomputable def momentum (m c : ℝ) (v : Vec3) : Vec3 :=
  (lorentzFactor c v * m) • v

/-- Rest energy `E₀ = m c²`. -/
def restEnergy (m c : ℝ) : ℝ :=
  m * c ^ 2

/-- Relativistic kinetic energy `E_K = E - E₀`. -/
noncomputable def kineticEnergy (m c : ℝ) (v : Vec3) : ℝ :=
  energy m c v - restEnergy m c

/-- Minkowski inner product with metric signature `(+ − − −)`:
`⟨P, Q⟩ = P⁰ Q⁰ − 𝐏 · 𝐐`. -/
noncomputable def minkowskiInner (P Q : FourVec) : ℝ :=
  P.1 * Q.1 - inner ℝ P.2 Q.2

/-- Four-momentum `𝐏 = (E / c, 𝐩)` of a body of mass `m` moving with velocity `v`. -/
noncomputable def fourMomentum (m c : ℝ) (v : Vec3) : FourVec :=
  (energy m c v / c, momentum m c v)

/-- Invariant mass `M` associated with a (total) four-momentum `P`, defined through
`⟨P, P⟩ = (M c)²`, i.e. `M = √⟨P, P⟩ / c`. -/
noncomputable def invariantMass (c : ℝ) (P : FourVec) : ℝ :=
  Real.sqrt (minkowskiInner P P) / c

/-- Lorentz boost along the `x`-axis with velocity `u` (speed of light `c`), acting on
contravariant four-vector components:
`P'⁰ = γ (P⁰ − β Pˣ)`, `P'ˣ = γ (Pˣ − β P⁰)`, `P'ʸ = Pʸ`, `P'ᶻ = Pᶻ`,
where `β = u / c` and `γ = 1 / √(1 − β²)`. -/
noncomputable def boostX (c u : ℝ) (P : FourVec) : FourVec :=
  (1 / Real.sqrt (1 - (u / c) ^ 2) * (P.1 - u / c * P.2 0),
    !₂[1 / Real.sqrt (1 - (u / c) ^ 2) * (P.2 0 - u / c * P.1), P.2 1, P.2 2])

end EnergyMomentum

Source

Wikipedia, *Energy–momentum relation*, https://en.wikipedia.org/wiki/Energy%E2%80%93momentum_relation (PDF snapshot supplied by the proposer): lead section (eq. (1),

E_0 = mc^2

E_K

); §Heuristic approach for massive particles (

E=\gamma mc^2

p=\gamma mv

\gamma

); §Norm of the four-momentum / Special relativity (four-momentum, Minkowski metric with signature

(+,-,-,-)

, Lorentz invariance); §Many-particle systems (total mass

M

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).

The file defines, inside the namespace EnergyMomentum, the following objects. $\mathrm{Vec3}$ is the Euclidean space $\mathbb R^3$ (coordinates indexed $0,1,2$ ) with its Euclidean norm $|\cdot|$ and inner product, and $\mathrm{FourVec} = \mathbb R \times \mathbb R^3$ , whose elements are written $(P^0, \mathbf P)$ . For arbitrary real numbers $c, m, u$ (no sign conditions are imposed anywhere in the file) and $\mathbf v \in \mathbb R^3$ :

$\mathrm{lorentzFactor}(c,\mathbf v) = 1 / \sqrt{1 - (|\mathbf v|/c)^2}$ , where $\sqrt{\cdot}$ is the real square root which returns $0$ on negative inputs, $x/0 = 0$ and $1/0 = 0$ . In particular it equals $0$ whenever $|\mathbf v| \ge c > 0$ , and equals $1$ when $c = 0$ (since $|\mathbf v|/0 = 0$ ).
$\mathrm{energy}(m,c,\mathbf v) = \mathrm{lorentzFactor}(c,\mathbf v)\cdot m \cdot c^2$ .
$\mathrm{momentum}(m,c,\mathbf v) = (\mathrm{lorentzFactor}(c,\mathbf v)\cdot m)\,\mathbf v \in \mathbb R^3$ .
$\mathrm{restEnergy}(m,c) = m c^2$ .
$\mathrm{kineticEnergy}(m,c,\mathbf v) = \mathrm{energy}(m,c,\mathbf v) - \mathrm{restEnergy}(m,c)$ .
$\mathrm{minkowskiInner}(P,Q) = P^0 Q^0 - \mathbf P\cdot\mathbf Q$ (Euclidean dot product of the spatial parts).
$\mathrm{fourMomentum}(m,c,\mathbf v) = \big(\mathrm{energy}(m,c,\mathbf v)/c,\ \mathrm{momentum}(m,c,\mathbf v)\big)$ (first component is $0$ if $c = 0$ ).
$\mathrm{invariantMass}(c,P) = \sqrt{\mathrm{minkowskiInner}(P,P)}\,/\,c$ ; this is $0$ whenever $\mathrm{minkowskiInner}(P,P) \le 0$ or $c = 0$ .
$\mathrm{boostX}(c,u,P)$ : writing $g = 1/\sqrt{1-(u/c)^2}$ (same junk conventions; $g = 0$ when $|u| \ge |c| > 0$ ), it is the four-vector with time component $g\,(P^0 - (u/c)P_0)$ and spatial vector $\big(g\,(P_0 - (u/c)P^0),\ P_1,\ P_2\big)$ , where $P_0, P_1, P_2$ are the coordinates of $\mathbf P$ .

The file contains only definitions; it asserts no theorem.

View graph