Minkowski metric in spherical coordinates and its domain

Definition

Atlas_Minkowski_Spherical

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

coordinate-geometryexact-vacuum-atlasgeneral-relativityminkowski-spacespherical-coordinates

In coordinates $(t,r,\theta,\varphi)$ : $g^{\rm sph}=\mathrm{diag}(-1,\ 1,\ r^2,\ r^2\sin^2\theta)$ (line element $ds^2=-dt^2+dr^2+r^2(d\theta^2+\sin^2\theta\,d\varphi^2)$ ), candidate inverse $\mathrm{diag}(-1,1,1/r^2,1/(r^2\sin^2\theta))$ , and the domain $U^{\rm sph}=\{r>0,\ 0<\theta<\pi\}$ (equal to the Eddington–Finkelstein domain of bundle Atlas_Schwarzschild_Defs).

Row 2 data, written independently of Schwarzschild; the certificate is obtained from Schwarzschild at $M=0$ by transport.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Minkowski.Spherical; declarations: ExactVacuumAtlas.Minkowski.domSph, ExactVacuumAtlas.Minkowski.gSph, ExactVacuumAtlas.Minkowski.giSph. 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/Minkowski/Spherical.lean
-- definition bundle: kept ExactVacuumAtlas.Minkowski.domSph, ExactVacuumAtlas.Minkowski.gSph, ExactVacuumAtlas.Minkowski.giSph
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_Atlas_Schwarzschild_StdParts
import Definitions.Def_KerrBL_CoordGeometry
import Definitions.Def_KerrBL_Kerr_Metric
/-!
# Minkowski space in spherical coordinates `(t, r, θ, φ)`

`ds² = -dt² + dr² + r²(dθ² + sin²θ dφ²)` (Müller–Grave, *Catalogue of Spacetimes*, eq. minkSph).
The data below are written independently; the certificate is obtained by proving that they
coincide with standard Schwarzschild at `M = 0` on the domain, then transporting `Std.cert 0`.
Domain: `r > 0`, `0 < θ < π` (`domEF`), so the axis and the origin are excluded.
-/

open Real

namespace ExactVacuumAtlas.Minkowski

open ExactVacuumAtlas.Schwarzschild

noncomputable def gSph : Metric 4
  | 0, 0 => fun _ => -1
  | 1, 1 => fun _ => 1
  | 2, 2 => fun x => x 1 ^ 2
  | 3, 3 => fun x => x 1 ^ 2 * sin (x 2) ^ 2
  | _, _ => fun _ => 0

noncomputable def giSph : Metric 4
  | 0, 0 => fun _ => -1
  | 1, 1 => fun _ => 1
  | 2, 2 => fun x => 1 / x 1 ^ 2
  | 3, 3 => fun x => 1 / (x 1 ^ 2 * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Spherical chart domain `r > 0`, `0 < θ < π`. -/
def domSph : Set (Pt 4) := domEF

end ExactVacuumAtlas.Minkowski

Source

Müller–Grave catalogue eqs. minkCart and minkSph; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Minkowski/Spherical.lean (source module Atlas.Minkowski.Spherical, file sha256 ab4b8959cd1ac9b6b83f657f27f3300b2e02cd2984faf598e05b2b6b51035b1f; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Minkowski_Spherical.lean, sha256 9d901c608f9fefe419897fd15fa23bdb52da4571b18d85c58eebb5887b5fbeea)

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