Kerr in ingoing (Kerr's original) coordinates: metric, candidate inverse, domain

Definition

Atlas_Kerr_InDefs

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

coordinate-geometryexact-vacuum-atlasgeneral-relativityingoing-kerr-coordinateskerr-metric

In coordinates $(v,r,\theta,\varphi)=(x_0,x_1,x_2,x_3)$ , $\Sigma=r^2+a^2\cos^2\theta$ , $F=1-2Mr/\Sigma$ , $A=a\sin^2\theta$ , the ingoing Kerr metric $g^{\rm in}_{M,a}$ has $g_{vv}=-F$ , $g_{vr}=g_{rv}=1$ , $g_{v\varphi}=g_{\varphi v}=(1-F)A$ , $g_{r\varphi}=g_{\varphi r}=A$ , $g_{\theta\theta}=\Sigma$ , $g_{\varphi\varphi}=(2-F)A^2+\Sigma\sin^2\theta$ and all other entries $0$ ; this is Visser's line element $ds^2=-F(dv+A\,d\varphi)^2+2(dv+A\,d\varphi)(dr+A\,d\varphi)+\Sigma(d\theta^2+\sin^2\theta\,d\varphi^2)$ read with the half-Hessian convention ( $g_{vr}=1$ from $2\,dv\,dr$ ). The candidate inverse $\hat g^{\rm in}_{M,a}$ has $\hat g^{vv}=a^2\sin^2\theta/\Sigma$ , $\hat g^{vr}=\hat g^{rv}=(r^2+a^2)/\Sigma$ , $\hat g^{v\varphi}=\hat g^{\varphi v}=\hat g^{r\varphi}=\hat g^{\varphi r}=-a/\Sigma$ , $\hat g^{rr}=(r^2-2Mr+a^2)/\Sigma$ , $\hat g^{\theta\theta}=1/\Sigma$ , $\hat g^{\varphi\varphi}=1/(\Sigma\sin^2\theta)$ , other entries $0$ . The domain is $U^{\rm in}_a=\{x:\ \Sigma\neq0,\ \sin\theta\neq0\}$ (there is no $\Delta\neq0$ restriction; a point with $\Delta=0$ lies in the domain precisely when it also satisfies $\Sigma\neq0$ and $\sin\theta\neq0$ ). Also the equatorial point $(0,\rho,\pi/2,0)$ .

Clarification of the preserved source comment (2026-10-14). The published Lean text of this bundle keeps its original module docstring. The comment does not affect the Lean definitions and is left unchanged (published payloads are immutable; no replacement node was created). Three phrases there are to be read as follows. (i) “Visser's u is called v here (it is the advanced null coordinate)”: $v$ is an advanced-type coordinate; the radial coordinate vector $\partial_r$ is null ( $g_{rr}=0$ ), but for $a\neq0$ the covector $dv$ is not null, since $\hat g^{vv}=a^2\sin^2\theta/\Sigma\neq0$ on the domain (where $\hat g$ is the inverse by ExactVacuumAtlas.Kerr.In.cert); no claim is made that the hypersurfaces $v=\text{const}$ are null. (ii) “…, all other entries 0” after a list naming only $g_{vr}$ , $g_{v\varphi}$ , $g_{r\varphi}$ among the off-diagonal entries: the matrix is symmetric, and the definition gIn sets $g_{rv}$ , $g_{\varphi v}$ , $g_{\varphi r}$ to the same values; only the remaining entries are $0$ . (iii) “the coordinate locus Δ = 0 (horizon radii, as a name only) lies inside the domain”: there is no $\Delta\neq0$ restriction, and a point with $\Delta=0$ lies in the domain precisely when it also satisfies $\Sigma\neq0$ and $\sin\theta\neq0$ ; whether such points exist depends on $(M,a)$ (ExactVacuumAtlas.Release01.coverage gives one for $M>0$ , $a^2\le M^2$ ).

Row 7 data (all real $M,a$ ). The inverse is data to be verified, not assumed; the domain deliberately omits $\Delta\neq0$ .

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Kerr.InDefs; declarations: ExactVacuumAtlas.Kerr.In.domIn, ExactVacuumAtlas.Kerr.In.eqPt, ExactVacuumAtlas.Kerr.In.gIn, ExactVacuumAtlas.Kerr.In.giIn. 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/InDefs.lean
-- definition bundle: kept ExactVacuumAtlas.Kerr.In.domIn, ExactVacuumAtlas.Kerr.In.eqPt, ExactVacuumAtlas.Kerr.In.gIn, ExactVacuumAtlas.Kerr.In.giIn
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-!
# Kerr in Kerr's original (ingoing / advanced Eddington–Finkelstein) coordinates

Source: Visser, *The Kerr spacetime: a brief introduction*, arXiv:0706.0622, eq. (E:K1)
(local copy `archive/sources_atlas01/arXiv_0706.0622_eprint.tgz`, file `Survey-grqc-3.tex`,
lines 205–215), units `G = c = 1`, mass `m = M`:

`ds² = −[1 − 2Mr/Σ] (du + a sin²θ dφ)² + 2 (du + a sin²θ dφ)(dr + a sin²θ dφ) + Σ (dθ² + sin²θ dφ²)`,
`Σ = r² + a² cos²θ`.

Coordinates `(v, r, θ, φ) = (x 0, x 1, x 2, x 3)`; Visser's `u` is called `v` here (it is the
advanced null coordinate). Matrix entries are read off with the half-Hessian convention
(`g_{vr} = 1` from `2 dv dr`): with `F = 1 − 2Mr/Σ` and `A = a sin²θ`,
`g_vv = −F`, `g_vr = 1`, `g_vφ = −F A + A`, `g_rφ = A`, `g_θθ = Σ`,
`g_φφ = −F A² + 2 A² + Σ sin²θ`, all other entries `0`.

Parameters: every real `M`, `a`. Domain: `Σ ≠ 0`, `sin θ ≠ 0`. There is **no** `Δ ≠ 0`
condition: the coordinate locus `Δ = r² − 2Mr + a² = 0` (horizon radii, as a name only) lies inside
the domain. No causal statement is made.
-/

open Real

namespace ExactVacuumAtlas.Kerr.In

/-- Kerr metric in Kerr's original ingoing coordinates (Visser E:K1). -/
noncomputable def gIn (M a : ℝ) : Metric 4
  | 0, 0 => fun x => -(1 - 2 * M * x 1 / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2))
  | 0, 1 => fun _ => 1
  | 1, 0 => fun _ => 1
  | 0, 3 => fun x => -(1 - 2 * M * x 1 / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)) * (a * sin (x 2) ^ 2)
      + a * sin (x 2) ^ 2
  | 3, 0 => fun x => -(1 - 2 * M * x 1 / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)) * (a * sin (x 2) ^ 2)
      + a * sin (x 2) ^ 2
  | 1, 3 => fun x => a * sin (x 2) ^ 2
  | 3, 1 => fun x => a * sin (x 2) ^ 2
  | 2, 2 => fun x => x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2
  | 3, 3 => fun x => -(1 - 2 * M * x 1 / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)) * (a * sin (x 2) ^ 2) ^ 2
      + 2 * (a * sin (x 2) ^ 2) ^ 2 + (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2) * sin (x 2) ^ 2
  | _, _ => fun _ => 0

/-- Candidate inverse (checked, not assumed, in the certificate). -/
noncomputable def giIn (M a : ℝ) : Metric 4
  | 0, 0 => fun x => a ^ 2 * sin (x 2) ^ 2 / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 0, 1 => fun x => (x 1 ^ 2 + a ^ 2) / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 1, 0 => fun x => (x 1 ^ 2 + a ^ 2) / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 0, 3 => fun x => -a / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 3, 0 => fun x => -a / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 1, 1 => fun x => (x 1 ^ 2 - 2 * M * x 1 + a ^ 2) / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 1, 3 => fun x => -a / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 3, 1 => fun x => -a / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 2, 2 => fun x => 1 / (x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2)
  | 3, 3 => fun x => 1 / ((x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2) * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Domain of the ingoing chart: `Σ ≠ 0` and `sin θ ≠ 0`; `v, r, φ` otherwise arbitrary. -/
def domIn (a : ℝ) : Set (Pt 4) := {x | x 1 ^ 2 + a ^ 2 * cos (x 2) ^ 2 ≠ 0 ∧ sin (x 2) ≠ 0}

/-- Equatorial point `(0, ρ, π/2, 0)`. -/
noncomputable def eqPt (ρ : ℝ) : Pt 4 := ![0, ρ, π / 2, 0]

end ExactVacuumAtlas.Kerr.In

Source

M. Visser, arXiv:0706.0622, eq. (E:K1) (Survey-grqc-3.tex lines 205–215), Visser's u renamed v; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Kerr/InDefs.lean (source module Atlas.Kerr.InDefs, file sha256 92173ff8b35ada9a1760d7ae329e4b7269959cba38661c8d5b59d7c915eb5b35; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Kerr_InDefs.lean, sha256 7e78d96ef73df0fb80c48d219f4a41d1e39e2903166ed06e4b8d37a6de631b7c)

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