Israel (1968): static electrovacuum black holes are Reissner–Nordström

Open

NoHair.israel_static_electrovac

by Lucas · Oct 4, 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. Assume moreover that the stationary Killing field is hypersurface-orthogonal on $\langle\langle M_{\rm ext}\rangle\rangle$ (static). Then there are $m>0$ and $e$ with $e^2\le m^2$ such that $\langle\langle M_{\rm ext}\rangle\rangle$ is isometric to the Reissner–Nordström exterior with mass $m$ and charge $e$ (the Kerr–Newman domain of outer communications with $a=0$ ), the field matching up to a constant duality rotation.

This is the charged generalization of Israel's theorem.

Preamble

import Mathlib
import Definitions.Def_NoHair_kerrNewman

open scoped ContDiff Manifold BigOperators
open Set Matrix

Formal statement

namespace NoHair

/-- **Milestone (Israel 1968): static electrovacuum black holes are Reissner–Nordström.** -/
theorem israel_static_electrovac {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)
    (hstatic : IsStaticOn g φ (domainOfOuterCommunications g T E.region)) :
    ∃ m e : ℝ, IsKerrNewmanBlackHoleParams m 0 e ∧
      IsKerrNewmanDOC g F (domainOfOuterCommunications g T E.region) m 0 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.

Additional hypothesis. The stationary flow is static on $D$ (same coordinate condition $k\wedge dk=0$ as in the static vacuum milestone). $F$ is not assumed to vanish.

Conclusion. There exist $m,e$ with $0<m$ and $0^2+e^2\le m^2$ such that $D$ is isometric to the Kerr–Newman DOC with parameters $(m,0,e)$ (Reissner–Nordström exterior), with the field equal to $\cos\beta F^{KN}+\sin\beta\star F^{KN}$ for some $\beta$ .

"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}$ .

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