VI-02 candidate MP01 (μ = 3, a = 1/2): transcribed data

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

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

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

noncomputable def fP (r : ℝ) : ℝ := ((16:ℝ) * r ^ 4 + (8:ℝ) * r ^ 2 + (13:ℝ))

noncomputable def rB (r : ℝ) : ℝ := (((((r ^ 2) + ((1/2:ℝ) ^ 2)) ^ 2) + (-((3:ℝ) * (r ^ 2)))) / ((((r ^ 2) + ((1/2:ℝ) ^ 2)) ^ 2) + ((3:ℝ) * ((1/2:ℝ) ^ 2))))
noncomputable def rD (r : ℝ) : ℝ := ((((r ^ 2) + ((1/2:ℝ) ^ 2)) * (r ^ 2)) / ((((r ^ 2) + ((1/2:ℝ) ^ 2)) ^ 2) + (-((3:ℝ) * (r ^ 2)))))
noncomputable def rA (r : ℝ) : ℝ := ((r ^ 2) + ((1/2:ℝ) ^ 2))
noncomputable def rH (r : ℝ) : ℝ := (((((r ^ 2) + ((1/2:ℝ) ^ 2)) ^ 2) + ((3:ℝ) * ((1/2:ℝ) ^ 2))) / ((r ^ 2) + ((1/2:ℝ) ^ 2)))
noncomputable def rW (r : ℝ) : ℝ := (((3:ℝ) * (1/2:ℝ)) / ((((r ^ 2) + ((1/2:ℝ) ^ 2)) ^ 2) + ((3:ℝ) * ((1/2:ℝ) ^ 2))))
noncomputable def rPhi (r : ℝ) : ℝ := (0:ℝ)
noncomputable def rPsi (r : ℝ) : ℝ := (0:ℝ)
noncomputable def rX (r : ℝ) : ℝ := ((((r ^ 2) + ((1/2:ℝ) ^ 2)) ^ 2) + (-((3:ℝ) * (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 candPot : CoVec 5 := esPotential rPhi rPsi
noncomputable def candF : TwoForm 5 := esFaraday rPhi rPsi

noncomputable def gN : Metric 5
  | 0, 0 => liftRU (fun r u => ((-4:ℝ) * r ^ 2 + (11:ℝ)) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 0, 3 => liftRU (fun r u => ((-6:ℝ) * u) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 0, 4 => liftRU (fun r u => ((6:ℝ) * u + (-6:ℝ)) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 1, 1 => liftRU (fun r u => ((16:ℝ) * r ^ 4 + (4:ℝ) * r ^ 2) / ((1:ℝ) * fDl r) : ℝ → ℝ → ℝ)
  | 2, 2 => liftRU (fun r u => ((4:ℝ) * r ^ 2 + (1:ℝ)) / ((16:ℝ) * u * (1 - u)) : ℝ → ℝ → ℝ)
  | 3, 0 => liftRU (fun r u => ((-6:ℝ) * u) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 3, 3 => liftRU (fun r u => ((16:ℝ) * r ^ 4 * u + (8:ℝ) * r ^ 2 * u + (12:ℝ) * u ^ 2 + (1:ℝ) * u) / ((4:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 3, 4 => liftRU (fun r u => ((-3:ℝ) * u ^ 2 + (3:ℝ) * u) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 4, 0 => liftRU (fun r u => ((6:ℝ) * u + (-6:ℝ)) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 4, 3 => liftRU (fun r u => ((-3:ℝ) * u ^ 2 + (3:ℝ) * u) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 4, 4 => liftRU (fun r u => ((-16:ℝ) * r ^ 4 * u + (16:ℝ) * r ^ 4 + (-8:ℝ) * r ^ 2 * u + (8:ℝ) * r ^ 2 + (12:ℝ) * u ^ 2 + (-25:ℝ) * u + (13:ℝ)) / ((4:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | _, _ => liftRU (fun _ _ => (0:ℝ))

noncomputable def giN : Metric 5
  | 0, 0 => liftRU (fun r u => ((-16:ℝ) * r ^ 4 + (-8:ℝ) * r ^ 2 + (-13:ℝ)) / ((1:ℝ) * fDl r) : ℝ → ℝ → ℝ)
  | 0, 3 => liftRU (fun r u => ((-24:ℝ)) / ((1:ℝ) * fDl r) : ℝ → ℝ → ℝ)
  | 0, 4 => liftRU (fun r u => ((-24:ℝ)) / ((1:ℝ) * fDl r) : ℝ → ℝ → ℝ)
  | 1, 1 => liftRU (fun r u => ((16:ℝ) * r ^ 4 + (-40:ℝ) * r ^ 2 + (1:ℝ)) / ((4:ℝ) * fS r * r ^ 2) : ℝ → ℝ → ℝ)
  | 2, 2 => liftRU (fun r u => ((-16:ℝ) * u ^ 2 + (16:ℝ) * u) / ((1:ℝ) * fS r) : ℝ → ℝ → ℝ)
  | 3, 0 => liftRU (fun r u => ((-24:ℝ)) / ((1:ℝ) * fDl r) : ℝ → ℝ → ℝ)
  | 3, 3 => liftRU (fun r u => ((64:ℝ) * r ^ 4 + (-160:ℝ) * r ^ 2 + (-48:ℝ) * u + (4:ℝ)) / ((1:ℝ) * fDl r * fS r * u) : ℝ → ℝ → ℝ)
  | 3, 4 => liftRU (fun r u => ((-48:ℝ)) / ((1:ℝ) * fDl r * fS r) : ℝ → ℝ → ℝ)
  | 4, 0 => liftRU (fun r u => ((-24:ℝ)) / ((1:ℝ) * fDl r) : ℝ → ℝ → ℝ)
  | 4, 3 => liftRU (fun r u => ((-48:ℝ)) / ((1:ℝ) * fDl r * fS r) : ℝ → ℝ → ℝ)
  | 4, 4 => liftRU (fun r u => ((64:ℝ) * r ^ 4 + (-160:ℝ) * r ^ 2 + (48:ℝ) * u + (-44:ℝ)) / ((1:ℝ) * fDl r * fS r * (1 - u)) : ℝ → ℝ → ℝ)
  | _, _ => liftRU (fun _ _ => (0:ℝ))

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.MP01

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