Atlas_Isotropic_Defs

Definition

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

exact-vacuum-atlasgeneral-relativitylean4mathlib

Coordinates (t, ρ, θ, φ); Bf M ρ = 1 + M/(2ρ), Af M ρ = (1 − M/(2ρ))/(1 + M/(2ρ)). gIso M = diag(−A², B⁴, B⁴ρ², B⁴ρ² sin²θ), giIso M the reciprocal diagonal (written independently; checked in the certificate). Domains: domIso M = {ρ > 0, ρ ≠ M/2, 0 < θ < π}; domIsoOut M = {M/2 < ρ, 0 < ρ, 0 < θ < π}; domIsoIn M = {0 < ρ < M/2, 0 < θ < π}; domStdExt M = {2M < r, 0 < r, 0 < θ < π}. Radial map rad M ρ = ρ(1 + M/(2ρ))² with the two inverse branches radInvOut M r = (r − M + √(r(r − 2M)))/2 and radInvIn M r = (r − M − √(r(r − 2M)))/2; toStd M x = (t, rad M ρ, θ, φ), fromStdOut/fromStdIn the corresponding inverse maps; jacIso M x = diag(1, 1 − M²/(4ρ²), 1, 1), jacIsoInv its reciprocal (valid for ρ ≠ 0, ±M/2). Cartesian form: rho x = √(x² + y² + z²), gIsoCart M = diag(−A(ρ)², B(ρ)⁴, B(ρ)⁴, B(ρ)⁴), giIsoCart the reciprocal, domIsoCart M = {ρ > 0, ρ ≠ M/2}. Lean conventions: division by zero is 0, so Af M 0 = 1 and the radial Jacobian entry at ρ = 0 is 1 — these points are excluded from every domain; Real.sqrt of a negative number is 0 — never used, since r(r − 2M) ≥ 0 on domStdExt. For M > 0, ρ = M/2 (A = 0) is a chart degeneracy and is excluded; for M = 0 it coincides with the excluded origin.

中文导读。 isotropic 数据：B = 1 + M/2ρ、A = (1 − M/2ρ)/B、球坐标与 Cartesian 度规及候选逆、域（完整域、内外支、r > 2M）、径向映射 r = ρ(1 + M/2ρ)² 与两支逆 ρ±、Jacobian diag(1, 1 − M²/4ρ², 1, 1)。

Definition code

-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Isotropic/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.Iso.Af, ExactVacuumAtlas.Schwarzschild.Iso.Bf, ExactVacuumAtlas.Schwarzschild.Iso.domIso, ExactVacuumAtlas.Schwarzschild.Iso.domIsoCart, ExactVacuumAtlas.Schwarzschild.Iso.domIsoIn, ExactVacuumAtlas.Schwarzschild.Iso.domIsoOut, ExactVacuumAtlas.Schwarzschild.Iso.domStdExt, ExactVacuumAtlas.Schwarzschild.Iso.fromStdIn, ExactVacuumAtlas.Schwarzschild.Iso.fromStdOut, ExactVacuumAtlas.Schwarzschild.Iso.gIso, ExactVacuumAtlas.Schwarzschild.Iso.gIsoCart, ExactVacuumAtlas.Schwarzschild.Iso.giIso, ExactVacuumAtlas.Schwarzschild.Iso.giIsoCart, ExactVacuumAtlas.Schwarzschild.Iso.jacIso, ExactVacuumAtlas.Schwarzschild.Iso.jacIsoInv, ExactVacuumAtlas.Schwarzschild.Iso.rad, ExactVacuumAtlas.Schwarzschild.Iso.radInvIn, ExactVacuumAtlas.Schwarzschild.Iso.radInvOut, ExactVacuumAtlas.Schwarzschild.Iso.rho, ExactVacuumAtlas.Schwarzschild.Iso.toStd
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
/-!
# Isotropic Schwarzschild: data, domains, radial map and its two inverse branches (ATLAS-II)

Coordinates `(t, ρ, θ, φ)`, `G = c = 1`, signature `(−,+,+,+)`; `B = 1 + M/(2ρ)`, `A = (1 − M/(2ρ))/B`;

  `ds² = −A² dt² + B⁴ (dρ² + ρ² dθ² + ρ² sin²θ dφ²)`   (Müller–Grave arXiv:0904.4184v3 §2.2.3).

Cartesian form: `ds² = −A² dt² + B⁴ (dx² + dy² + dz²)`, `ρ = √(x² + y² + z²)`.

Relation to the standard chart: `r = ρ (1 + M/(2ρ))² = (2ρ + M)²/(4ρ)`, with the two inverse branches
`ρ± = (r − M ± √(r(r − 2M)))/2`. For `M > 0` the outer branch `ρ > M/2` and the inner branch
`0 < ρ < M/2` are **each** mapped onto `r > 2M`; `ρ = M/2` (`A = 0`) is a degeneracy of the chart and is
not certified; the inner branch is **not** the interior `r < 2M`, and the union of the two branches is
**not** a single bijection onto anything. `M = 0` is Minkowski in spherical coordinates (`A = B = 1`).

This file contains data and elementary algebra only (no certificate).
-/

open Real

namespace ExactVacuumAtlas.Schwarzschild.Iso

/-- `B(ρ) = 1 + M/(2ρ)`. -/
noncomputable def Bf (M ρ : ℝ) : ℝ := 1 + M / (2 * ρ)

/-- `A(ρ) = (1 − M/(2ρ)) / (1 + M/(2ρ))`. -/
noncomputable def Af (M ρ : ℝ) : ℝ := (1 - M / (2 * ρ)) / (1 + M / (2 * ρ))

/-- Spherical isotropic metric. -/
noncomputable def gIso (M : ℝ) : Metric 4
  | 0, 0 => fun x => -(Af M (x 1) ^ 2)
  | 1, 1 => fun x => Bf M (x 1) ^ 4
  | 2, 2 => fun x => Bf M (x 1) ^ 4 * x 1 ^ 2
  | 3, 3 => fun x => Bf M (x 1) ^ 4 * x 1 ^ 2 * sin (x 2) ^ 2
  | _, _ => fun _ => 0

/-- Candidate inverse (written independently). -/
noncomputable def giIso (M : ℝ) : Metric 4
  | 0, 0 => fun x => -(1 / Af M (x 1) ^ 2)
  | 1, 1 => fun x => 1 / Bf M (x 1) ^ 4
  | 2, 2 => fun x => 1 / (Bf M (x 1) ^ 4 * x 1 ^ 2)
  | 3, 3 => fun x => 1 / (Bf M (x 1) ^ 4 * x 1 ^ 2 * sin (x 2) ^ 2)
  | _, _ => fun _ => 0

/-- Full spherical isotropic domain `ρ > 0`, `ρ ≠ M/2`, `0 < θ < π`. -/
def domIso (M : ℝ) : Set (Pt 4) := {x | 0 < x 1 ∧ x 1 ≠ M / 2 ∧ 0 < x 2 ∧ x 2 < π}

/-- Outer branch `ρ > M/2` (and `ρ > 0`). -/
def domIsoOut (M : ℝ) : Set (Pt 4) := {x | M / 2 < x 1 ∧ 0 < x 1 ∧ 0 < x 2 ∧ x 2 < π}

/-- Inner branch `0 < ρ < M/2`. -/
def domIsoIn (M : ℝ) : Set (Pt 4) := {x | 0 < x 1 ∧ x 1 < M / 2 ∧ 0 < x 2 ∧ x 2 < π}

/-- Exterior region of the standard chart, `r > 2M` (and `r > 0`). -/
def domStdExt (M : ℝ) : Set (Pt 4) := {x | 2 * M < x 1 ∧ 0 < x 1 ∧ 0 < x 2 ∧ x 2 < π}

/-- Radial map `r(ρ) = ρ (1 + M/(2ρ))²`. -/
noncomputable def rad (M ρ : ℝ) : ℝ := ρ * (1 + M / (2 * ρ)) ^ 2

/-- Outer inverse branch `ρ₊(r) = (r − M + √(r(r − 2M)))/2`. -/
noncomputable def radInvOut (M r : ℝ) : ℝ := (r - M + Real.sqrt (r * (r - 2 * M))) / 2

/-- Inner inverse branch `ρ₋(r) = (r − M − √(r(r − 2M)))/2`. -/
noncomputable def radInvIn (M r : ℝ) : ℝ := (r - M - Real.sqrt (r * (r - 2 * M))) / 2

/-- Isotropic → standard, `(t, ρ, θ, φ) ↦ (t, r(ρ), θ, φ)`. -/
noncomputable def toStd (M : ℝ) (x : Pt 4) : Pt 4 := ![x 0, rad M (x 1), x 2, x 3]

noncomputable def fromStdOut (M : ℝ) (y : Pt 4) : Pt 4 := ![y 0, radInvOut M (y 1), y 2, y 3]

noncomputable def fromStdIn (M : ℝ) (y : Pt 4) : Pt 4 := ![y 0, radInvIn M (y 1), y 2, y 3]

/-- Jacobian of `toStd`: `dr/dρ = 1 − M²/(4ρ²)`. -/
noncomputable def jacIso (M : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, 0, 0, 0; 0, 1 - M ^ 2 / (4 * x 1 ^ 2), 0, 0; 0, 0, 1, 0; 0, 0, 0, 1]

/-- Right inverse of `jacIso` (valid for `ρ ≠ 0`, `ρ ≠ ±M/2`). -/
noncomputable def jacIsoInv (M : ℝ) (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, 0, 0, 0; 0, 1 / (1 - M ^ 2 / (4 * x 1 ^ 2)), 0, 0; 0, 0, 1, 0; 0, 0, 0, 1]

/-! ### Cartesian form -/

/-- `ρ(x) = √(x² + y² + z²)` with `(x, y, z) = (x 1, x 2, x 3)`. -/
noncomputable def rho (x : Pt 4) : ℝ := Real.sqrt (x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2)

/-- Cartesian isotropic metric `−A(ρ)² dt² + B(ρ)⁴ (dx² + dy² + dz²)`. -/
noncomputable def gIsoCart (M : ℝ) : Metric 4
  | 0, 0 => fun x => -(Af M (rho x) ^ 2)
  | 1, 1 => fun x => Bf M (rho x) ^ 4
  | 2, 2 => fun x => Bf M (rho x) ^ 4
  | 3, 3 => fun x => Bf M (rho x) ^ 4
  | _, _ => fun _ => 0

noncomputable def giIsoCart (M : ℝ) : Metric 4
  | 0, 0 => fun x => -(1 / Af M (rho x) ^ 2)
  | 1, 1 => fun x => 1 / Bf M (rho x) ^ 4
  | 2, 2 => fun x => 1 / Bf M (rho x) ^ 4
  | 3, 3 => fun x => 1 / Bf M (rho x) ^ 4
  | _, _ => fun _ => 0

/-- Natural Cartesian domain: only `ρ = 0` and `ρ = M/2` removed (no axis or azimuthal cut). -/
def domIsoCart (M : ℝ) : Set (Pt 4) := {x | 0 < rho x ∧ rho x ≠ M / 2}

/-! ### Elementary algebra of the radial map -/

end ExactVacuumAtlas.Schwarzschild.Iso

Source

He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Isotropic/Defs.lean; SHA-256 3f92e15a444a4c96a42e80b16bf07e7a93b5e27f53720e1eb06cfd8535c2315a. Mathematical background: See mission/PHYSICS_BOUNDARY.md §A-F for registered definitions and literature references (Wald, Müller-Grave arXiv:0904.4184, Visser arXiv:0706.0622, Martel-Poisson gr-qc/0001069).

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by He Wang · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph