Atlas Isotropic CartChart
DefinitionAtlas_Isotropic_CartChartexact-vacuum-atlasgeneral-relativitylean4mathlib
fromCart y = (t, ρ, arccos(z/ρ), 2 arctan(y/(r_xy + x))) with ρ = rho y, r_xy = rxy y. The half-angle form 2 arctan(y/(r_xy + x)) equals the azimuth in (−π, π) off the closed half-plane y = 0, x ≤ 0; arccos(z/ρ) ∈ (0, π) when |z| < ρ. Mathlib’s arccos is clamped outside [−1, 1] and arctan is total; the theorems use the map only on domCartSlit where |z/ρ| < 1 and r_xy + x > 0.
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Isotropic/CartChart.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.Iso.fromCart
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_Core_Relation
import Definitions.Def_Atlas_Isotropic_CartMaps
import Definitions.Def_Atlas_Isotropic_Defs
import Definitions.Def_Atlas_Minkowski_Spherical
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_Atlas_Transport_Connection
import Definitions.Def_Atlas_Transport_Curvature
import Definitions.Def_Atlas_Transport_MatrixCalc
set_option maxHeartbeats 4000000
/-!
# Isotropic Schwarzschild, Cartesian form: the slit chart and its transported certificate (ATLAS-II)
Inverse map on the slit domain `domCartSlit M = {ρ > 0, ρ ≠ M/2, r_xy + x > 0}`:
`fromCart (t, x, y, z) = (t, ρ, arccos (z/ρ), 2 arctan (y / (r_xy + x)))`,
(`2 arctan(y/(r_xy + x)) = φ` is the half-angle form of `atan2`, smooth off the closed half-plane
`y = 0, x ≤ 0`). `relation_sph_cart` is the first-release bundle `CoordRelation (gIso M) (gIsoCart M)
(domIsoChart M) (domCartSlit M) toCart fromCart jacCart`; `cert_cart_slit` transports the spherical
isotropic certificate to the Cartesian slit domain through the inverse relation
(`CoordRelation.inverse`) and the transport theorem. Coverage of the remaining Cartesian points
(the half-plane, hence the `z`-axis) is in `CartCover.lean`.
-/
open Real Matrix
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild
namespace ExactVacuumAtlas.Schwarzschild.Iso
/-- Cartesian → spherical on the slit domain. -/
noncomputable def fromCart (y : Pt 4) : Pt 4 :=
![y 0, rho y, Real.arccos (y 3 / rho y), 2 * Real.arctan (y 2 / (rxy y + y 1))]
/-! ### Elementary facts about `rho`, `rxy` -/
variable {M : ℝ}
/-! ### Mutual inverses -/
/-! ### Smoothness of the inverse map -/
/-! ### The relation and the transported certificate -/
end ExactVacuumAtlas.Schwarzschild.Iso
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Isotropic/CartChart.lean; SHA-256 a978cca33484092eed822c5786ba958ae7ad983e09ca84ea1c69e67017f2162e. 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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.