Boyer-Lindquist Kerr metric, closed-form inverse and regular coordinate domain

Definition

KerrBL_Kerr_Metric

by He Wang · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

coordinate-geometrygeneral-relativitykerr-metrickerrbl-missionricci-flatness

Let $M,a\in\mathbb R$ and write $x=(t,r,\theta,\varphi)$ , $s=\sin\theta$ , $c=\cos\theta$ ,

\Sigma := r^2+a^2c^2,\qquad \Delta := r^2-2Mr+a^2 .

The bundle defines the Boyer-Lindquist Kerr metric $g$ (signature $(-,+,+,+)$ , $G=c=1$ ) as a $4\times4$ matrix of functions of $x$ :

g_{tt}=-\Big(1-\frac{2Mr}{\Sigma}\Big),\quad g_{rr}=\frac{\Sigma}{\Delta},\quad g_{\theta\theta}=\Sigma,\quad g_{\varphi\varphi}=\Big(r^2+a^2+\frac{2Mra^2s^2}{\Sigma}\Big)s^2,\quad g_{t\varphi}=g_{\varphi t}=-\frac{2Mars^2}{\Sigma},

with all other entries $0$ ; the candidate inverse $\hat g$ :

\hat g^{tt}=\frac{\Delta a^2s^2-(r^2+a^2)^2}{\Sigma\Delta},\quad \hat g^{t\varphi}=\hat g^{\varphi t}=-\frac{2Mar}{\Sigma\Delta},\quad \hat g^{rr}=\frac{\Delta}{\Sigma},\quad \hat g^{\theta\theta}=\frac{1}{\Sigma},\quad \hat g^{\varphi\varphi}=\frac{\Delta-a^2s^2}{\Sigma\Delta s^2};

and the regular domain

\mathrm{Reg}_{M,a}(x)\ :\Longleftrightarrow\ \Sigma\neq0\ \wedge\ \Delta\neq0\ \wedge\ \sin\theta\neq0 .

The parameters are arbitrary reals: the black-hole regime $M>0$ , $|a|\le M$ is not assumed, negative $r$ is allowed, and the axis $\sin\theta=0$ is excluded because the inverse carries $1/\sin^2\theta$ .

The five non-zero components are transcribed token-for-token from the parent project's canonical certificate EinsteinSolver/certificate/kerr/metric.json (sha256 d729883d...0be336); five source-lock lemmas gKerr_ij_src prove that the compact definitions equal those transcriptions. The remaining lemmas are rfl accessors for the 32 matrix entries.

Formalization Note Real division by zero is $0$ in Lean, so the components take junk values off the regular domain; every theorem of the mission assumes $\mathrm{Reg}_{M,a}(x)$ . Nothing about curvature or Ricci-flatness is part of this bundle.

Definition code

import Definitions.Def_KerrBL_CoordGeometry
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Tactic
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

/-! Layer I data for the Kerr metric (generated by mission_emit.py from
EinsteinSolver/certificate/kerr/metric.json sha256=d729883d95fd7d3cf84d9c971c6725f847155562cc4e88660535b8d0bd0be336). -/

namespace KerrBL

/-- Atom `Sig` = `a**2*c**2 + r**2` -/
noncomputable def Sig (a r c : ℝ) : ℝ := r^(2:ℕ) + a^(2:ℕ)*c^(2:ℕ)

/-- Atom `Del` = `-2*M*r + a**2 + r**2` -/
noncomputable def Del (M a r : ℝ) : ℝ := a^(2:ℕ) + r^(2:ℕ) - 2*M*r

/-- The Kerr metric components g_{ij} at a coordinate point (transcribed from metric.json). -/
noncomputable def gKerr (M a : ℝ) : Fin 4 → Fin 4 → Pt → ℝ
  | 0, 0 => fun x => (-1) + 2*M*(x 1)/Sig a (x 1) (Real.cos (x 2))
  | 0, 3 => fun x => ((-2))*M*a*(x 1)*Real.sin (x 2)^(2:ℕ)/Sig a (x 1) (Real.cos (x 2))
  | 1, 1 => fun x => Sig a (x 1) (Real.cos (x 2))/Del M a (x 1)
  | 2, 2 => fun x => Sig a (x 1) (Real.cos (x 2))
  | 3, 0 => fun x => ((-2))*M*a*(x 1)*Real.sin (x 2)^(2:ℕ)/Sig a (x 1) (Real.cos (x 2))
  | 3, 3 => fun x => Real.sin (x 2)^(2:ℕ)*(a^(2:ℕ) + (x 1)^(2:ℕ) + 2*M*(x 1)*a^(2:ℕ)*Real.sin (x 2)^(2:ℕ)/Sig a (x 1) (Real.cos (x 2)))
  | _, _ => fun _ => 0

/-- Closed-form candidate inverse g^{ij}; certified by `ginv_mul_g`. -/
noncomputable def giKerr (M a : ℝ) : Fin 4 → Fin 4 → Pt → ℝ
  | 0, 0 => fun x => (Del M a (x 1)*a^(2:ℕ)*Real.sin (x 2)^(2:ℕ) - (a^(2:ℕ) + (x 1)^(2:ℕ))^(2:ℕ))/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1)))
  | 0, 3 => fun x => ((-2))*M*a*(x 1)/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1)))
  | 1, 1 => fun x => Del M a (x 1)/Sig a (x 1) (Real.cos (x 2))
  | 2, 2 => fun x => 1/Sig a (x 1) (Real.cos (x 2))
  | 3, 0 => fun x => ((-2))*M*a*(x 1)/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1)))
  | 3, 3 => fun x => (Del M a (x 1) - a^(2:ℕ)*Real.sin (x 2)^(2:ℕ))/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1)*Real.sin (x 2)^(2:ℕ)))
  | _, _ => fun _ => 0

/-- Regular coordinate domain: every denominator of the metric, its inverse and the
Christoffel symbols is nonzero. -/
def RegKerr (M a : ℝ) (x : Pt) : Prop := Sig a (x 1) (Real.cos (x 2)) ≠ 0 ∧ Del M a (x 1) ≠ 0 ∧ Real.sin (x 2) ≠ 0

theorem gKerr_00 (M a : ℝ) (x : Pt) : gKerr M a 0 0 x = (-1) + 2*M*(x 1)/Sig a (x 1) (Real.cos (x 2)) := rfl
theorem gKerr_01 (M a : ℝ) (x : Pt) : gKerr M a 0 1 x = 0 := rfl
theorem gKerr_02 (M a : ℝ) (x : Pt) : gKerr M a 0 2 x = 0 := rfl
theorem gKerr_03 (M a : ℝ) (x : Pt) : gKerr M a 0 3 x = ((-2))*M*a*(x 1)*Real.sin (x 2)^(2:ℕ)/Sig a (x 1) (Real.cos (x 2)) := rfl
theorem gKerr_10 (M a : ℝ) (x : Pt) : gKerr M a 1 0 x = 0 := rfl
theorem gKerr_11 (M a : ℝ) (x : Pt) : gKerr M a 1 1 x = Sig a (x 1) (Real.cos (x 2))/Del M a (x 1) := rfl
theorem gKerr_12 (M a : ℝ) (x : Pt) : gKerr M a 1 2 x = 0 := rfl
theorem gKerr_13 (M a : ℝ) (x : Pt) : gKerr M a 1 3 x = 0 := rfl
theorem gKerr_20 (M a : ℝ) (x : Pt) : gKerr M a 2 0 x = 0 := rfl
theorem gKerr_21 (M a : ℝ) (x : Pt) : gKerr M a 2 1 x = 0 := rfl
theorem gKerr_22 (M a : ℝ) (x : Pt) : gKerr M a 2 2 x = Sig a (x 1) (Real.cos (x 2)) := rfl
theorem gKerr_23 (M a : ℝ) (x : Pt) : gKerr M a 2 3 x = 0 := rfl
theorem gKerr_30 (M a : ℝ) (x : Pt) : gKerr M a 3 0 x = ((-2))*M*a*(x 1)*Real.sin (x 2)^(2:ℕ)/Sig a (x 1) (Real.cos (x 2)) := rfl
theorem gKerr_31 (M a : ℝ) (x : Pt) : gKerr M a 3 1 x = 0 := rfl
theorem gKerr_32 (M a : ℝ) (x : Pt) : gKerr M a 3 2 x = 0 := rfl
theorem gKerr_33 (M a : ℝ) (x : Pt) : gKerr M a 3 3 x = Real.sin (x 2)^(2:ℕ)*(a^(2:ℕ) + (x 1)^(2:ℕ) + 2*M*(x 1)*a^(2:ℕ)*Real.sin (x 2)^(2:ℕ)/Sig a (x 1) (Real.cos (x 2))) := rfl
theorem giKerr_00 (M a : ℝ) (x : Pt) : giKerr M a 0 0 x = (Del M a (x 1)*a^(2:ℕ)*Real.sin (x 2)^(2:ℕ) - (a^(2:ℕ) + (x 1)^(2:ℕ))^(2:ℕ))/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1))) := rfl
theorem giKerr_01 (M a : ℝ) (x : Pt) : giKerr M a 0 1 x = 0 := rfl
theorem giKerr_02 (M a : ℝ) (x : Pt) : giKerr M a 0 2 x = 0 := rfl
theorem giKerr_03 (M a : ℝ) (x : Pt) : giKerr M a 0 3 x = ((-2))*M*a*(x 1)/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1))) := rfl
theorem giKerr_10 (M a : ℝ) (x : Pt) : giKerr M a 1 0 x = 0 := rfl
theorem giKerr_11 (M a : ℝ) (x : Pt) : giKerr M a 1 1 x = Del M a (x 1)/Sig a (x 1) (Real.cos (x 2)) := rfl
theorem giKerr_12 (M a : ℝ) (x : Pt) : giKerr M a 1 2 x = 0 := rfl
theorem giKerr_13 (M a : ℝ) (x : Pt) : giKerr M a 1 3 x = 0 := rfl
theorem giKerr_20 (M a : ℝ) (x : Pt) : giKerr M a 2 0 x = 0 := rfl
theorem giKerr_21 (M a : ℝ) (x : Pt) : giKerr M a 2 1 x = 0 := rfl
theorem giKerr_22 (M a : ℝ) (x : Pt) : giKerr M a 2 2 x = 1/Sig a (x 1) (Real.cos (x 2)) := rfl
theorem giKerr_23 (M a : ℝ) (x : Pt) : giKerr M a 2 3 x = 0 := rfl
theorem giKerr_30 (M a : ℝ) (x : Pt) : giKerr M a 3 0 x = ((-2))*M*a*(x 1)/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1))) := rfl
theorem giKerr_31 (M a : ℝ) (x : Pt) : giKerr M a 3 1 x = 0 := rfl
theorem giKerr_32 (M a : ℝ) (x : Pt) : giKerr M a 3 2 x = 0 := rfl
theorem giKerr_33 (M a : ℝ) (x : Pt) : giKerr M a 3 3 x = (Del M a (x 1) - a^(2:ℕ)*Real.sin (x 2)^(2:ℕ))/((Sig a (x 1) (Real.cos (x 2))*Del M a (x 1)*Real.sin (x 2)^(2:ℕ))) := rfl

/-! Source lock: each component equals the token-level transcription of the metric.json string. -/
theorem gKerr_00_src (M a : ℝ) (x : Pt) : gKerr M a 0 0 x = -(1 - 2*M*(x 1)/((x 1)^(2:ℕ) + a^(2:ℕ)*Real.cos (x 2)^(2:ℕ))) := by
  simp only [gKerr_00, Sig, Del]
  first | done | ring1
theorem gKerr_11_src (M a : ℝ) (x : Pt) : gKerr M a 1 1 x = ((x 1)^(2:ℕ) + a^(2:ℕ)*Real.cos (x 2)^(2:ℕ))/((x 1)^(2:ℕ) - 2*M*(x 1) + a^(2:ℕ)) := by
  simp only [gKerr_11, Sig, Del]
  first | done | ring1
theorem gKerr_22_src (M a : ℝ) (x : Pt) : gKerr M a 2 2 x = (x 1)^(2:ℕ) + a^(2:ℕ)*Real.cos (x 2)^(2:ℕ) := by
  simp only [gKerr_22, Sig, Del]
  first | done | ring1
theorem gKerr_33_src (M a : ℝ) (x : Pt) : gKerr M a 3 3 x = ((x 1)^(2:ℕ) + a^(2:ℕ) + 2*M*(x 1)*a^(2:ℕ)*Real.sin (x 2)^(2:ℕ)/((x 1)^(2:ℕ) + a^(2:ℕ)*Real.cos (x 2)^(2:ℕ)))*Real.sin (x 2)^(2:ℕ) := by
  simp only [gKerr_33, Sig, Del]
  first | done | ring1
theorem gKerr_03_src (M a : ℝ) (x : Pt) : gKerr M a 0 3 x = -2*M*a*(x 1)*Real.sin (x 2)^(2:ℕ)/((x 1)^(2:ℕ) + a^(2:ℕ)*Real.cos (x 2)^(2:ℕ)) := by
  simp only [gKerr_03, Sig, Del]
  first | done | ring1

end KerrBL

Source

R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237-238, https://doi.org/10.1103/PhysRevLett.11.237; R. H. Boyer and R. W. Lindquist, Maximal analytic extension of the Kerr metric, J. Math. Phys. 8 (1967) 265-281, https://doi.org/10.1063/1.1705193, Sec. 2 (Boyer-Lindquist form of the Kerr line element); metric components transcribed token-for-token from the project certificate EinsteinSolver/certificate/kerr/metric.json (sha256 d729883d95fd7d3cf84d9c971c6725f847155562cc4e88660535b8d0bd0be336); design record LEAN/kerr-formalization/mission/DESIGN.md, definition bundle D2 (generated from metric.json, human-auditable)

Human review

Endorsed by Shuze Chen · Sep 14, 2026
Endorsed by He Wang · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph