VI-02 MP02 radial closed forms

-- Generated by scripts/release06/gen_platform_tree.py (RELEASE06; copy of release05, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/Cand/MP02/Reduced.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cA, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cA1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cA2, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cB, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cB1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cB2, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cD, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cD1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cD2, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cH, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cH1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cH2, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cPhi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cPhi1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cPhi2, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cPsi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cPsi1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cPsi2, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cW, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cW1, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02.cW2
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_MP02_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Cert
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Data
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Reduced
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Tables
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/es5red.py` from candidate `b02_mp_mu5_a2_3` (task `em5_equalspin_v1`). Do not edit.

Closed forms of the radial derivatives, the seven reduced equations, and the certificate via `Generic.es_certificate_iff`. -/

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

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.MP02

noncomputable def cB (r : ℝ) : ℝ := ((81:ℝ) * r ^ 4 + (-333:ℝ) * r ^ 2 + (16:ℝ)) / ((1:ℝ) * fP r)
noncomputable def cB1 (r : ℝ) : ℝ := ((65610:ℝ) * r ^ 5 + (58320:ℝ) * r ^ 3 + (-132840:ℝ) * r) / ((1:ℝ) * fP r ^ 2)
noncomputable def cB2 (r : ℝ) : ℝ := ((-15943230:ℝ) * r ^ 8 + (-18895680:ℝ) * r ^ 6 + (135419040:ℝ) * r ^ 4 + (62985600:ℝ) * r ^ 2 + (-26036640:ℝ)) / ((1:ℝ) * fP r ^ 3)

noncomputable def cD (r : ℝ) : ℝ := ((81:ℝ) * r ^ 4 + (36:ℝ) * r ^ 2) / ((1:ℝ) * fDl r)
noncomputable def cD1 (r : ℝ) : ℝ := ((-59778:ℝ) * r ^ 5 + (5184:ℝ) * r ^ 3 + (1152:ℝ) * r) / ((1:ℝ) * fDl r ^ 2)
noncomputable def cD2 (r : ℝ) : ℝ := ((14526054:ℝ) * r ^ 8 + (17806554:ℝ) * r ^ 6 + (-3709152:ℝ) * r ^ 4 + (1399680:ℝ) * r ^ 2 + (18432:ℝ)) / ((1:ℝ) * fDl r ^ 3)

noncomputable def cA (r : ℝ) : ℝ := ((9:ℝ) * r ^ 2 + (4:ℝ)) / ((9:ℝ))
noncomputable def cA1 (r : ℝ) : ℝ := ((2:ℝ) * r)
noncomputable def cA2 (r : ℝ) : ℝ := ((2:ℝ))

noncomputable def cH (r : ℝ) : ℝ := ((81:ℝ) * r ^ 4 + (72:ℝ) * r ^ 2 + (196:ℝ)) / ((9:ℝ) * fS r)
noncomputable def cH1 (r : ℝ) : ℝ := ((162:ℝ) * r ^ 5 + (144:ℝ) * r ^ 3 + (-328:ℝ) * r) / ((1:ℝ) * fS r ^ 2)
noncomputable def cH2 (r : ℝ) : ℝ := ((1458:ℝ) * r ^ 6 + (1944:ℝ) * r ^ 4 + (10584:ℝ) * r ^ 2 + (-1312:ℝ)) / ((1:ℝ) * fS r ^ 3)

noncomputable def cW (r : ℝ) : ℝ := ((-270:ℝ)) / ((1:ℝ) * fP r)
noncomputable def cW1 (r : ℝ) : ℝ := ((87480:ℝ) * r ^ 3 + (38880:ℝ) * r) / ((1:ℝ) * fP r ^ 2)
noncomputable def cW2 (r : ℝ) : ℝ := ((-35429400:ℝ) * r ^ 6 + (-28343520:ℝ) * r ^ 4 + (43040160:ℝ) * r ^ 2 + (7620480:ℝ)) / ((1:ℝ) * fP r ^ 3)

noncomputable def cPhi (r : ℝ) : ℝ := (0:ℝ)
noncomputable def cPhi1 (r : ℝ) : ℝ := (0:ℝ)
noncomputable def cPhi2 (r : ℝ) : ℝ := (0:ℝ)

noncomputable def cPsi (r : ℝ) : ℝ := (0:ℝ)
noncomputable def cPsi1 (r : ℝ) : ℝ := (0:ℝ)
noncomputable def cPsi2 (r : ℝ) : ℝ := (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).