Kerr–Newman metric solves the Einstein–Maxwell equations

Proved

NoHair.kerrNewman_einsteinMaxwell

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

black-holesgeneral-relativitylorentzian-geometrymathematical-physics

For all real $m,a,e$ and every point $y$ of Kerr–Schild coordinate space with $r(y)>0$ , the Kerr–Newman metric $g^{KN}_{m,a,e}=\eta+f\,k\otimes k$ and field $F^{KN}_{a,e}=dA$ satisfy at $y$

G_{\mu\nu}=2\Big(F_{\mu\alpha}F_\nu{}^\alpha-\tfrac14g_{\mu\nu}F_{\alpha\beta}F^{\alpha\beta}\Big),\qquad\partial_\mu\big(\sqrt{|\det g|}F^{\mu\nu}\big)=0,\qquad\partial_{[\lambda}F_{\mu\nu]}=0.

This confirms that the model family named in the no-hair theorem consists of solutions of the theory, in the conventions used throughout the mission.

Preamble

import Mathlib
import Definitions.Def_NoHair_kerrNewman

open scoped ContDiff Manifold BigOperators
open Set Matrix

Formal statement

namespace NoHair

/-- **Milestone: Kerr–Newman solves Einstein–Maxwell.** In Kerr–Schild coordinates the
Kerr–Newman metric and field satisfy the Einstein–Maxwell equations wherever `r > 0`. -/
theorem kerrNewman_einsteinMaxwell (m a e : ℝ) (y : E4) (hy : 0 < ksRadius a y) :
    EinsteinMaxwellAt (kerrNewmanMetric m a e) (kerrNewmanField a e) y := 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 all real numbers $m,a,e$ and every point $y\in\mathbb R^4$ with $r(y)>0$ ( $r$ the Kerr–Schild radial function with parameter $a$ ), the coordinate Einstein–Maxwell predicate holds at $y$ for the matrix functions $G=g^{KN}_{m,a,e}$ (i.e. $\eta+f k k^{\mathsf T}$ ) and $F=F^{KN}_{a,e}$ (i.e. $\partial_\mu A_\nu-\partial_\nu A_\mu$ with $A=\frac{er^3}{r^4+a^2z^2}k$ ). Concretely, at $y$ : (i) $G_{\mu\nu}=2\big(\sum F_{\mu\alpha}g^{\alpha\beta}F_{\nu\beta}-\frac14g_{\mu\nu}\sum F_{\alpha\beta}F^{\alpha\beta}\big)$ for all $\mu,\nu$ , with curvature computed from the classical Christoffel formulas using Fréchet derivatives; (ii) $\sum_\mu\partial_\mu(\sqrt{|\det g|}F^{\mu\nu})=0$ for each $\nu$ ; (iii) $\partial_\lambda F_{\mu\nu}+\partial_\mu F_{\nu\lambda}+\partial_\nu F_{\lambda\mu}=0$ . No sign or size condition is imposed on $m,a,e$ (negative mass, super-extremal and $a=0$ cases are all included); the only restriction is $r(y)>0$ .

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