Prove2Me

ST03 (μ = 2, Q = 1, β = 1/3): closed form of the radial function rPhi

Proved
ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.ST03.rPhi_eq

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

einstein-maxwellexact-spacetime-atlas-viexact-vacuum-atlasfive-dimensional-gravitygeneral-relativity

ST03 (μ = 2, Q = 1, β = 1/3): closed form of the radial function rPhi

For candidate ST03 (μ = 2, Q = 1, β = 1/3): for every r ∈ radR, the transcribed radial function rPhi equals the factored closed form printed in the statement (factor polynomials f… are opaque names).

Scope. Exactly the hypotheses printed in the formal statement.

中文摘要 候选径向函数在 radR 上的因式化闭式。

Preamble
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Certificate
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_D_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Cand_ST03_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Defs
open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas
open ExactVacuumAtlas.EinsteinMaxwell
open ExactVacuumAtlas.EinsteinMaxwell.ES5
open ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand
open ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.ST03
set_option maxHeartbeats 8000000
set_option maxRecDepth 100000
set_option linter.unusedVariables false
set_option linter.unusedSimpArgs false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
Formal statement
theorem ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.ST03.rPhi_eq (r : ℝ) (hr : r ∈ radR) : rPhi r = ((-1/2:ℝ) / (r ^ 2)) := by sorry
Source
He Wang, Exact Spacetime Atlas VI: Five-Dimensional Einstein–Maxwell Certificates and Equal-Spin Radial Reduction. Local source, no public repository; commit 4a4048a; Atlas/EinsteinMaxwell/ES5/Cand/ST03/Defs.lean#L76-L82; SHA-256 cbbd87aeb4fd4a2e825cc5cbe2c56aaed785af23b07bab33fbae28d77f9c5cc0. Registered definitions: mission/PHYSICS_BOUNDARY.md (§N–§O); literature: R. C. Myers, M. J. Perry, Ann. Phys. 172 (1986) 304; F. R. Tangherlini, Nuovo Cimento 27 (1963) 636.
Human review

  • Endorsed by Shuze Chen · Oct 29, 2026

    Confirmed by the moderator at approval.

  • Endorsed by He Wang · Oct 29, 2026

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

View graph