Prove2Me

Boyer–Lindquist Kerr: Carter-type frames for Δ>0\Delta>0 and Δ<0\Delta<0

Definition
Atlas_Kerr_Frame

by He Wang · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

boyer-lindquistcoordinate-geometryexact-vacuum-atlasgeneral-relativitykerr-metriclorentzian-signature

Two explicit 4×44\times4 matrix fields in coordinates (t,r,θ,φ)(t,r,\theta,\varphi), columns T0=(r2+a2)∂t+a∂φT_0=(r^2+a^2)\partial_t+a\partial_\varphi, T1=∂rT_1=\partial_r, T2=∂θT_2=\partial_\theta, T3=asin⁡2θ ∂t+∂φT_3=a\sin^2\theta\,\partial_t+\partial_\varphi (frameP, for Δ>0\Delta>0), and the same columns with T0,T1T_0,T_1 swapped (frameN, for Δ<0\Delta<0, where ∂r\partial_r is timelike):

frameP=(r2+a200asin⁡2θ01000010a001).\mathrm{frameP}=\begin{pmatrix}r^2+a^2&0&0&a\sin^2\theta\\0&1&0&0\\0&0&1&0\\a&0&0&1\end{pmatrix}.

They diagonalise the Boyer–Lindquist metric without square roots: for T=framePT=\mathrm{frameP} the diagonal is (−ΔΣ, Σ/Δ, Σ, Σsin⁡2θ)(-\Delta\Sigma,\ \Sigma/\Delta,\ \Sigma,\ \Sigma\sin^2\theta), and for T=frameNT=\mathrm{frameN} the first two entries are exchanged, TTgT=diag(Σ/Δ,−ΔΣ,Σ,Σsin⁡2θ)T^{\mathsf T}gT=\mathrm{diag}(\Sigma/\Delta,-\Delta\Sigma,\Sigma,\Sigma\sin^2\theta); det⁡frameP=Σ\det\mathrm{frameP}=\Sigma.

Frame data for the signature obligation of row 6 (theorem ExactVacuumAtlas.Kerr.lorentz); the unnormalised Carter tetrad directions.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Kerr.Frame; declarations: ExactVacuumAtlas.Kerr.frameN, ExactVacuumAtlas.Kerr.frameP. No theorem is proved inside the bundle; it imports only Mathlib and other Definitions.Def_* bundles.

Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Kerr/Frame.lean
-- definition bundle: kept ExactVacuumAtlas.Kerr.frameN, ExactVacuumAtlas.Kerr.frameP
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Kerr_Domain
import Definitions.Def_KerrBL_CoordGeometry
import Definitions.Def_KerrBL_Kerr_Metric
/-!
# Kerr, Boyer–Lindquist: Lorentz signature on the whole regular domain

Let `P = r² + a²`. The unnormalised Carter-type frame
`T₀ = P ∂_t + a ∂_φ`, `T₁ = ∂_r`, `T₂ = ∂_θ`, `T₃ = a sin²θ ∂_t + ∂_φ`
(columns of `frameP`; `det frameP = P − a² sin²θ = Σ`) diagonalises the metric *without square
roots*: `Tᵀ g T = diag(−ΔΣ, Σ/Δ, Σ, Σ sin²θ)`. The three nontrivial identities are
`P² g_tt + 2aP g_tφ + a² g_φφ = −ΔΣ`, `a sin²θ · P · g_tt + (P + a² sin²θ) g_tφ + a g_φφ = 0` and
`a² sin⁴θ g_tt + 2a sin²θ g_tφ + g_φφ = Σ sin²θ`; they hold on `Σ ≠ 0` using `cos²θ = 1 − sin²θ`.

For `Δ > 0` the first entry is negative and the rest positive; for `Δ < 0` the roles of `T₀`
and `T₁` are swapped (`frameN`), since then `∂_r` is timelike and `T₀` spacelike. No part of `domBL`
(`Δ < 0`, `r < 0`, `g_tt ≥ 0`, `g_φφ ≤ 0`) is excluded. Normalisation by `1/√|dᵢ|`
happens once, in `isLorentzian_of_diag`.
-/

open Real

namespace ExactVacuumAtlas.Kerr

/-- Frame for `Δ > 0`: columns `P ∂_t + a ∂_φ`, `∂_r`, `∂_θ`, `a sin²θ ∂_t + ∂_φ`. -/
noncomputable def frameP (a : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![(x 1)^2 + a^2, 0, 0, a * sin (x 2)^2;
     0, 1, 0, 0;
     0, 0, 1, 0;
     a, 0, 0, 1]

/-- Frame for `Δ < 0`: the same columns with the first two swapped (`∂_r` timelike). -/
noncomputable def frameN (a : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![0, (x 1)^2 + a^2, 0, a * sin (x 2)^2;
     1, 0, 0, 0;
     0, 0, 1, 0;
     0, a, 0, 1]

end ExactVacuumAtlas.Kerr
Source
R. P. Kerr, Phys. Rev. Lett. 11 (1963) 237, https://doi.org/10.1103/PhysRevLett.11.237; R. H. Boyer, R. W. Lindquist, J. Math. Phys. 8 (1967) 265, https://doi.org/10.1063/1.1705193; Müller–Grave catalogue eq. kerrBLbardeen; metric data = platform definition KerrBL_Kerr_Metric (id 8b2152c1-375e-4302-8acf-50c30d42d46d); Sylvester's law of inertia (standard linear algebra); Mathlib LinearAlgebra/QuadraticForm/Signature.lean (pinned 0df444a3) for sigPos/sigNeg; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Kerr/Frame.lean (source module Atlas.Kerr.Frame, file sha256 5a92b81fee538de9260bd7366efb75564a03d8023a764de125f0f9562b79d07a; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Kerr_Frame.lean, sha256 545ebda36f580128c0761e9b420c1a726573a5380cc8634f09378c7732139094)
Human review

  • Endorsed by Shuze Chen · Oct 14, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 14, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph