Prove2Me

Spherical chart: the Cartesian map is inverted on the chart

Proved
ExactVacuumAtlas.Minkowski.R4.fromCart_toCart

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

coordinate-geometrycoordinate-transformationexact-vacuum-atlasgeneral-relativityminkowski-spacespherical-coordinates

Let Φ(t,r,θ,φ)=(t, rsin⁡θcos⁡φ, rsin⁡θsin⁡φ, rcos⁡θ)\Phi(t,r,\theta,\varphi)=(t,\ r\sin\theta\cos\varphi,\ r\sin\theta\sin\varphi,\ r\cos\theta) and Ψ\Psi the inverse map of bundle Atlas_Minkowski_R4 (ρ=x2+y2+z2\rho=\sqrt{x^2+y^2+z^2}, θ=arccos⁡(z/ρ)\theta=\arccos(z/\rho), φ=π+2arctan⁡(−y/(x2+y2−x))\varphi=\pi+2\arctan\big(-y/(\sqrt{x^2+y^2}-x)\big)). For every x=(t,r,θ,φ)x=(t,r,\theta,\varphi) in the chart U={r>0, 0<θ<π, 0<φ<2π}U=\{r>0,\ 0<\theta<\pi,\ 0<\varphi<2\pi\},

Ψ(Φ(x))=x.\Psi(\Phi(x))=x.

Left-inverse obligation of relation R4.

Preamble
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Minkowski_Cartesian
import Definitions.Def_Atlas_Minkowski_R4
import Definitions.Def_Atlas_Minkowski_Spherical
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
open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Minkowski
open ExactVacuumAtlas
open ExactVacuumAtlas.Minkowski
open ExactVacuumAtlas.Minkowski.R4
set_option maxHeartbeats 4000000
set_option linter.unusedSimpArgs false
Formal statement
theorem ExactVacuumAtlas.Minkowski.R4.fromCart_toCart {x : Pt 4} (hx : x ∈ domChart) : fromCart (toCart x) = x := by sorry
Source
elementary spherical coordinates on R^3 (standard); Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Minkowski/R4.lean#L155-L210 (module Atlas.Minkowski.R4, file sha256 a1fc97dfc0dd15a14ffbb8dfbee1cfe1421e5f3119a6b8607bb683d8caafc495; uploaded stub = platform_mirror/Theorems/Thm_ExactVacuumAtlas_Minkowski_R4_fromCart_toCart.lean)
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