VI-02 candidate NQ14 (ST03 metric with charge 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/NQ14/Defs.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.candF, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.candG, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.candGi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.candPot, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.dom, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.ff, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.gN, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.giN, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rA, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rB, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rD, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rH, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rPhi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rPsi, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rW, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.rX, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.radR, ExactVacuumAtlas.EinsteinMaxwell.ES5.Cand.NQ14.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 `n14_static_wrong_charge` (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.NQ14

noncomputable def ff (r : ℝ) : ℝ := ((3:ℝ) * r ^ 4 + (-6:ℝ) * r ^ 2 + (1:ℝ))

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

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 => ((-3:ℝ) * r ^ 4 + (6:ℝ) * r ^ 2 + (-1:ℝ)) / ((3:ℝ) * r ^ 4) : ℝ → ℝ → ℝ)
  | 1, 1 => liftRU (fun r u => ((3:ℝ) * r ^ 4) / ((1:ℝ) * ff r) : ℝ → ℝ → ℝ)
  | 2, 2 => liftRU (fun r u => ((1:ℝ) * r ^ 2) / ((4:ℝ) * u * (1 - u)) : ℝ → ℝ → ℝ)
  | 3, 3 => liftRU (fun r u => ((1:ℝ) * r ^ 2 * u) : ℝ → ℝ → ℝ)
  | 4, 4 => liftRU (fun r u => ((-1:ℝ) * r ^ 2 * u + (1:ℝ) * r ^ 2) : ℝ → ℝ → ℝ)
  | _, _ => liftRU (fun _ _ => (0:ℝ))

noncomputable def giN : Metric 5
  | 0, 0 => liftRU (fun r u => ((-3:ℝ) * r ^ 4) / ((1:ℝ) * ff r) : ℝ → ℝ → ℝ)
  | 1, 1 => liftRU (fun r u => ((3:ℝ) * r ^ 4 + (-6:ℝ) * r ^ 2 + (1:ℝ)) / ((3:ℝ) * r ^ 4) : ℝ → ℝ → ℝ)
  | 2, 2 => liftRU (fun r u => ((-4:ℝ) * u ^ 2 + (4:ℝ) * u) / ((1:ℝ) * r ^ 2) : ℝ → ℝ → ℝ)
  | 3, 3 => liftRU (fun r u => ((1:ℝ)) / ((1:ℝ) * r ^ 2 * u) : ℝ → ℝ → ℝ)
  | 4, 4 => liftRU (fun r u => ((1:ℝ)) / ((1:ℝ) * r ^ 2 * (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.NQ14

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