Prove2Me

Ingoing Kerr: rational atoms 1/Σ1/\Sigma and 1/sin⁡θ1/\sin\theta

Definition
Atlas_Kerr_InAtoms

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

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

Two notation wrappers: U(a,r,θ)=(r2+a2cos⁡2θ)−1=1/ΣU(a,r,\theta)=\big(r^2+a^2\cos^2\theta\big)^{-1}=1/\Sigma (Ui) and W(θ)=(sin⁡θ)−1W(\theta)=(\sin\theta)^{-1} (Wi), Mathlib's total real inverse (value 00 at 00).

The generated ingoing-Kerr tables are polynomials in r,sin⁡θ,cos⁡θ,U,Wr,\sin\theta,\cos\theta,U,W; the wrappers make 1/Σ1/\Sigma and 1/sin⁡θ1/\sin\theta opaque atoms for normalisation, and their derivative rules are the only analytic input.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Kerr.InAtoms; declarations: ExactVacuumAtlas.Kerr.In.Ui, ExactVacuumAtlas.Kerr.In.Wi. 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/InAtoms.lean
-- definition bundle: kept ExactVacuumAtlas.Kerr.In.Ui, ExactVacuumAtlas.Kerr.In.Wi
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_Kerr_InDefs
/-!
# Ingoing Kerr: rational atoms and their derivatives

Notation wrappers (B3 class B): `Ui a r θ = (r² + a² cos²θ)⁻¹ = 1/Σ` and `Wi θ = (sin θ)⁻¹`.
Generated tables (`Atlas.Kerr.InTables`) are polynomials in `r, sin θ, cos θ, Ui, Wi`; these
wrappers make `ring` treat `1/Σ` and `1/sin θ` as atoms. The derivative rules below are the
only analytic input of the tables.
-/

open Real

namespace ExactVacuumAtlas.Kerr.In

/-- `1/Σ` with `Σ = r² + a² cos²θ`. -/
noncomputable def Ui (a r θ : ℝ) : ℝ := (r ^ 2 + a ^ 2 * cos θ ^ 2)⁻¹

/-- `1/sin θ`. -/
noncomputable def Wi (θ : ℝ) : ℝ := (sin θ)⁻¹

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/InAtoms.lean (source module Atlas.Kerr.InAtoms, file sha256 30e14f9094cc6659a7670a18a03040eb71977f1710ab1a059d8f086edad7527a; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Kerr_InAtoms.lean, sha256 2ca1035b3897072e8df68cfa1efaf1f384be37fe0ae0c2377a84a9624e9af533)
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