VI-02 candidate MP02 (μ = 5, rotation constant −2/3): transcribed data

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Cand/MP02/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.candF, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.candG, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.candGi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.dom, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.fDl, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.fP, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.fS, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rA, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rB, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rD, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rH, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rPhi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rPsi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rW, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.rX, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.radR, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.xw
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_Defs
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

/-! Generated by `scripts/vi02_02/es5gen.py` from candidate `b02_mp_mu5_a2_3` (task `em5_equalspin_v1`). Do not edit.

Radial functions are transcribed verbatim from the candidate ASTs (`r = x 1`, parameters substituted). `f…` are opaque names for the integer factor polynomials of the denominators; `gN`/`giN` are normalised closed forms bound to `esMetric`/`esInverse` of the candidate on `dom` (`bind_g`, `bind_gi`). -/

open scoped ContDiff
open ExactVacuumAtlas ExactVacuumAtlas.EinsteinMaxwell ExactVacuumAtlas.EinsteinMaxwell.D
open ExactVacuumAtlas.EinsteinMaxwell.ES5

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02

noncomputable def fS (r : ℝ) : ℝ := ((9:ℝ) * r ^ 2 + (4:ℝ))

noncomputable def fDl (r : ℝ) : ℝ := ((81:ℝ) * r ^ 4 + (-333:ℝ) * r ^ 2 + (16:ℝ))

noncomputable def fP (r : ℝ) : ℝ := ((81:ℝ) * r ^ 4 + (72:ℝ) * r ^ 2 + (196:ℝ))

noncomputable def rB (r : ℝ) : ℝ := (((((r ^ 2) + ((-2/3:ℝ) ^ 2)) ^ 2) + (-((5:ℝ) * (r ^ 2)))) / ((((r ^ 2) + ((-2/3:ℝ) ^ 2)) ^ 2) + ((5:ℝ) * ((-2/3:ℝ) ^ 2))))
noncomputable def rD (r : ℝ) : ℝ := ((((r ^ 2) + ((-2/3:ℝ) ^ 2)) * (r ^ 2)) / ((((r ^ 2) + ((-2/3:ℝ) ^ 2)) ^ 2) + (-((5:ℝ) * (r ^ 2)))))
noncomputable def rA (r : ℝ) : ℝ := ((r ^ 2) + ((-2/3:ℝ) ^ 2))
noncomputable def rH (r : ℝ) : ℝ := (((((r ^ 2) + ((-2/3:ℝ) ^ 2)) ^ 2) + ((5:ℝ) * ((-2/3:ℝ) ^ 2))) / ((r ^ 2) + ((-2/3:ℝ) ^ 2)))
noncomputable def rW (r : ℝ) : ℝ := (((5:ℝ) * (-2/3:ℝ)) / ((((r ^ 2) + ((-2/3:ℝ) ^ 2)) ^ 2) + ((5:ℝ) * ((-2/3:ℝ) ^ 2))))
noncomputable def rPhi (r : ℝ) : ℝ := (0:ℝ)
noncomputable def rPsi (r : ℝ) : ℝ := (0:ℝ)
noncomputable def rX (r : ℝ) : ℝ := ((((r ^ 2) + ((-2/3:ℝ) ^ 2)) ^ 2) + (-((5:ℝ) * (r ^ 2))))

def radR : Set ℝ := {r | 0 < r ∧ rX r ≠ 0}
def dom : Set (Pt 5) := esDomain radR

noncomputable def candG : Metric 5 := esMetric rB rD rA rH rW
noncomputable def candGi : Metric 5 := esInverse rB rD rA rH rW

noncomputable def candF : TwoForm 5 := esFaraday rPhi rPsi

noncomputable def xw : Pt 5 := fun i => if i.val = 1 then (3:ℝ) else if i.val = 2 then (1/2:ℝ) else 0

end ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02

• 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).