Schwarzschild: equatorial reference point

Definition

Atlas_Schwarzschild_Domain

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

coordinate-geometrydomainexact-vacuum-atlasgeneral-relativityschwarzschild-metric

The point $(0,\rho,\pi/2,0)\in\mathbb R^4$ for a real $\rho$ (equatorPt), on the equator at radius $\rho$ .

Used to show the Schwarzschild and Minkowski domains are nonempty and to exhibit the $r=2M$ coverage witness.

Formalization Note Definition bundle generated by skeleton subtraction from the source module Atlas.Schwarzschild.Domain; declarations: ExactVacuumAtlas.Schwarzschild.equatorPt. No theorem is proved inside the bundle; it imports only Mathlib and other Definitions.Def_* bundles.

Definition code

-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Schwarzschild/Domain.lean
-- definition bundle: kept ExactVacuumAtlas.Schwarzschild.equatorPt
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Schwarzschild_Defs
/-! # Elementary facts about the Schwarzschild coordinate domains -/

open Real

namespace ExactVacuumAtlas.Schwarzschild

/-- A reference point on the equator at radius `ρ`. -/
noncomputable def equatorPt (ρ : ℝ) : Pt 4 := ![0, ρ, π / 2, 0]

end ExactVacuumAtlas.Schwarzschild

Source

Müller–Grave catalogue eq. schwarzschildSpherical (r_s = 2M, G = c = 1); Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Schwarzschild/Domain.lean (source module Atlas.Schwarzschild.Domain, file sha256 8f6da091014e8dd9f976fc71cc47fe8dd0266fa39e25a359d3663b743c579208; uploaded bundle = platform_mirror/Definitions/Def_Atlas_Schwarzschild_Domain.lean, sha256 1a38a124991de959ad11432c4ac16f0978fc439a7d0568be147b622664c2fae3)

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by He Wang · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph