Atlas_Schwarzschild_PGDefs
DefinitionCoordinates (T, r, θ, φ), G = c = 1, signature (−,+,+,+). qf M r = √(2M/r) (Mathlib Real.sqrt; used only with M ≥ 0, r > 0, where q² = 2M/r; the junk value on negative arguments is never used to extend a statement). gPG M ε: g_TT = −(1 − 2M/r), g_Tr = g_rT = ε q, g_rr = 1, g_θθ = r², g_φφ = r² sin²θ, else 0 — the line element −dT² + (dr + ε q dT)² + r² dΩ² (Martel–Poisson gr-qc/0001069 eqs. 2.6–2.7; Müller–Grave arXiv:0904.4184v3 PG subsection; the matrix entry g_Tr is half the literature cross term 2√(2M/r) dT dr). giPG M ε: ĝ^TT = −1, ĝ^Tr = ĝ^rT = ε q, ĝ^rr = 1 − 2M/r, ĝ^θθ = 1/r², ĝ^φφ = 1/(r² sin²θ), else 0 (checked in the certificate, valid for ε² = 1, M ≥ 0, r > 0). HPG M r = r − 2√(2M)√r + 4M log(√r + √(2M)), one primitive of 1/(1 + q) (H_0 = id); pgToEF M ε x = (T + ε H_M(r), r, θ, φ) and pgFromEF M ε y = (w − ε H_M(r), r, θ, φ). ε = +1 ingoing (Painlevé), −1 outgoing. Domain of use: domEF = {r > 0, 0 < θ < π}, which for M > 0 contains r = 2M (q = 1, g_TT = 0).
中文导读。 PG 目录数据：q = √(2M/r)（仅用于 M ≥ 0、r > 0）、度规 gPG（g_TT = −(1−2M/r)、g_Tr = εq、g_rr = 1、角块 r²、r² sin²θ）、候选逆 giPG、原函数 H_M（H_M′ = 1/(1+q)）、PG↔EF 映射 w = T ± H_M。
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Schwarzschild/PGDefs.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.PG.HPG, ExactVacuumAtlas.Schwarzschild.PG.gPG, ExactVacuumAtlas.Schwarzschild.PG.giPG, ExactVacuumAtlas.Schwarzschild.PG.pgFromEF, ExactVacuumAtlas.Schwarzschild.PG.pgToEF, ExactVacuumAtlas.Schwarzschild.PG.qf
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
/-!
# Schwarzschild in Painlevé–Gullstrand coordinates: catalogue data (independent of any proof)
Coordinates `(T, r, θ, φ)` indexed `0, 1, 2, 3`; units `G = c = 1`, signature `(-,+,+,+)`, mass `M`.
Line element (Martel–Poisson, arXiv:gr-qc/0001069, Painlevé–Gullstrand form; Müller–Grave,
*Catalogue of Spacetimes*, arXiv:0904.4184v3, Painlevé–Gullstrand subsection):
`ds² = −dT² + (dr + ε q dT)² + r² (dθ² + sin²θ dφ²)`, `q = √(2M/r)`, `ε² = 1`,
i.e. `g_TT = −(1 − 2M/r)`, `g_Tr = g_rT = ε q`, `g_rr = 1`, `g_θθ = r²`, `g_φφ = r² sin²θ`.
`ε = +1` is the ingoing (Painlevé) form, `ε = −1` the outgoing one. The literature form with
`2√(2M/r) dT dr` corresponds to the matrix entry `g_Tr = √(2M/r)` (half of the cross term).
**Modelling range.** `q = √(2M/r)` is used only for `M ≥ 0` and `r > 0`, where it is the real
square root of a nonnegative number and `q² = 2M/r` (`PG.qf_sq`). Mathlib's `Real.sqrt` returns
`0` on negative arguments; this junk value is *never* used to extend any statement to `M < 0`:
every PG certificate and relation carries the hypothesis `0 ≤ M` explicitly. The first-release
EF and standard certificates for arbitrary real `M` are unchanged.
Domain: the EF domain `domEF = {r > 0, 0 < θ < π}` (`T`, `φ` arbitrary), which for `M > 0`
contains the points with `r = 2M` (there `q = 1` and `g_TT = 0`; nothing degenerates).
-/
open Real
namespace ExactVacuumAtlas.Schwarzschild.PG
/-- The PG velocity atom `q(M, r) = √(2M/r)` (B3 class B notation wrapper around `Real.sqrt`). -/
noncomputable def qf (M r : ℝ) : ℝ := Real.sqrt (2 * M / r)
/-- Painlevé–Gullstrand metric `g_{ij}` in `(T, r, θ, φ)`, sign `ε`. -/
noncomputable def gPG (M ε : ℝ) : Metric 4
| 0, 0 => fun x => -(1 - 2 * M / x 1)
| 0, 1 => fun x => ε * qf M (x 1)
| 1, 0 => fun x => ε * qf M (x 1)
| 1, 1 => fun _ => 1
| 2, 2 => fun x => x 1 ^ 2
| 3, 3 => fun x => x 1 ^ 2 * sin (x 2) ^ 2
| _, _ => fun _ => 0
/-- Candidate inverse for `gPG` (checked, not assumed, in the certificate; valid when `ε² = 1`,
`M ≥ 0`, `r > 0`). -/
noncomputable def giPG (M ε : ℝ) : Metric 4
| 0, 0 => fun _ => -1
| 0, 1 => fun x => ε * qf M (x 1)
| 1, 0 => fun x => ε * qf M (x 1)
| 1, 1 => fun x => 1 - 2 * M / x 1
| 2, 2 => fun x => 1 / x 1 ^ 2
| 3, 3 => fun x => 1 / (x 1 ^ 2 * sin (x 2) ^ 2)
| _, _ => fun _ => 0
/-- Radial primitive relating PG time to the EF null coordinate:
`H_M(r) = r − 2√(2M)·√r + 4M·log(√r + √(2M))`. For `M ≥ 0`, `r > 0` its derivative is
`1/(1 + √(2M/r))` (`PG.hasDerivAt_HPG`); `H_0(r) = r`. It is one primitive of `1/(1+q)`; any
other differs by an additive constant, which does not affect the geometric relation. -/
noncomputable def HPG (M r : ℝ) : ℝ :=
r - 2 * Real.sqrt (2 * M) * Real.sqrt r + 4 * M * Real.log (Real.sqrt r + Real.sqrt (2 * M))
/-- PG → EF (same `ε`): `w = T + ε H_M(r)`, other coordinates unchanged. -/
noncomputable def pgToEF (M ε : ℝ) (x : Pt 4) : Pt 4 :=
![x 0 + ε * HPG M (x 1), x 1, x 2, x 3]
/-- EF → PG: `T = w − ε H_M(r)`. -/
noncomputable def pgFromEF (M ε : ℝ) (y : Pt 4) : Pt 4 :=
![y 0 - ε * HPG M (y 1), y 1, y 2, y 3]
end ExactVacuumAtlas.Schwarzschild.PG
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.