Atlas Isotropic CartCover
DefinitionAtlas_Isotropic_CartCoverexact-vacuum-atlasgeneral-relativitylean4mathlib
reflX y = (t, −x, y, z) (self-inverse); rotC y = (t, y, z, x) and its inverse rotCInv y = (t, z, x, y) (cyclic relabellings); constant Jacobians jacReflX = diag(1, −1, 1, 1), jacRotC (row k = output component) and jacRotCInv = jacRotCᵀ; the preimage domains domRefl M = reflX⁻¹(domCartSlit M), domRot M = rotC⁻¹(domCartSlit M). ρ is invariant under all three maps and the spatial block of gIsoCart is B⁴·I, so these are isometries of the Cartesian isotropic metric.
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Isotropic/CartCover.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.Iso.domRefl, ExactVacuumAtlas.Schwarzschild.Iso.domRot, ExactVacuumAtlas.Schwarzschild.Iso.jacReflX, ExactVacuumAtlas.Schwarzschild.Iso.jacRotC, ExactVacuumAtlas.Schwarzschild.Iso.jacRotCInv, ExactVacuumAtlas.Schwarzschild.Iso.reflX, ExactVacuumAtlas.Schwarzschild.Iso.rotC, ExactVacuumAtlas.Schwarzschild.Iso.rotCInv
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_CartChart
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: covering the natural domain (ATLAS-II)
The slit certificate `cert_cart_slit` covers `r_xy + x > 0`. The closed half-plane `y = 0, x ≤ 0`
(which contains the `z`-axis) is covered by transporting the same certificate along two **linear**
symmetries of the Cartesian isotropic metric (`ρ` is invariant, the spatial block is `B⁴·I`):
* the reflection `reflX : x ↦ −x` (covers `r_xy − x > 0`, i.e. everything off `y = 0, x ≥ 0`);
* the cyclic relabelling `rotC : (x, y, z) ↦ (y, z, x)` (covers `√(y² + z²) + y > 0`, in particular
the `z`-axis minus the origin).
`domIsoCart_eq_union`: `{ρ > 0, ρ ≠ M/2}` is the union of the three open pieces;
`cert_cart`: the certificate on all of it (`VacuumCertificate.union`). No axis or azimuthal cut
remains; only `ρ = 0` and `ρ = M/2` are excluded.
-/
open Real Matrix
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild
namespace ExactVacuumAtlas.Schwarzschild.Iso
/-- Reflection `x ↦ −x` (self-inverse). -/
noncomputable def reflX (y : Pt 4) : Pt 4 := ![y 0, -(y 1), y 2, y 3]
/-- Cyclic relabelling `(x, y, z) ↦ (y, z, x)`. -/
noncomputable def rotC (y : Pt 4) : Pt 4 := ![y 0, y 2, y 3, y 1]
/-- Inverse relabelling `(x, y, z) ↦ (z, x, y)`. -/
noncomputable def rotCInv (y : Pt 4) : Pt 4 := ![y 0, y 3, y 1, y 2]
/-- Constant Jacobian of `reflX`. -/
def jacReflX : Matrix (Fin 4) (Fin 4) ℝ := !![1, 0, 0, 0; 0, -1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1]
/-- Constant Jacobian of `rotC` (row `k` = output component). -/
def jacRotC : Matrix (Fin 4) (Fin 4) ℝ := !![1, 0, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1; 0, 1, 0, 0]
/-- Its inverse (= transpose). -/
def jacRotCInv : Matrix (Fin 4) (Fin 4) ℝ := !![1, 0, 0, 0; 0, 0, 0, 1; 0, 1, 0, 0; 0, 0, 1, 0]
/-- The reflected and relabelled slit domains (preimages). -/
def domRefl (M : ℝ) : Set (Pt 4) := reflX ⁻¹' domCartSlit M
def domRot (M : ℝ) : Set (Pt 4) := rotC ⁻¹' domCartSlit M
variable {M : ℝ}
end ExactVacuumAtlas.Schwarzschild.Iso
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Isotropic/CartCover.lean; SHA-256 3d002dd52a357723e244eaf9df6b7c1eeb689295cf962455f5f09ab6ece860c8. 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.