R4 data: spherical chart, Cartesian image, the maps and the Jacobian

Definition

Atlas_Minkowski_R4

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

cartesian-coordinatescoordinate-geometrycoordinate-transformationexact-vacuum-atlasgeneral-relativityminkowski-spacespherical-coordinates

The chart $U=\{(t,r,\theta,\varphi):\ r>0,\ 0<\theta<\pi,\ 0<\varphi<2\pi\}$ (domChart); the map $\Phi(t,r,\theta,\varphi)=(t,\ r\sin\theta\cos\varphi,\ r\sin\theta\sin\varphi,\ r\cos\theta)$ (toCart); the image $V=\{(t,x,y,z):\ \neg(y=0\wedge x\ge0)\}$ , the complement of the closed half-plane $\{y=0,x\ge0\}$ (imgCart); the inverse $\Psi(t,x,y,z)=\big(t,\ \rho,\ \arccos(z/\rho),\ \pi+2\arctan\frac{-y}{\sqrt{x^2+y^2}-x}\big)$ with $\rho=\sqrt{x^2+y^2+z^2}$ (fromCart); and the Jacobian matrix $J$ of $\Phi$ with rows $(1,0,0,0)$ , $(0,\sin\theta\cos\varphi,r\cos\theta\cos\varphi,-r\sin\theta\sin\varphi)$ , $(0,\sin\theta\sin\varphi,r\cos\theta\sin\varphi,r\sin\theta\cos\varphi)$ , $(0,\cos\theta,-r\sin\theta,0)$ (jac).

Data of relation R4 on one chart; $\varphi\sim\varphi+2\pi$ is not modelled.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Minkowski.R4; declarations: ExactVacuumAtlas.Minkowski.R4.domChart, ExactVacuumAtlas.Minkowski.R4.fromCart, ExactVacuumAtlas.Minkowski.R4.imgCart, ExactVacuumAtlas.Minkowski.R4.jac, ExactVacuumAtlas.Minkowski.R4.toCart. 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/R4.lean
-- definition bundle: kept ExactVacuumAtlas.Minkowski.R4.domChart, ExactVacuumAtlas.Minkowski.R4.fromCart, ExactVacuumAtlas.Minkowski.R4.imgCart, ExactVacuumAtlas.Minkowski.R4.jac, ExactVacuumAtlas.Minkowski.R4.toCart
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_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
set_option maxHeartbeats 4000000
set_option linter.unusedSimpArgs false

/-!
# R4: Minkowski Cartesian ↔ spherical — the actual coordinate map on a chart

Chart `domChart = {r > 0, 0 < θ < π, 0 < φ < 2π}` ⊆ `domSph`. The map
`toCart (t, r, θ, φ) = (t, r sin θ cos φ, r sin θ sin φ, r cos θ)` is a `C^∞` bijection of
`domChart` onto `imgCart = ℝ⁴ ∖ {y = 0, x ≥ 0}` (the closed half-plane slit, which contains the
`z`-axis), with `C^∞` inverse `fromCart`. The Jacobian `jac` has genuine-derivative entries,
`det jac = r² sin θ`, and the pull-back identity `jacᵀ · η · jac = gSph` holds on the chart.
`φ ~ φ + 2π` is not formalised; this is one chart.
-/

open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Minkowski

namespace ExactVacuumAtlas.Minkowski.R4

/-- Spherical chart: `r > 0`, `0 < θ < π`, `0 < φ < 2π`. -/
def domChart : Set (Pt 4) := {x | 0 < x 1 ∧ 0 < x 2 ∧ x 2 < π ∧ 0 < x 3 ∧ x 3 < 2 * π}

/-- 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)]

/-- Image of the chart: complement of the closed half-plane `{y = 0, x ≥ 0}`. -/
def imgCart : Set (Pt 4) := {y | ¬ (y 2 = 0 ∧ 0 ≤ y 1)}

/-- Cartesian → spherical on `imgCart`. -/
noncomputable def fromCart (y : Pt 4) : Pt 4 :=
  ![y 0, √(y 1 ^ 2 + y 2 ^ 2 + y 3 ^ 2),
    arccos (y 3 / √(y 1 ^ 2 + y 2 ^ 2 + y 3 ^ 2)),
    π + 2 * arctan (-(y 2) / (√(y 1 ^ 2 + y 2 ^ 2) - y 1))]

/-! ## Domains -/

/-! ## Maps between the domains -/

/-! ## Smoothness -/

/-! ## Jacobian -/

/-- Jacobian of `toCart`: row `k` = output component, column `i` = input coordinate. -/
noncomputable def jac (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]

/-! ## Pull-back -/

end ExactVacuumAtlas.Minkowski.R4

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 (source module Atlas.Minkowski.R4, file sha256 a1fc97dfc0dd15a14ffbb8dfbee1cfe1421e5f3119a6b8607bb683d8caafc495; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Minkowski_R4.lean, sha256 07dbdf4cce66ed5735add8db24c6750ff2cb595a7a68a98918d8d6172b1f01d3)

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