No-hair conjecture: stationary electrovacuum black holes are Kerr–Newman

Open

NoHair.no_hair_conjecture

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

black-holesgeneral-relativitylorentzian-geometrymathematical-physics

Let $(M,g,F,T)$ be a 4-dimensional spacetime: a smooth manifold $M$ , a smooth Lorentzian metric $g$ of signature $(-,+,+,+)$ , a smooth electromagnetic 2-form $F$ and a time orientation $T$ . Assume $(g,F)$ solves the Einstein–Maxwell equations with zero cosmological constant, is stationary under a smooth one-parameter group $\varphi_t$ of isometries preserving $F$ , and has a stationary asymptotically flat end $M_{\rm ext}$ on which $\varphi_t$ acts by time translation. Assume the domain of outer communications $\langle\langle M_{\rm ext}\rangle\rangle=I^+(M_{\rm ext})\cap I^-(M_{\rm ext})$ is globally hyperbolic, the black-hole region $M\setminus I^-(M_{\rm ext})$ is nonempty, and the future event horizon $\partial I^-(M_{\rm ext})$ is connected.

Then there are parameters $m>0$ , $a$ , $e$ with $a^2+e^2\le m^2$ such that $\langle\langle M_{\rm ext}\rangle\rangle$ is isometric to the domain of outer communications $\{r>r_+\}$ of the Kerr–Newman spacetime with mass $m$ , angular-momentum parameter $a$ and charge $e$ :

\exists\,\Psi:\{r>r_+\}\xrightarrow{\ \cong\ }\langle\langle M_{\rm ext}\rangle\rangle,\qquad \Psi^*g=g^{KN}_{m,a,e},\qquad \Psi^*F=\cos\beta\,F^{KN}_{a,e}+\sin\beta\,\star F^{KN}_{a,e}

for some constant duality angle $\beta$ .

This is the precise form of the statement that a stationary black hole of the Einstein–Maxwell theory is characterized by its mass, angular momentum and electric charge. The source states it is unproved in general and is called the no-hair conjecture by mathematicians.

Formalization Note The duality angle $\beta$ allows a magnetic charge, which the source mentions as a possible fourth parameter: the metric depends only on $q^2+p^2=e^2$ . Connectedness of the horizon excludes the static multi-black-hole Majumdar–Papapetrou solutions; global hyperbolicity of the domain of outer communications is the standard regularity assumption.

Preamble

import Mathlib
import Definitions.Def_NoHair_kerrNewman

open scoped ContDiff Manifold BigOperators
open Set Matrix

Formal statement

namespace NoHair

/-- **Goal (no-hair conjecture, Einstein–Maxwell, Λ = 0).** The domain of outer communications
of every stationary, asymptotically flat electrovacuum black-hole spacetime with globally
hyperbolic domain of outer communications and connected event horizon is isometric to a
Kerr–Newman domain of outer communications (field up to duality rotation). -/
theorem no_hair_conjecture {M : Type*} [TopologicalSpace M] [ChartedSpace E4 M]
    [IsManifold 𝓘(ℝ, E4) ∞ M] (g F : BilinField M) (T : VecField M) (φ : ℝ → M → M)
    (E : AsymptoticallyFlatEnd g F φ) (h : IsStationaryBlackHole g F T φ E) :
    ∃ m a e : ℝ, IsKerrNewmanBlackHoleParams m a e ∧
      IsKerrNewmanDOC g F (domainOfOuterCommunications g T E.region) 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.

$M$ is any type with a topology and a charted-space structure on $\mathbb R^4$ that is a $C^\infty$ manifold (no Hausdorff/second-countable/connected assumption). $g,F$ are arbitrary bilinear fields, $T$ a vector field, $\varphi:\mathbb R\to M\to M$ any map, $E$ an asymptotically flat end for $(g,F,\varphi)$ (data $R>0$ , $\psi$ , $C$ with: $\psi$ a diffeomorphism from $\Omega_R=\{|\vec y|>R\}$ onto the open set $\psi(\Omega_R)$ , $\psi(y+se_0)=\varphi_s(\psi y)$ , $|g_{\mu\nu}-\eta_{\mu\nu}|\le C/|\vec y|$ , $|\partial_\sigma g_{\mu\nu}|\le C/|\vec y|^2$ , $|F_{\mu\nu}|\le C/|\vec y|^2$ in $\psi$ -coordinates). Hypothesis $h$ says: $g$ is Lorentzian (orthonormal basis of signature $(-,+,+,+)$ at each point); $g$ and $F$ have $C^\infty$ components in every chart; $F$ is antisymmetric; $T$ is continuous and $g(T,T)<0$ ; the coordinate Einstein–Maxwell equations ( $G_{\mu\nu}=2(F_{\mu\alpha}F_\nu{}^\alpha-\frac14g_{\mu\nu}F^2)$ , $\partial_\mu(\sqrt{|\det g|}F^{\mu\nu})=0$ , $dF=0$ ) hold at every point of every chart; $\varphi$ is a jointly smooth $\mathbb R$ -action preserving $g$ and $F$ ; the set $D=I^+(\psi(\Omega_R))\cap I^-(\psi(\Omega_R))$ (chronological sets via $C^1$ future-timelike curves, $g(\gamma',\gamma')<0$ , $g(\gamma',T)<0$ , on $[0,1]$ ) is globally hyperbolic (no closed future causal $C^1$ curve in $D$ , and $J^+_D(p)\cap J^-_D(q)$ compact for $p,q\in D$ ); the complement of $I^-(\psi(\Omega_R))$ is nonempty; the frontier of $I^-(\psi(\Omega_R))$ is connected and nonempty.

Conclusion. There exist reals $m,a,e$ with $0<m$ and $a^2+e^2\le m^2$ such that $D$ is isometric to the Kerr–Newman DOC with parameters $(m,a,e)$ .

"Isometric to the Kerr–Newman DOC with parameters $(m,a,e)$ " means: there exist a real $\beta$ and a map $\Psi:\mathbb R^4\to M$ with a two-sided inverse $\chi$ between $\{y:r(y)>r_+\}$ and $D$ , both $C^\infty$ on these sets, such that for all $y$ with $r(y)>r_+$ the pulled-back metric matrix $(\Psi^*g)(y)$ equals $\eta+f k k^{\mathsf T}$ (Kerr–Newman in Kerr–Schild form, with $r$ , $k$ , $f$ as in the coordinate definitions) and $(\Psi^*F)(y)=\cos\beta\,F^{KN}(y)+\sin\beta\,\star F^{KN}(y)$ ; here $r_+=m+\sqrt{m^2-a^2-e^2}$ .

Edge cases: $\beta$ is unconstrained, so the field is determined only up to a constant duality rotation; the extremal case $a^2+e^2=m^2$ is allowed; nothing is asserted about $M$ outside $D$ .

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