Prove2Me

NQ14 (ST03 metric with charge 2): closed form of the radial function rH

Proved
ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rH_eq

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

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

NQ14 (ST03 metric with charge 2): closed form of the radial function rH

For candidate NQ14 (ST03 metric with charge 2): for every r ∈ radR, the transcribed radial function rH 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_NQ14_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.NQ14
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.NQ14.rH_eq (r : ℝ) (hr : r ∈ radR) : rH r = ((1:ℝ) * 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/NQ14/Defs.lean#L128-L134; SHA-256 414b38f26c883112e2d1e08ed57a5a8b68ed097c41c3b20cf6eb280987bfac30. 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