Changing the reference frame I: boosting to the rest frame

Proved

NoHair.rest_frame_exists

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

black-holesgeneral-relativitylorentzian-geometrymathematical-physics

Let $P\in\mathbb R^4$ be a future-directed timelike 4-momentum: $\eta(P,P)=P^{\mathsf T}\eta P<0$ and $P^0>0$ , with $\eta=\mathrm{diag}(-1,1,1,1)$ . Then there is a proper orthochronous Lorentz transformation $\Lambda$ ( $\Lambda^{\mathsf T}\eta\Lambda=\eta$ , $\det\Lambda=1$ , $\Lambda^0{}_0\ge1$ ) with

\Lambda P=\big(\sqrt{-\eta(P,P)},0,0,0\big).

This is the step of the source's frame argument that sets the linear momentum to zero.

Preamble

import Mathlib
import Definitions.Def_NoHair_kerrNewman

open scoped ContDiff Manifold BigOperators
open Set Matrix

Formal statement

namespace NoHair

/-- **Milestone (changing the reference frame I): rest frame.** Every future-directed timelike
4-momentum `P` is carried by a proper orthochronous Lorentz transformation to
`(√(-η(P,P)), 0, 0, 0)`. -/
theorem rest_frame_exists (P : Fin 4 → ℝ) (hP : P ⬝ᵥ (minkowski *ᵥ P) < 0) (hP0 : 0 < P 0) :
    ∃ Λ : Matrix (Fin 4) (Fin 4) ℝ, Λᵀ * minkowski * Λ = minkowski ∧ Λ.det = 1 ∧
      1 ≤ Λ 0 0 ∧ Λ *ᵥ P = ![Real.sqrt (-(P ⬝ᵥ (minkowski *ᵥ P))), 0, 0, 0] := by
  sorry

end NoHair

Source

Wikipedia, "No-hair theorem" (revision oldid=1353599195), https://en.wikipedia.org/w/index.php?title=No-hair_theorem&oldid=1353599195

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as the drafter; non-blind

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), with full knowledge of the source and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; reviewers should compare it against the Lean code themselves or obtain an independent read-back.

Let $P:\{0,1,2,3\}\to\mathbb R$ satisfy $P\cdot(\eta P)<0$ (i.e. $-P_0^2+P_1^2+P_2^2+P_3^2<0$ ) and $P_0>0$ , where $\eta=\mathrm{diag}(-1,1,1,1)$ . Then there is a real $4\times4$ matrix $\Lambda$ with $\Lambda^{\mathsf T}\eta\Lambda=\eta$ , $\det\Lambda=1$ , $1\le\Lambda_{00}$ , and $\Lambda P=\big(\sqrt{-P\cdot\eta P},0,0,0\big)$ (matrix–vector product).

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph