Prove2Me

Jacobian of the spherical-to-Cartesian map, entrywise as genuine derivatives

Proved
ExactVacuumAtlas.Minkowski.R4.hasDerivAt_toCart

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

coordinate-geometrycoordinate-transformationderivativeexact-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

J(x)=(10000sin⁡θcos⁡φrcos⁡θcos⁡φ−rsin⁡θsin⁡φ0sin⁡θsin⁡φrcos⁡θsin⁡φrsin⁡θcos⁡φ0cos⁡θ−rsin⁡θ0).J(x)=\begin{pmatrix}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\end{pmatrix}.

For every x∈R4x\in\mathbb R^4 and all indices k,i∈{0,1,2,3}k,i\in\{0,1,2,3\}, the one-variable function u↦Φ(x[xi:=u])ku\mapsto\Phi(x[x_i:=u])_k has derivative J(x)kiJ(x)_{ki} at u=xiu=x_i.

Jacobian obligation of relation R4, stated without any domain restriction; det⁡J=r2sin⁡θ\det J=r^2\sin\theta.

Formalization Note Row kk is the output component, column ii the input coordinate; each entry is a HasDerivAt statement.

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.hasDerivAt_toCart (x : Pt 4) (k i : Fin 4) :
    HasDerivAt (fun u => toCart (Function.update x i u) k) (jac x k i) (x i) := 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#L330-L392 (module Atlas.Minkowski.R4, file sha256 a1fc97dfc0dd15a14ffbb8dfbee1cfe1421e5f3119a6b8607bb683d8caafc495; uploaded stub = platform_mirror/Theorems/Thm_ExactVacuumAtlas_Minkowski_R4_hasDerivAt_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