Buildable, MHD-stable quasi-isodynamic stellarator

Paper designs claiming all reactor requirements simultaneously now exist (e.g. Proxima's Stellaris, CIEMAT-QI4X), but no reactor-relevant QI stellarator with HTS coils has been built; Proxima's first hardware de-risking step, the Stellarator Model Coil, is scheduled for 2027. On the benchmark side the ConStellaration mhd_stable track had only 6 submitter labels and 42 result rows as of 2026-09-21, and recent literature notes pressure-driven instabilities persist in QI configurations, limiting access to high power density.

Source: proximafusion.com

import Mathlib

/-!
# Buildable, MHD-stable quasi-isodynamic (QI) stellarator

Acceptance predicate modelled on the ConStellaration benchmark (Proxima Fusion /
Hugging Face), "MHD-stable QI" track: a fixed-boundary plasma shape that is
quasi-isodynamic, compact, not too elongated, has a vacuum magnetic well and
limited flux compression in bad curvature, scored on coil simplicity.

Formalized concretely: the candidate object (stellarator-symmetric Fourier boundary),
the constraint set, the scalarized objective threshold, and a monotone rung family.

Opaque oracle (`Evaluator`): the ideal-MHD equilibrium solve (VMEC++ in the benchmark)
and every derived figure of merit. Lean does not compute any of them. The attester is
whoever runs the pinned evaluator version on the submitted boundary (benchmark
maintainers or an agreed third party); a board must pin evaluator version + resolution.

Units: boundary coefficients in metres; all figures of merit dimensionless.
QI residual is compared on log10 scale as in the benchmark. The default numbers in
`benchmarkLimits` are indicative of the published track and must be re-checked against
the pinned release before money moves.
-/

namespace OpenSpur.Problems.StellaratorQiMhd

/-- Stellarator-symmetric boundary: (m, n, R_mn cosine, Z_mn sine), metres. -/
structure Boundary where
  fieldPeriods : ℕ
  modes : List (ℕ × ℤ × ℝ × ℝ)

/-- Outputs of the pinned equilibrium + metrics pipeline (oracle, not verified). -/
structure Evaluator where
  /-- equilibrium solve converged at pinned resolution and the surface is non-self-intersecting -/
  converged : Boundary → Prop
  log10QiResidual : Boundary → ℝ
  aspectRatio : Boundary → ℝ
  maxElongation : Boundary → ℝ
  /-- edge rotational transform divided by number of field periods -/
  edgeIotaPerPeriod : Boundary → ℝ
  mirrorRatio : Boundary → ℝ
  /-- vacuum magnetic well depth; > 0 means a well (favourable for interchange) -/
  vacuumWell : Boundary → ℝ
  /-- flux compression in regions of bad curvature (benchmark proxy) -/
  fluxCompression : Boundary → ℝ
  /-- normalized minimum magnetic-gradient scale length L_∇B (coil-simplicity proxy; larger is simpler) -/
  gradScaleLength : Boundary → ℝ

structure Limits where
  maxLog10Qi : ℝ
  maxAspect : ℝ
  maxElongation : ℝ
  minEdgeIotaPerPeriod : ℝ
  maxMirror : ℝ
  maxFluxCompression : ℝ
  /-- required coil-simplicity objective -/
  minGradScaleLength : ℝ

/-- Indicative thresholds (re-verify against the pinned ConStellaration release). -/
def benchmarkLimits : Limits where
  maxLog10Qi := -3.5
  maxAspect := 10
  maxElongation := 5
  minEdgeIotaPerPeriod := 0.25
  maxMirror := 0.25
  maxFluxCompression := 0.9
  minGradScaleLength := 1

/-- Feasibility for the MHD-stable QI track. Vacuum well is strictly positive. -/
def Feasible (E : Evaluator) (L : Limits) (b : Boundary) : Prop :=
  E.converged b ∧
  E.log10QiResidual b ≤ L.maxLog10Qi ∧
  E.aspectRatio b ≤ L.maxAspect ∧
  E.maxElongation b ≤ L.maxElongation ∧
  L.minEdgeIotaPerPeriod ≤ E.edgeIotaPerPeriod b ∧
  E.mirrorRatio b ≤ L.maxMirror ∧
  0 < E.vacuumWell b ∧
  E.fluxCompression b ≤ L.maxFluxCompression

/-- SOLVED: a feasible boundary that also meets the coil-simplicity target. -/
def Solved (E : Evaluator) (L : Limits) (b : Boundary) : Prop :=
  Feasible E L b ∧ L.minGradScaleLength ≤ E.gradScaleLength b

/-- Rung k: QI tolerance tightens by 0.25 decades and L_∇B target rises by 0.1 per rung. -/
noncomputable def rung (L : Limits) (k : ℕ) : Limits :=
  { L with maxLog10Qi := L.maxLog10Qi - (k : ℝ) / 4,
           minGradScaleLength := L.minGradScaleLength + (k : ℝ) / 10 }

/-- Solving a higher rung implies solving any lower rung (same evaluator). -/
theorem rung_mono (E : Evaluator) (L : Limits) (b : Boundary) {j k : ℕ} (hjk : j ≤ k)
    (h : Solved E (rung L k) b) : Solved E (rung L j) b := by
  have hc : (j : ℝ) ≤ k := by exact_mod_cast hjk
  obtain ⟨⟨h0, hqi, hrest⟩, hg⟩ := h
  refine ⟨⟨h0, ?_, hrest⟩, ?_⟩
  · simp only [rung] at hqi ⊢; linarith
  · simp only [rung] at hg ⊢; linarith

end OpenSpur.Problems.StellaratorQiMhd

• ConStellaration leaderboard (Hugging Face Space; geometrical / simple_to_build / mhd_stable tracks)
• ConStellaration dataset (~182k rows of QI-like boundaries with VMEC equilibria and metrics)
• ConStellaration public results dataset
• Official evaluator (problems.py: MHDStableQIStellarator)
• ConStellaration paper (arXiv 2506.19583)
• Stellaris QI power-plant design (Fusion Engineering and Design, 2025)