Prove2Me

Relativistic kinetic energy EK=(pc)2+(mc2)2−mc2E_K = \sqrt{(pc)^2 + (mc^2)^2} - mc^2

Proved
EnergyMomentum.kineticEnergy_eq

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

mathematical-physicsspecial-relativity

Let c>0c>0, m>0m>0 and v∈R3\mathbf v\in\mathbb R^3 with ∣v∣<c|\mathbf v|<c. The relativistic kinetic energy EK=E−E0E_K = E - E_0, the difference between the total energy E=γmc2E = \gamma mc^2 and the rest energy E0=mc2E_0 = mc^2, satisfies

EK=(pc)2+(mc2)2−mc2,E_K = \sqrt{(pc)^2 + (mc^2)^2} - mc^2 ,

where p=∣γmv∣p = |\gamma m\mathbf v|.

Preamble
import Mathlib
import Definitions.Def_EnergyMomentum_basic
Formal statement
namespace EnergyMomentum

/-- Relativistic kinetic energy: `E_K = E − E₀ = √((p c)² + (m c²)²) − m c²`. -/
theorem kineticEnergy_eq (m c : ℝ) (v : Vec3)
    (hc : 0 < c) (hm : 0 < m) (hv : ‖v‖ < c) :
    kineticEnergy m c v
      = Real.sqrt ((‖momentum m c v‖ * c) ^ 2 + (m * c ^ 2) ^ 2) - 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), lead section (display following equation (1)).
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,cm, c and v∈R3\mathbf v\in\mathbb R^3 with 0<c0<c, 0<m0<m, ∣v∣<c|\mathbf v|<c:

kineticEnergy(m,c,v)=(∣momentum(m,c,v)∣ c)2+(mc2)2−mc2,\mathrm{kineticEnergy}(m,c,\mathbf v) = \sqrt{\big(|\mathrm{momentum}(m,c,\mathbf v)|\, c\big)^2 + (m c^2)^2} - m c^2 ,

where kineticEnergy(m,c,v)=γmc2−mc2\mathrm{kineticEnergy}(m,c,\mathbf v) = \gamma m c^2 - m c^2, momentum(m,c,v)=γmv\mathrm{momentum}(m,c,\mathbf v) = \gamma m\mathbf v and γ=1/1−(∣v∣/c)2\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}. The square-root argument on the right is positive, so the square root is the genuine one.

View graph