R3 data: Boyer–Lindquist to ingoing Kerr map, inverse, Jacobian and explicit antiderivatives of $1/\Delta$

Definition

Atlas_Kerr_R3

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

boyer-lindquistcoordinate-geometrycoordinate-transformationexact-vacuum-atlasgeneral-relativityingoing-kerr-coordinateskerr-metric

With $\Delta(r)=r^2-2Mr+a^2$ (Delta) and the radial set $\{r:\Delta(r)\neq0\}$ (radDom): for functions $H_1,H_2:\mathbb R\to\mathbb R$ the map $\Phi_{H_1,H_2}(t,r,\theta,\varphi)=(t+r+H_1(r),\ r,\ \theta,\ -\varphi-H_2(r))$ (toIn) and its inverse $\Psi_{H_1,H_2}(v,r,\theta,\tilde\varphi)=(v-r-H_1(r),\ r,\ \theta,\ -\tilde\varphi-H_2(r))$ (fromIn); the Jacobian

J(x)=\begin{pmatrix}1&\frac{r^2+a^2}{\Delta}&0&0\\0&1&0&0\\0&0&1&0\\0&-\frac a\Delta&0&-1\end{pmatrix}

(jac); the three branch antiderivatives $K_{\rm two}(b,r)=\frac{\log(r-(M+b))-\log(r-(M-b))}{2b}$ , $K_{\rm arc}(b,r)=\frac{\arctan((r-M)/b)}{b}$ , $K_{\rm dbl}(r)=-\frac1{r-M}$ ; the global $K(r)$ chosen by the sign of $M^2-a^2$ ( $b=\sqrt{|M^2-a^2|}$ ); and $H_1(r)=M\log\Delta(r)+2M^2K(r)$ , $H_2(r)=aK(r)$ , so that $H_1'=2Mr/\Delta$ , $H_2'=a/\Delta$ off the roots (Mathlib's $\log$ is $\log|\cdot|$ ).

Data of relation R3 (Visser's change of coordinates $u=t+r$ , $t=t_{\rm BL}+2M\int r\,dr/\Delta$ , $\varphi=-\varphi_{\rm BL}-a\int dr/\Delta$ with the integrals made explicit for every real $M,a$ ). The generic obligations are proved for arbitrary $H_1,H_2$ with these derivatives, then instantiated.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Kerr.R3; declarations: ExactVacuumAtlas.Kerr.R3.H1, ExactVacuumAtlas.Kerr.R3.H2, ExactVacuumAtlas.Kerr.R3.K, ExactVacuumAtlas.Kerr.R3.Karc, ExactVacuumAtlas.Kerr.R3.Kdbl, ExactVacuumAtlas.Kerr.R3.Ktwo, ExactVacuumAtlas.Kerr.R3.fromIn, ExactVacuumAtlas.Kerr.R3.jac, ExactVacuumAtlas.Kerr.R3.radDom, ExactVacuumAtlas.Kerr.R3.toIn, ExactVacuumAtlas.Kerr.R3.Delta. 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/R3.lean
-- definition bundle: kept ExactVacuumAtlas.Kerr.R3.H₁, ExactVacuumAtlas.Kerr.R3.H₂, ExactVacuumAtlas.Kerr.R3.K, ExactVacuumAtlas.Kerr.R3.Karc, ExactVacuumAtlas.Kerr.R3.Kdbl, ExactVacuumAtlas.Kerr.R3.Ktwo, ExactVacuumAtlas.Kerr.R3.fromIn, ExactVacuumAtlas.Kerr.R3.jac, ExactVacuumAtlas.Kerr.R3.radDom, ExactVacuumAtlas.Kerr.R3.toIn, ExactVacuumAtlas.Kerr.R3.Δ
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Kerr_Domain
import Definitions.Def_Atlas_Kerr_InDefs
import Definitions.Def_KerrBL_CoordGeometry
import Definitions.Def_KerrBL_Kerr_Metric
set_option maxHeartbeats 4000000

/-!
# R3: Boyer–Lindquist ↔ ingoing Kerr on the overlap `Δ ≠ 0`

Visser, arXiv:0706.0622, eqs. (E:BL-change-1)–(E:BL-change-3): starting from the ingoing form
(E:K1) with coordinates `(u, r, θ, φ)`,
`u = t + r`, `t = t_BL + 2M ∫ r dr/Δ`, `φ = −φ_BL − a ∫ dr/Δ`, `r = r_BL`, `θ = θ_BL`,
gives the Boyer–Lindquist line element (our `KerrBL.gKerr`). Hence the map BL → ingoing is

  `toIn x = (t + r + H₁(r), r, θ, −φ − H₂(r))`, `H₁' = 2Mr/Δ`, `H₂' = a/Δ`,

with inverse `fromIn y = (v − r − H₁(r), r, θ, −φ̃ − H₂(r))`. The Jacobian is
`∂v/∂r = 1 + 2Mr/Δ = (r² + a²)/Δ`, `∂φ̃/∂r = −a/Δ`, `∂φ̃/∂φ = −1`.

**Generic part** (this file, section `Generic`): for *any* `H₁ H₂ : ℝ → ℝ` with those derivatives
on `{Δ ≠ 0}` and `C^∞` there, all R3 obligations hold: `C^∞` both ways, bijection of `domBL`
onto itself, Jacobian entries are genuine derivatives, and `jacᵀ · (gIn ∘ toIn) · jac = gKerr`.

**Reading note.** `gIn` depends only on `(r, θ)`, which `toIn` fixes, and `jac` is an explicit matrix, so
the identity `pullback` alone does not involve `H₁ H₂`; it certifies the map only *together with*
`hasDerivAt_pd_toIn` / `pd_toIn`, which prove that `jac` is the genuine Jacobian of `toIn` (this is where
`H₁' = 2Mr/Δ`, `H₂' = a/Δ` enter). Cite the pair. `φ ∼ φ + 2π` is not modelled (`φ, φ̃ ∈ ℝ`).

**Concrete part** (section `Branches`): explicit `H₁`, `H₂` for the three parameter branches
`M² > a²` (two real roots, logarithms), `M² = a²` (double root, rational `K`; `H₁` keeps its `M log|Δ|`
term) and `M² < a²` (no real root, arctan), each with its derivative proved; then the generic result is instantiated. These
are parameter sub-rows of R3, not a reduction of its scope.
-/

open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Kerr

namespace ExactVacuumAtlas.Kerr.R3

/-- `Δ = r² − 2Mr + a²`. -/
noncomputable def Delta (M a r : ℝ) : ℝ := r ^ 2 - 2 * M * r + a ^ 2

section Generic

variable (M a : ℝ) (H₁ H₂ : ℝ → ℝ)

/-- BL → ingoing. -/
noncomputable def toIn (x : Pt 4) : Pt 4 := ![x 0 + x 1 + H₁ (x 1), x 1, x 2, -(x 3) - H₂ (x 1)]

/-- ingoing → BL. -/
noncomputable def fromIn (y : Pt 4) : Pt 4 := ![y 0 - y 1 - H₁ (y 1), y 1, y 2, -(y 3) - H₂ (y 1)]

/-- The set of radii with `Δ ≠ 0`. -/
def radDom : Set ℝ := {r | Delta M a r ≠ 0}

variable (h₁ : ContDiffOn ℝ ∞ H₁ (radDom M a)) (h₂ : ContDiffOn ℝ ∞ H₂ (radDom M a))
include h₁ h₂

omit h₁ h₂

/-- Jacobian of `toIn`: row `k` = output component, column `i` = input coordinate. -/
noncomputable def jac (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, (x 1 ^ 2 + a ^ 2) / Delta M a (x 1), 0, 0;
     0, 1, 0, 0;
     0, 0, 1, 0;
     0, -a / Delta M a (x 1), 0, -1]

variable (d₁ : ∀ r ∈ radDom M a, HasDerivAt H₁ (2 * M * r / Delta M a r) r)
variable (d₂ : ∀ r ∈ radDom M a, HasDerivAt H₂ (a / Delta M a r) r)
include d₁

omit d₁
include d₂

omit d₂
include d₁ d₂

omit d₁ d₂

end Generic

/-! ## Concrete antiderivatives `K` with `K' = 1/Δ`, by parameter branch -/
section Branches

variable (M a : ℝ)

/-- Two real roots `r± = M ± b`, `b = √(M² − a²)`, `M² > a²`. -/
noncomputable def Ktwo (b r : ℝ) : ℝ := (log (r - (M + b)) - log (r - (M - b))) / (2 * b)

/-- No real root, `M² < a²`, `b = √(a² − M²)`. -/
noncomputable def Karc (b r : ℝ) : ℝ := arctan ((r - M) / b) / b

/-- Double root `M² = a²`. -/
noncomputable def Kdbl (r : ℝ) : ℝ := -(r - M)⁻¹

/-- `K` on the whole parameter space, chosen by the sign of `M² − a²`. -/
noncomputable def K (r : ℝ) : ℝ :=
  if 0 < M ^ 2 - a ^ 2 then Ktwo M (Real.sqrt (M ^ 2 - a ^ 2)) r
  else if M ^ 2 - a ^ 2 < 0 then Karc M (Real.sqrt (a ^ 2 - M ^ 2)) r
  else Kdbl M r

/-- `H₁ = M log|Δ| + 2M² K` (`H₁' = 2Mr/Δ`). -/
noncomputable def H1 (r : ℝ) : ℝ := M * log (Delta M a r) + 2 * M ^ 2 * K M a r

/-- `H₂ = a K` (`H₂' = a/Δ`). -/
noncomputable def H2 (r : ℝ) : ℝ := a * K M a r

/-! ## R3 instantiated with the explicit `H₁`, `H₂` (all real `M`, `a`) -/

end Branches

end ExactVacuumAtlas.Kerr.R3

Source

M. Visser, arXiv:0706.0622, eqs. (E:BL-change-1), (E:BL-change-2), (E:BL-change-3): u = t + r, t = t_BL + 2M∫ r dr/Δ, φ = −φ_BL − a∫ dr/Δ; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Kerr/R3.lean (source module Atlas.Kerr.R3, file sha256 8c3daf73ffed5d59070e65502f367d8325cf71e38068784dd6b32e7621d72d5c; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Kerr_R3.lean, sha256 4e2946f2cf920f9c76764f0efb1298f85fd2d43be7dfcc8346fb58d8a434f7df)

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

R3 data: Boyer–Lindquist to ingoing Kerr map, inverse, Jacobian and explicit antiderivatives of 1/Δ1/\Delta1/Δ

R3 data: Boyer–Lindquist to ingoing Kerr map, inverse, Jacobian and explicit antiderivatives of $1/\Delta$