Prove2Me

Atlas Isotropic CartMaps

Definition
Atlas_Isotropic_CartMaps

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

exact-vacuum-atlasgeneral-relativitylean4mathlib

toCart x = (t, ρ sin θ cos φ, ρ sin θ sin φ, ρ cos θ); rxy y = √(x² + y²); domIsoChart M = domIso M ∩ {−π < φ < π}; domCartSlit M = {ρ > 0, ρ ≠ M/2, r_xy + x > 0} (the natural domain intersected with "off the closed half-plane y = 0, x ≤ 0"); jacCart x = the 4×4 Jacobian of toCart (rows t, x, y, z; columns t, ρ, θ, φ), det = ρ² sin θ.

Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Isotropic/CartMaps.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.Iso.domCartSlit, ExactVacuumAtlas.Schwarzschild.Iso.domIsoChart, ExactVacuumAtlas.Schwarzschild.Iso.jacCart, ExactVacuumAtlas.Schwarzschild.Iso.rxy, ExactVacuumAtlas.Schwarzschild.Iso.toCart
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Isotropic_Defs
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
set_option maxHeartbeats 4000000

/-!
# Isotropic Schwarzschild: spherical → Cartesian map, its Jacobian and the pull-back (ATLAS-II)

`toCart (t, ρ, θ, φ) = (t, ρ sinθ cosφ, ρ sinθ sinφ, ρ cosθ)` on the chart domain
`domIsoChart M = domIso M ∩ {−π < φ < π}`, with image in the slit domain
`domCartSlit M = {ρ > 0, ρ ≠ M/2, r_xy + x > 0}` (`r_xy = √(x² + y²)`; `r_xy + x > 0` is exactly
"off the closed half-plane `y = 0, x ≤ 0`"). Explicit Jacobian `jacCart` with `det = ρ² sinθ`, and the
pull-back identity `Jᵀ gIsoCart(toCart x) J = gIso x`. The inverse map lives in `CartChart.lean`.
-/

open Real Matrix
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild

namespace ExactVacuumAtlas.Schwarzschild.Iso

/-- Spherical → Cartesian. -/
noncomputable def toCart (x : Pt 4) : Pt 4 :=
  ![x 0, x 1 * sin (x 2) * cos (x 3), x 1 * sin (x 2) * sin (x 3), x 1 * cos (x 2)]

/-- `r_xy = √(x² + y²)`. -/
noncomputable def rxy (y : Pt 4) : ℝ := Real.sqrt (y 1 ^ 2 + y 2 ^ 2)

/-- Spherical chart domain `domIso M ∩ {−π < φ < π}`. -/
def domIsoChart (M : ℝ) : Set (Pt 4) := {x | x ∈ domIso M ∧ -π < x 3 ∧ x 3 < π}

/-- Cartesian slit domain: `ρ > 0`, `ρ ≠ M/2`, `r_xy + x > 0`. -/
def domCartSlit (M : ℝ) : Set (Pt 4) := {y | 0 < rho y ∧ rho y ≠ M / 2 ∧ 0 < rxy y + y 1}

/-- Jacobian of `toCart` (rows `t, x, y, z`; columns `t, ρ, θ, φ`). -/
noncomputable def jacCart (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, 0, 0, 0;
     0, sin (x 2) * cos (x 3), x 1 * cos (x 2) * cos (x 3), -(x 1 * sin (x 2) * sin (x 3));
     0, sin (x 2) * sin (x 3), x 1 * cos (x 2) * sin (x 3), x 1 * sin (x 2) * cos (x 3);
     0, cos (x 2), -(x 1 * sin (x 2)), 0]

end ExactVacuumAtlas.Schwarzschild.Iso
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Isotropic/CartMaps.lean; SHA-256 19aa01acaa7bc462019d7acb24320f1f0b760ab3f42a9833c3f2e0404b8b12b1. 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