Prove2Me

Schwarzschild data: standard and Eddington–Finkelstein metrics, inverses, domains, coordinate maps

Definition
Atlas_Schwarzschild_Defs

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

coordinate-geometryeddington-finkelsteinexact-vacuum-atlasgeneral-relativityschwarzschild-metric

Units G=c=1G=c=1, signature (−,+,+,+)(-,+,+,+), rs=2Mr_s=2M, coordinates indexed 0,1,2,30,1,2,3. Standard (t,r,θ,φ)(t,r,\theta,\varphi): gMstd=diag(−(1−2Mr), 11−2M/r, r2, r2sin⁡2θ)g^{\rm std}_M=\mathrm{diag}\big(-(1-\tfrac{2M}r),\ \tfrac1{1-2M/r},\ r^2,\ r^2\sin^2\theta\big), candidate inverse diag(−11−2M/r, 1−2Mr, 1r2, 1r2sin⁡2θ)\mathrm{diag}\big(-\tfrac1{1-2M/r},\ 1-\tfrac{2M}r,\ \tfrac1{r^2},\ \tfrac1{r^2\sin^2\theta}\big), domain UMstd={r>0, r≠2M, 0<θ<π}U^{\rm std}_M=\{r>0,\ r\neq2M,\ 0<\theta<\pi\}. Eddington–Finkelstein family (w,r,θ,φ)(w,r,\theta,\varphi), ε=1\varepsilon=1 ingoing (w=vw=v), ε=−1\varepsilon=-1 outgoing (w=uw=u): gww=−(1−2Mr)g_{ww}=-(1-\tfrac{2M}r), gwr=grw=εg_{wr}=g_{rw}=\varepsilon, gθθ=r2g_{\theta\theta}=r^2, gφφ=r2sin⁡2θg_{\varphi\varphi}=r^2\sin^2\theta, other entries 00 (from ds2=−(1−rs/r)dv2+2 dv dr+r2dΩ2ds^2=-(1-r_s/r)dv^2+2\,dv\,dr+r^2d\Omega^2, matrix entry gvr=1g_{vr}=1, not 22); candidate inverse g^wr=g^rw=ε\hat g^{wr}=\hat g^{rw}=\varepsilon, g^rr=1−2Mr\hat g^{rr}=1-\tfrac{2M}r, g^θθ=1r2\hat g^{\theta\theta}=\tfrac1{r^2}, g^φφ=1r2sin⁡2θ\hat g^{\varphi\varphi}=\tfrac1{r^2\sin^2\theta} (valid when ε2=1\varepsilon^2=1); domain UEF={r>0, 0<θ<π}U^{\rm EF}=\{r>0,\ 0<\theta<\pi\}, which contains r=2Mr=2M when M>0M>0. Coordinate maps: ΦM,ε(t,r,θ,φ)=(t+ε(r+2Mlog⁡∣r−2M∣),r,θ,φ)\Phi_{M,\varepsilon}(t,r,\theta,\varphi)=(t+\varepsilon(r+2M\log\lvert r-2M\rvert),r,\theta,\varphi) (toEF) and ΨM,ε(w,r,θ,φ)=(w−ε(r+2Mlog⁡∣r−2M∣),r,θ,φ)\Psi_{M,\varepsilon}(w,r,\theta,\varphi)=(w-\varepsilon(r+2M\log\lvert r-2M\rvert),r,\theta,\varphi) (fromEF); Mathlib's log⁡\log is log⁡∣⋅∣\log|\cdot|, so these are the usual r+2Mln⁡∣r−2M∣r+2M\ln|r-2M| on both sides of r=2Mr=2M.

Data of rows 3–5 and relations R1–R2 (all real MM; no sign assumed).

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Schwarzschild.Defs; declarations: ExactVacuumAtlas.Schwarzschild.domEF, ExactVacuumAtlas.Schwarzschild.domStd, ExactVacuumAtlas.Schwarzschild.fromEF, ExactVacuumAtlas.Schwarzschild.gEF, ExactVacuumAtlas.Schwarzschild.gStd, ExactVacuumAtlas.Schwarzschild.giEF, ExactVacuumAtlas.Schwarzschild.giStd, ExactVacuumAtlas.Schwarzschild.toEF. 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/Schwarzschild/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.domEF, ExactVacuumAtlas.Schwarzschild.domStd, ExactVacuumAtlas.Schwarzschild.fromEF, ExactVacuumAtlas.Schwarzschild.gEF, ExactVacuumAtlas.Schwarzschild.gStd, ExactVacuumAtlas.Schwarzschild.giEF, ExactVacuumAtlas.Schwarzschild.giStd, ExactVacuumAtlas.Schwarzschild.toEF
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-!
# Schwarzschild: catalogue data (independent of any proof)

Coordinates are indexed `0, 1, 2, 3`; units `G = c = 1`, signature `(-,+,+,+)`, mass `M`.

Sources (local copies with SHA-256 in `archive/sources_atlas01/`):
* standard coordinates `(t, r, θ, φ)`: Müller–Grave, *Catalogue of Spacetimes*, arXiv:0904.4184v3,
  eq. (schwarzschildSpherical): `ds² = -(1 - r_s/r) dt² + dr²/(1 - r_s/r) + r² dΩ²`, `r_s = 2M`.
* Eddington–Finkelstein `(v, r, θ, φ)`: same catalogue, eq. (eddFinkel):
  `ds² = -(1 - r_s/r) dv² + 2 dv dr + r² dΩ²`, with `v = t + r + r_s ln(r - r_s)`.
  The outgoing form uses `u = t - r - r_s ln|r - r_s|` and `-2 du dr`. Both are the case
  `ε = ±1` of `gEF M ε`; matrix entries are `g_{vr} = g_{rv} = ε` (not `2ε`).

Real `log` satisfies `log x = log |x|`, so `toEF` is the usual `r + 2M ln|r - 2M|` on both sides
of `r = 2M`.
-/

open Real

namespace ExactVacuumAtlas.Schwarzschild

/-- Standard Schwarzschild metric `g_{ij}` in `(t, r, θ, φ)`. -/
noncomputable def gStd (M : ℝ) : Metric 4
  | 0, 0 => fun x => -(1 - 2 * M / x 1)
  | 1, 1 => fun x => 1 / (1 - 2 * M / x 1)
  | 2, 2 => fun x => x 1 ^ 2
  | 3, 3 => fun x => x 1 ^ 2 * sin (x 2) ^ 2
  | _, _ => fun _ => 0

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

/-- Domain of the standard chart: `r > 0`, `r ≠ 2M`, `0 < θ < π`; `t, φ` arbitrary. For `M > 0`
it has two components (exterior and interior); it never contains `r = 2M`. -/
def domStd (M : ℝ) : Set (Pt 4) := {x | 0 < x 1 ∧ x 1 ≠ 2 * M ∧ 0 < x 2 ∧ x 2 < π}

/-- Eddington–Finkelstein family in `(w, r, θ, φ)`: `ε = 1` ingoing (`w = v`),
`ε = -1` outgoing (`w = u`). -/
noncomputable def gEF (M ε : ℝ) : Metric 4
  | 0, 0 => fun x => -(1 - 2 * M / x 1)
  | 0, 1 => fun _ => ε
  | 1, 0 => fun _ => ε
  | 2, 2 => fun x => x 1 ^ 2
  | 3, 3 => fun x => x 1 ^ 2 * sin (x 2) ^ 2
  | _, _ => fun _ => 0

/-- Candidate inverse for `gEF` (valid when `ε² = 1`). -/
noncomputable def giEF (M ε : ℝ) : Metric 4
  | 0, 1 => fun _ => ε
  | 1, 0 => fun _ => ε
  | 1, 1 => fun x => 1 - 2 * M / x 1
  | 2, 2 => fun x => 1 / x 1 ^ 2
  | 3, 3 => fun x => 1 / (x 1 ^ 2 * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Domain of the EF charts: `r > 0`, `0 < θ < π`; `w, φ` arbitrary. Contains `r = 2M` when `M > 0`
(for `M ≤ 0` there is no such point with `r > 0`). -/
def domEF : Set (Pt 4) := {x | 0 < x 1 ∧ 0 < x 2 ∧ x 2 < π}

/-- Standard → EF: `w = t + ε (r + 2M log (r - 2M))`, other coordinates unchanged. -/
noncomputable def toEF (M ε : ℝ) (x : Pt 4) : Pt 4 :=
  ![x 0 + ε * (x 1 + 2 * M * log (x 1 - 2 * M)), x 1, x 2, x 3]

/-- EF → standard: `t = w - ε (r + 2M log (r - 2M))`. -/
noncomputable def fromEF (M ε : ℝ) (y : Pt 4) : Pt 4 :=
  ![y 0 - ε * (y 1 + 2 * M * log (y 1 - 2 * M)), y 1, y 2, y 3]

end ExactVacuumAtlas.Schwarzschild
Source
Müller–Grave catalogue eq. schwarzschildSpherical (r_s = 2M, G = c = 1); Müller–Grave catalogue eq. eddFinkel: ds² = −(1−r_s/r) dv² + 2 dv dr + r² dΩ², v = t + r + r_s ln(r − r_s); outgoing form with u = t − r − r_s ln|r − r_s|; Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Schwarzschild/Defs.lean (source module Atlas.Schwarzschild.Defs, file sha256 ea0aee6cb47c8ae637aea0597c62cb9c3b90585a0ec28f54647231f9f8e27fd1; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Schwarzschild_Defs.lean, sha256 dbcb2947e61002e59457a733fbfc3c88fd2a6ba37994edc04af0a4804522242e)
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