Atlas Schwarzschild PGRelation
DefinitionAtlas_Schwarzschild_PGRelationexact-vacuum-atlasgeneral-relativitylean4mathlib
jac M ε x = I + (ε/(1 + q)) E₀₁ (row 0 = output w, column 1 = input r; radial mixed entry ε/(1+q), det = 1) and jacInv M ε y = I − (ε/(1 + q)) E₀₁. Every entry is a genuine slice derivative (theorems hasDerivAt_pd_pgToEF / hasDerivAt_pd_pgFromEF, separate); jac · jacInv = 1. The module docstring (kept) describes the relation theorems, which are separate nodes.
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Schwarzschild/PGRelation.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.PG.jac, ExactVacuumAtlas.Schwarzschild.PG.jacInv
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_Core_Relation
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_Atlas_Schwarzschild_PGDefs
set_option maxHeartbeats 4000000
/-!
# Painlevé–Gullstrand ↔ Eddington–Finkelstein (same `ε`): the actual coordinate map on all of `domEF`
For `M ≥ 0`, `ε = ±1`, on the **whole** PG/EF domain `domEF = {r > 0, 0 < θ < π}` — the points
`r = 2M` (for `M > 0`) are *not* excluded — we prove:
* `pgToEF M ε : (T, r, θ, φ) ↦ (T + ε H_M(r), r, θ, φ)` and `pgFromEF M ε` are mutually inverse
(globally), map `domEF` onto itself (`bijOn`), and are `C^∞` on `domEF`;
* `H_M' = 1/(1 + q)` with `q = √(2M/r)` (`hasDerivAt_HPG`), so the Jacobian of `pgToEF` is the
explicit matrix `jac` with radial mixed entry `ε/(1 + q)` and `det jac = 1`; every entry is a
genuine `HasDerivAt` (`hasDerivAt_pd_pgToEF`);
* pull-back identity `jacᵀ · (gEF ∘ pgToEF) · jac = gPG` on `domEF` (`pullback`);
* the same in the other direction (`pgFromEF`, `jacInv`, `pullback_inv`).
Bundled as `relation_toEF : CoordRelation (gPG M ε) (gEF M ε) domEF domEF …` and `relation_fromEF`.
At `r = 2M` (`M > 0`): `q = 1`, `H' = 1/2`, `jac 0 1 = ε/2`, `det = 1` — nothing degenerates
(`PGSpecial.horizon_data`). The primitive `H_M` is one choice; the literature's `T = t + …` differs
from `w − ε H_M` by an additive constant that depends on the normalisation of the EF time (with the
source convention `Schwarzschild.toEF` the constant is `0`; `mission/PHYSICS_BOUNDARY.md` E4), which
does not affect the relation.
No statement is made through the standard chart (where `r ≠ 2M` would be forced).
-/
open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild
namespace ExactVacuumAtlas.Schwarzschild.PG
variable (M ε : ℝ)
/-! ### The primitive `H_M` -/
/-! ### Jacobians -/
/-- Jacobian `∂(pgToEF)ᵏ/∂xⁱ`; row `k`, column `i`. Radial mixed entry `ε/(1 + q)`. -/
noncomputable def jac (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
!![1, ε / (1 + qf M (x 1)), 0, 0;
0, 1, 0, 0;
0, 0, 1, 0;
0, 0, 0, 1]
/-- Jacobian of `pgFromEF`; radial mixed entry `−ε/(1 + q)`. -/
noncomputable def jacInv (y : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ :=
!![1, -ε / (1 + qf M (y 1)), 0, 0;
0, 1, 0, 0;
0, 0, 1, 0;
0, 0, 0, 1]
/-! ### Pull-back identities (on all of `domEF`, `r = 2M` included) -/
/-! ### Bundles -/
end ExactVacuumAtlas.Schwarzschild.PG
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Schwarzschild/PGRelation.lean; SHA-256 15a42669f14c3556d812be0667228c735019b13b898fa9b0552c54b35498feb7. 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.