Lorentz factor in terms of momentum: $\gamma = \sqrt{1 + (p/mc)^2}$

Proved

EnergyMomentum.lorentzFactor_eq_sqrt_momentum

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

mathematical-physicsspecial-relativity

Let $c > 0$ , $m > 0$ and let $\mathbf v \in \mathbb R^3$ with $|\mathbf v| < c$ . With $\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}$ and relativistic momentum $\mathbf p = \gamma m\mathbf v$ , $p = |\mathbf p|$ ,

\gamma = \sqrt{1 + \left(\frac{p}{mc}\right)^2}.

This alternative form expresses the Lorentz factor through momentum and mass instead of velocity.

Preamble

import Mathlib
import Definitions.Def_EnergyMomentum_basic

Formal statement

namespace EnergyMomentum

/-- Lorentz factor in terms of three-momentum: `γ = √(1 + (p / (m c))²)`. -/
theorem lorentzFactor_eq_sqrt_momentum (m c : ℝ) (v : Vec3)
    (hc : 0 < c) (hm : 0 < m) (hv : ‖v‖ < c) :
    lorentzFactor c v = Real.sqrt (1 + (‖momentum 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), §Origins and derivation of the equation → Heuristic approach for massive particles (alternative form of the Lorentz factor).

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 numbers $m, c$ and every $\mathbf v \in \mathbb R^3$ , assuming $0 < c$ , $0 < m$ and $|\mathbf v| < c$ :

\frac{1}{\sqrt{1 - (|\mathbf v|/c)^2}} \;=\; \sqrt{1 + \left(\frac{|\mathrm{momentum}(m,c,\mathbf v)|}{m\,c}\right)^2},

where $\mathrm{momentum}(m,c,\mathbf v) = \gamma m\,\mathbf v$ with $\gamma$ the left-hand side. Under the hypotheses all square-root arguments are positive and $m c \ne 0$ , so no junk values occur.

View graph

Lorentz factor in terms of momentum: γ=1+(p/mc)2\gamma = \sqrt{1 + (p/mc)^2}γ=1+(p/mc)2​

Lorentz factor in terms of momentum: $\gamma = \sqrt{1 + (p/mc)^2}$