Prove2Me

Atlas Schwarzschild PGCertParts

Definition
Atlas_Schwarzschild_PGCertParts

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

exact-vacuum-atlasgeneral-relativitylean4mathlib

frameE M ε x: the frame matrix entries — (0,0) = 1, (1,0) = −ε q, (1,1) = 1, (2,2) = 1/r, (3,3) = 1/(r sin θ), others 0; frame M ε x = Matrix.of (frameE M ε x). Columns e₀ = ∂_T − ε q ∂_r, e₁ = ∂_r, e₂ = r⁻¹∂_θ, e₃ = (r sin θ)⁻¹∂_φ; the certificate proves Eᵀ g E = diag(−1,1,1,1) on all of domEF for M ≥ 0 and ε² = 1, including its regular-coordinate points with r = 2M when M > 0 (no square root of 1 − 2M/r is involved). Generated by scripts/gen_pg_cert.py.

Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Schwarzschild/PGCertParts.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.PG.frame, ExactVacuumAtlas.Schwarzschild.PG.frameE
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_Schwarzschild_Defs
import Definitions.Def_Atlas_Schwarzschild_Domain
import Definitions.Def_Atlas_Schwarzschild_PGDefs
set_option maxHeartbeats 4000000
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

/-! Generated by `scripts/gen_pg_cert.py`. Do not edit by hand. -/

open Real
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.Schwarzschild
namespace ExactVacuumAtlas.Schwarzschild.PG
variable (M ε : ℝ)

/-- Explicit orthonormal frame for `gPG` (valid on all of `domEF`, including `r = 2M`):
columns `e₀ = ∂_T − ε q ∂_r`, `e₁ = ∂_r`, `e₂ = r⁻¹ ∂_θ`, `e₃ = (r sin θ)⁻¹ ∂_φ`. -/
noncomputable def frameE (x : Pt 4) : Fin 4 → Fin 4 → ℝ
  | 0, 0 => 1
  | 1, 0 => -ε * qf M (x 1)
  | 1, 1 => 1
  | 2, 2 => 1 / (x 1)
  | 3, 3 => 1 / ((x 1) * sin (x 2))
  | _, _ => 0

noncomputable def frame (x : Pt 4) : Matrix (Fin 4) (Fin 4) ℝ := Matrix.of (frameE M ε x)

end ExactVacuumAtlas.Schwarzschild.PG
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Schwarzschild/PGCertParts.lean; SHA-256 ad7b92882aa3b758b883597632c3b12fa5869b9063a4746f8c22464ee27854ab. 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

  • Endorsed by Shuze Chen · Oct 18, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph