Kerr–Newman spacetime satisfies the standing hypotheses

Open

NoHair.kerrNewman_isStationaryBlackHole

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

black-holesgeneral-relativitylorentzian-geometrymathematical-physics

Let $m>0$ and $a^2+e^2\le m^2$ . On the Kerr–Newman spacetime $\{r>0\}\subseteq\mathbb R^4$ with metric $g^{KN}_{m,a,e}$ and field $F^{KN}_{a,e}$ there exist a time orientation $T$ , a symmetry flow $\varphi$ and a stationary asymptotically flat end $E$ such that all standing hypotheses of the mission hold (Lorentzian smooth metric, smooth 2-form, Einstein–Maxwell, stationarity, globally hyperbolic domain of outer communications, nonempty black-hole region, connected future event horizon), and the domain of outer communications is exactly $\{r>r_+\}$ , $r_+=m+\sqrt{m^2-a^2-e^2}$ .

This shows the hypotheses of the goal theorem are satisfiable and that the Kerr–Newman black holes themselves fall under the goal, so the goal is neither vacuous nor contradicted by its own model family.

Preamble

import Mathlib
import Definitions.Def_NoHair_kerrNewman

open scoped ContDiff Manifold BigOperators
open Set Matrix

Formal statement

namespace NoHair

/-- **Milestone: Kerr–Newman is a stationary black hole.** For admissible parameters, the
Kerr–Newman spacetime `{r > 0}` satisfies all the standing hypotheses, and its domain of outer
communications is `{r > r₊}`. -/
theorem kerrNewman_isStationaryBlackHole (m a e : ℝ) (hp : IsKerrNewmanBlackHoleParams m a e) :
    ∃ (T : VecField (kerrNewmanSpacetime a))
      (φ : ℝ → kerrNewmanSpacetime a → kerrNewmanSpacetime a)
      (E : AsymptoticallyFlatEnd (kerrNewmanMetricField m a e) (kerrNewmanFieldField a e) φ),
      IsStationaryBlackHole (kerrNewmanMetricField m a e) (kerrNewmanFieldField a e) T φ E ∧
      Subtype.val '' domainOfOuterCommunications (kerrNewmanMetricField m a e) T E.region
        = kerrNewmanDOC m a e := 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.

For real $m,a,e$ with $0<m$ and $a^2+e^2\le m^2$ : there exist a vector field $T$ on the Kerr–Newman spacetime $M_a=\{y:r(y)>0\}\subseteq\mathbb R^4$ , a map $\varphi:\mathbb R\to M_a\to M_a$ , and an asymptotically flat end $E$ for (Kerr–Newman metric field, Kerr–Newman field, $\varphi$ ), such that (1) the full stationary-black-hole predicate holds for $(g^{KN},F^{KN},T,\varphi,E)$ — Lorentzian, smooth metric and field, antisymmetric field, $T$ a time orientation, Einstein–Maxwell in every chart, $\varphi$ a symmetry flow, the DOC $I^+(\text{end})\cap I^-(\text{end})$ globally hyperbolic, black-hole region nonempty, event horizon connected — and (2) the image in $\mathbb R^4$ (under the inclusion $M_a\hookrightarrow\mathbb R^4$ ) of that DOC is exactly $\{y: r_+<r(y)\}$ with $r_+=m+\sqrt{m^2-a^2-e^2}$ . $T$ , $\varphi$ and $E$ are existentially quantified, not specified.

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