No-hair: the Kerr–Newman spacetime as a manifold

Definition

NoHair_kerrNewman

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

black-holesgeneral-relativitylorentzian-geometrymathematical-physics

The Kerr–Newman spacetime as a manifold.

For a rotation parameter $a$ , the Kerr–Newman spacetime is the open subset $\{y\in\mathbb R^4: r(y)>0\}$ of Kerr–Schild coordinate space (the region where the Kerr–Schild radial function $r$ of the coordinate definitions is positive; the disc/ring where $r=0$ is removed), regarded as a 4-manifold. On it, the Kerr–Newman metric and field are the bilinear fields

g_y(v,w)=\sum_{\mu,\nu}g^{KN}_{\mu\nu}(y)\,v^\mu w^\nu,\qquad F_y(v,w)=\sum_{\mu,\nu}F^{KN}_{\mu\nu}(y)\,v^\mu w^\nu .

This is the concrete model used to check that the standing hypotheses of the mission are satisfiable.

Formalization Note The region is a TopologicalSpace.Opens of EuclideanSpace ℝ (Fin 4); its openness is proved from the continuity of $r$ .

Definition code

import Mathlib
import Definitions.Def_NoHair_spacetime

/-!
# No-hair mission: the Kerr–Newman spacetime as a manifold

The region `{r > 0}` of Kerr–Schild coordinate space, with the Kerr–Newman metric and field,
viewed as a spacetime (an open submanifold of `ℝ⁴`).
-/

noncomputable section

open scoped ContDiff Manifold BigOperators
open Set

namespace NoHair

/-- The continuous bilinear form `(v, w) ↦ ∑_{μν} A_{μν} v^μ w^ν` on `ℝ⁴` with matrix `A`. -/
def matrixBilin (A : Matrix (Fin 4) (Fin 4) ℝ) : E4 →L[ℝ] E4 →L[ℝ] ℝ :=
  LinearMap.toContinuousLinearMap
    ((LinearMap.toContinuousLinearMap : (E4 →ₗ[ℝ] ℝ) ≃ₗ[ℝ] (E4 →L[ℝ] ℝ)).toLinearMap ∘ₗ
      ((Matrix.toLinearMap₂' ℝ A).compl₁₂
        (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).toLinearMap
        (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).toLinearMap))

lemma continuous_ksRadius (a : ℝ) : Continuous (ksRadius a) := by
  unfold ksRadius
  fun_prop

/-- The Kerr–Newman spacetime region `{r > 0}` of Kerr–Schild coordinate space (the ring
singularity and the disc `r = 0` removed). -/
def kerrNewmanSpacetime (a : ℝ) : TopologicalSpace.Opens E4 :=
  ⟨{y | 0 < ksRadius a y}, isOpen_lt continuous_const (continuous_ksRadius a)⟩

/-- The Kerr–Newman metric as a bilinear field on `kerrNewmanSpacetime a`. -/
def kerrNewmanMetricField (m a e : ℝ) : BilinField (kerrNewmanSpacetime a) :=
  fun x => matrixBilin (kerrNewmanMetric m a e x)

/-- The Kerr–Newman electromagnetic field as a bilinear field on `kerrNewmanSpacetime a`. -/
def kerrNewmanFieldField (a e : ℝ) : BilinField (kerrNewmanSpacetime a) :=
  fun x => matrixBilin (kerrNewmanField a e x)

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 a real $a$ , the Kerr–Newman spacetime is the subset $\{y\in\mathbb R^4: 0<r(y)\}$ of coordinate space, where $r$ is the Kerr–Schild radial function with parameter $a$ from the coordinate definitions; it is shown to be open (from continuity of $r$ , proved in the file) and carries the open-subset manifold structure. For $m,e$ , the metric field at a point $y$ is the bilinear form $(v,w)\mapsto\sum_{\mu\nu}g^{KN}_{\mu\nu}(y)v^\mu w^\nu$ with $g^{KN}$ the Kerr–Newman metric matrix for $(m,a,e)$ at $y$ , and the field at $y$ is $(v,w)\mapsto\sum_{\mu\nu}F^{KN}_{\mu\nu}(y)v^\mu w^\nu$ with the Kerr–Newman field matrix for $(a,e)$ . Tangent vectors are identified with $\mathbb R^4$ via the identity chart. When $a=0$ , $r(y)=\sqrt{x^2+y^2+z^2}$ and the set is $\mathbb R^4$ minus the $t$ -axis. The definitions themselves impose no condition on $m,a,e$ .

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