Formalization handbook · all 12 guides

Detailed plans and progress for every workstream. Compiled results & assumption ledger → Vacuum demonstrator: checked margins & next device →

Fundamentals & Physics Principles Magnetic Confinement Fusion

What is a Stellarator? Physics Concepts, Geometry & Importance

Nuclear fusion requires heating hydrogen isotopes (Deuterium & Tritium) to over 100 million degrees Celsius—far hotter than the core of the Sun. At these extreme temperatures, matter becomes fully ionized plasma. To prevent this ultra-hot plasma from touching solid walls, magnetic fields trap charged particles inside a toroidal "magnetic bottle."

A stellarator uses external three-dimensional coils to create magnetic-field twist without requiring a large inductive plasma current. This supports the goal of steady-state operation. Finite plasma currents and instability mechanisms remain possible, so confinement, stability, and engineering feasibility each need their own analysis.

INTERACTIVE DIAGRAM

1. Toroidal Geometry & Helical Field Twist ($\iota$)

Simulates magnetic field lines wrapping around a torus. Toggle between Tokamak (driven current) vs. Stellarator (3D coil twist).

Schematic torus, field lines, and particle motion; no computed equilibrium or orbit solution.

Mode: 3D Helical Stellarator Coils Rotational Transform $\iota \approx 0.85$

🧲 Why Field Line Twist is Essential:

Simple toroidal magnetic fields cause charged particles to drift vertically due to magnetic field gradients ($\nabla B$) and curvature ($\mathbf{v}_d \propto \mathbf{B} \times \nabla B$). Ions drift up, electrons drift down, creating a huge electric field that blows the plasma apart.

By twisting magnetic field lines into a helical trajectory, a field line spends time on both top and bottom of the torus. This short-circuits the charge separation and confines the plasma!

Rotational Transform Metric:

$$\iota(\psi) = \frac{d\theta}{d\phi} = \text{Poloidal Turns per Toroidal Turn}$$

2. Tokamaks vs. Stellarators: Key Trade-offs & Physics Architecture

Why the world is shifting toward stellarators for commercial power generation.

TOKAMAK ARCHITECTURE 2D Axi-symmetric

High Current, High Disruption Risk

Uses planar toroidal coils combined with a massive central solenoid transformer to induce millions of Amperes of electric current ($I_p$) directly inside the plasma.

✗ Major Disruptions: Sudden instability collapses destroy vacuum chamber walls within milliseconds.
✗ Pulsed Operation: Solenoid flux runs out, requiring complex external current drive.
✓ Simple Coils: Planar circular magnets are much easier to manufacture.

Primary Bottleneck: Disruption avoidance & non-inductive current drive.

STELLARATOR ARCHITECTURE 3D Non-symmetric

External Field Twist & Steady-State Potential

Uses external three-dimensional coils to supply field twist; plasma currents can also affect the operating equilibrium.

✓ Reduced reliance on plasma current: Large inductive current is not required for confinement.
✓ Steady-state potential: Continuous operation also requires heat removal, transport control, and component margins.
⚠️ Complex Geometry: Highly complex 3D coils and high neoclassical drift losses unless quasisymmetric.

Primary Requirement: Mathematical optimization of 3D field geometry (Quasisymmetry).

The Core Challenge

Why Formal Verification (Lean 4) & Mathematical Theory are Essential

Because a stellarator lacks 2D rotational symmetry, particle orbits do not automatically conserve canonical toroidal momentum ($P_\phi$). Unoptimized 3D magnetic fields lead to severe particle drift losses where alpha particles ($\text{He}^{2+}$) escape before heating the plasma!

1. Quasisymmetry (QS)

Ensures magnetic field magnitude $|B(s, \theta, \phi)| = B(s, M\theta - N\phi)$ depends on only a single helicity combination, restoring continuous drift invariants!

2. High-Dimensional Design Space

Stellarator plasma boundaries are defined by dozens of Fourier coefficients ($R_{m,n}, Z_{m,n}$). Finding stable shapes ($\delta W > 0$) requires exploring infinite-dimensional functional spaces.

3. The PlasmaLean Solution

When complete, PlasmaLean will provide a formal mathematical foundation in Lean 4 without project-specific axioms. It is intended to enable AI agents to discover candidate geometries and prove precisely stated plasma-stability results with machine-checked certainty.

Target Goal: Mathematically proven stable, constructible 3D magnetic bottles.

Kernel Layer Specifications

The Kernel: Axiom-Free Foundations of MHD Physics

The planned Kernel will provide a minimal foundation for plasma domain modeling in Lean 4 (`PlasmaLean.Kernel`). It will introduce no ad hoc project axioms; mathematical entities will be represented by definitions, smooth structures, and explicit law-bearing structures grounded in Mathlib.

1. Ideal MHD System & 2-Forms

Kernel Axiom-Free

Models the continuum force balance on a compact 3-manifold $\Omega \subset \mathbb{R}^3$ with boundary $\partial \Omega$. In differential forms, the solenoidal magnetic field is represented as a closed 2-form $d\beta = 0$:

Force Equilibrium: $$\mathbf{J} \times \mathbf{B} = \nabla p$$

Solenoidal Field: $$\nabla \cdot \mathbf{B} = 0 \equiv d\beta = 0$$

Ampère's Law: $$\nabla \times \mathbf{B} = \mu_0 \mathbf{J}$$

Direct Deductions Planned for the Kernel:

$$\mathbf{B} \cdot \nabla p = 0 \quad \text{and} \quad \mathbf{J} \cdot \nabla p = 0$$

Magnetic field lines and current densities are everywhere tangent to scalar pressure isosurfaces $p(\mathbf{x}) = c$. By Poincaré-Hopf theorem, a connected, compact, boundaryless, orientable regular surface with a nonvanishing tangent field has genus one. A global nested foliation requires additional hypotheses.

Illustrative Lean sketch (`PlasmaLean/Kernel/MHD.lean`)

-- PlasmaLean/Kernel/MHD.lean
import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
import Mathlib.Analysis.InnerProductSpace.Basic

structure MHDEquilibrium (Ω : SmoothManifold 3) where
  B : VectorField Ω
  J : VectorField Ω
  p : SmoothFunction Ω
  mu_0 : ℝ
  force_balance : J × B = ∇ p
  solenoidal : ∇ · B = 0
  ampere : ∇ × B = mu_0 • J

theorem field_tangent_to_pressure (eq : MHDEquilibrium Ω) :
  (eq.B · ∇ eq.p = 0) ∧ (eq.J · ∇ eq.p = 0) := by
  -- Proven purely by algebraic linear combinations of force_balance
  sorry

2. Boozer Straight-Field-Line Charts

Coordinate Metric

On nested magnetic flux surfaces $\psi$, Boozer coordinates $(s, \theta, \phi)$ straighten magnetic field line trajectories. The Kernel is intended to formalize both contravariant and covariant representations:

Contravariant Representation:

$$\mathbf{B} = \nabla\psi \times \nabla\theta + \iota(\psi) \nabla\phi \times \nabla\psi$$

Covariant Representation:

$$\mathbf{B} = K \nabla\psi + I(\psi) \nabla\theta + G(\psi) \nabla\phi$$

Boozer Metric Volume Jacobian: $$\sqrt{g} = \frac{G + \iota I}{B^2}$$

Ensures non-singular coordinate transformations provided $B(\mathbf{x}) > 0$ throughout the volume.

Metric Jacobian $\sqrt{g}$ & $|B|$ vs. Poloidal Angle $\theta$ Chart.js Simulation

Illustrative supplied-chart Jacobian. Chart existence and regularity are separate theorem targets.

3. External Field Generators: Measure-Theoretic Biot-Savart

To connect continuous plasma manifolds to physical coil design, the Kernel defines current distributions as 1D space curves $C_k$ carrying current $I_k$:

Parametric Biot-Savart Formula

$$\mathbf{B}_{ext}(\mathbf{r}) = \frac{\mu_0 I}{4\pi} \oint_C \frac{d\mathbf{l} \times (\mathbf{r} - \mathbf{r}')}{|\mathbf{r} - \mathbf{r}'|^3}$$

Formulated in Lean using measure theory integrals over smooth embeddings $\gamma: S^1 \to \mathbb{R}^3$.

Planned formalization: Rather than relying on discrete straight-line approximations, the Kernel will represent the continuous Bochner/Lebesgue integral over suitable one-dimensional smooth embedded manifolds in $\mathbb{R}^3$.

Boundary Field Matching: This exact continuous definition is later used by the mathematical theory library to evaluate Neumann boundary matching $\mathbf{B}_{ext} \cdot \mathbf{n} = 0$ on plasma surfaces.

Theory Engine & Stability API

Mathematical Theory Engine: Asymmetric Solvability & Stability

This section outlines planned theoretical tools in mathematical physics (`PlasmaLean.Theory`). Drawing on functional analysis and Sobolev space theory ($H^k(\Omega)$), the completed library will formulate precisely scoped theorems about when 3D MHD models admit stable non-axisymmetric plasma equilibria ($\delta W > 0$).

1. Existence of Asymmetric Stable Equilibria

Existence Theorem

Will formalize conditions under which continuous spatial symmetry is not required by a specified confinement or stability result. A target theorem concerns smooth equilibria under non-axisymmetric boundary perturbations in appropriate Sobolev spaces:

Theorem (Asymmetric Existence): $$\exists \, \mathbf{B} \in H^k(\Omega), \; \nabla \cdot \mathbf{B} = 0 \land \mathbf{J} \times \mathbf{B} = \nabla p$$

The target is to prove, under explicit model and regularity hypotheses, that small non-axisymmetric boundary deformations $\partial \Omega_\epsilon$ admit a non-empty open set of smooth pressure profiles $p(\psi)$ yielding linearly stable, non-symmetric magnetic vector fields.

Illustrative Lean sketch (`PlasmaLean/Theory/AsymmetricExistence.lean`)

-- PlasmaLean/Theory/AsymmetricExistence.lean
import Mathlib.Analysis.SobolevSpace.Basic

theorem asymmetric_stable_equilibrium_exists
  (Ω : SmoothBoundary3D) (ε : ℝ) (hε : 0 < ε ∧ ε < ε_crit) :
  ∃ (B : VectorField Ω) (p : SmoothFunction Ω),
    MHDEquilibrium Ω B p ∧
    NonSymmetric B ∧
    SpectrumPositive (MHDOperator B) := by
  -- Proof leverages Nash-Moser implicit function theorem
  sorry

2. KAM Persistence of Invariant Flux Tori

KAM Surface Proof

To study barriers to chaotic magnetic-field-line drift, the Theory Engine is intended to formalize relevant Kolmogorov-Arnold-Moser (KAM) results for non-integrable Hamiltonian magnetic vector fields:

Diophantine Condition: $$\left|\iota(\psi) - \frac{m}{n}\right| \ge \frac{C}{n^{2+\gamma}}$$

A target theorem will state explicit hypotheses under which individual magnetic flux surfaces with suitable nonresonant rotational transform $\iota(\psi)$ persist under 3D non-axisymmetric perturbations; it will not assume a complete foliation.

Retained Flux Surface Fractional Volume vs. Perturbation $\epsilon$ KAM Persistence Curve

Synthetic curve for intuition. A quantitative KAM theorem needs explicit hypotheses; no retained-volume bound is certified here.

3. Linear MHD Stability Spectrum & Energy Principle ($\delta W > 0$)

An energy principle relates a specified equilibrium and admissible displacement space to a precise stability conclusion. Coercivity can give norm bounds; neutral modes, boundary conditions, and continuous spectrum require separate treatment. The handbook states these obligations explicitly.

Spectral Analysis

Fixed-boundary energy integral (zero-trace displacements):

$\delta W_p = \frac{1}{2} \int_V \left[ \frac{|\mathbf{Q}|^2}{\mu_0} - \mathbf{\xi}\cdot(\mathbf{J}\times\mathbf{Q}) + \gamma p (\nabla \cdot \mathbf{\xi})^2 + (\mathbf{\xi} \cdot \nabla p)(\nabla \cdot \mathbf{\xi}) \right] d^3x$

Where $\mathbf{Q} = \nabla \times (\mathbf{\xi} \times \mathbf{B})$ is the perturbed magnetic field and $\mathbf{\kappa} = (\mathbf{b} \cdot \nabla)\mathbf{b}$ is field line curvature.

Invented mode energies for illustration. Positive values in a finite set of modes do not establish continuum stability.

AI Agent Implementation Specification

Lean 4 AI Coding Agent Specification & Prompt Engine

To harness the power of AI in discovering new plasma stability theory for PlasmaLean, this specification provides guidelines, repository layout, Mathlib dependencies, tactic conventions, and structured prompts for autonomous AI coding agents (Cursor, Copilot, local LLMs).

1. Lake Project Setup (`lakefile.toml`)

PlasmaLean Package

Configure package dependencies ensuring Mathlib differential geometry, Sobolev spaces, and interval arithmetic libraries are linked:

# lakefile.toml
# Repository: https://github.com/siddhartha-gadgil/PlasmaLean
name = "PlasmaLean"
version = "0.1.0"
defaultTargets = ["PlasmaLean"]

[[lean_lib]]
name = "PlasmaLean"
srcDir = "src"

[dependencies]
mathlib = { git = "https://github.com/leanprover-community/mathlib4.git", rev = "v4.34.1" }

Mandatory Mathlib Imports for AI Agents:

• Mathlib.Geometry.Manifold.SmoothManifoldWithCorners

• Mathlib.Analysis.InnerProductSpace.Basic

• Mathlib.Analysis.SobolevSpace.Basic

• Mathlib.Topology.MeasureTheory.Integral.Bochner

2. Module Hierarchy & Separation

File Architecture

Coding agents must strictly maintain file boundaries and public/private API visibility rules across the core library modules:

PlasmaLean/Kernel/ Axiom-Free Core: `MHD.lean`, `Boozer.lean`, `BiotSavart.lean`. ZERO `axiom` declarations permitted!

PlasmaLean/Sanity/ Planned boundary limits: `GradShafranov.lean`, `VacuumLaplace.lean`, `GarrenBoozer.lean`. Will test Kernel consistency.

PlasmaLean/Theory/ Planned theoretical API: `AsymmetricExistence.lean`, `KAM.lean`, `EnergySpectrum.lean`. Will express precisely scoped stability results.

PlasmaLean/Bridge/ Constructible Realization: `RadiiPolynomials.lean`, `CoilBounds.lean`. Interval-checked hardware parameters.

3. Coding Rules & Tactic Conventions for AI Agents

Rule 1: Immediate Mathlib Lemmas

Immediately following every `def` or `structure`, the agent MUST formulate and prove characterizing `@[simp]` lemmas so that downstream proof synthesis avoids unfolding raw definitions.

Rule 2: Preferred Proof Tactics

Agents should prioritize robust tactics: `aesop` for structural goals, `calc` blocks for tensor manipulation, `positivity` for norm bounds, and `gcongr` for inequalities.

Rule 3: Zero Unverified Axioms

Agents must never introduce unverified `axiom` assumptions in `PlasmaLean/Kernel/`. All physical hypotheses must be explicit fields inside Lean structures.

Interactive AI Agent System Prompt Generator

Select a target module below to generate a system prompt tailored for LLM coding agents (Cursor, Copilot, Claude) targeting the siddhartha-gadgil/PlasmaLean repository:

Target Module:

Agent Capability Level:

Generated Agent Instruction Output

-- Loading prompt generator...

Constructible Design & Stability Studio

Constructible Stellarator Co-Design & Stability Studio

The long-term goal is to connect abstract mathematical stability theory ($\delta W > 0$) to constructible hardware. When implemented, the Co-Design Studio will test parameter choices against sourced physical constraints such as coil curvature, inter-coil clearance, and interval-certified numerical bounds in the `PlasmaLean` library.

1. Physical Constructibility Bounds

Hardware Bounds

To construct superconducting magnets (e.g. $\text{Nb}_3\text{Sn}$ or HTS tape), space curve geometries must satisfy strict bend radius and clearance thresholds:

Physical Metric	Illustrative Bound	Engineering Justification
Coil Bend Radius ($\rho_{min}$)	> 0.52 m	Example only; allowable strain requires sourced conductor data
Coil Clearance ($d_{c-c}$)	> 0.83 m	Example space budget; confirm for the selected device
Plasma-Coil Gap ($d_{p-c}$)	> 1.40 m	Example space budget; shielding needs its own model

2. Rigorous Numerics: Radii Polynomial Method

Computer-Assisted Proof

To bridge numerical design solvers (DESC, SIMSOPT, VMEC) with Lean 4 formal proofs, interval arithmetic is combined with Banach contraction operators:

Banach Space Fixed-Point Radii Certificate:

The planned certificate will let Lean verify that, when the radii-polynomial hypotheses hold, an exact mathematical solution exists within distance $r_{min}$ of the numerical result $\bar{x}$.

Illustrative target bound: $\|x_{exact} - x_{numerical}\| \le r_{min} = 3.42 \times 10^{-8}$

Interactive AI Co-Design Sandbox

Adjust the parameters below to preview an illustrative AI exploration workflow. The audit interaction simulates the checks and proof output that the completed system is intended to produce; it does not currently constitute a Lean certificate.

Geometric & Field Parameters

Aspect Ratio ($A = R/a$): 6.5

Rotational Transform ($\iota$): 0.85

Non-Axisymmetric Shaping ($\epsilon_{shaping}$): 0.18

Coils per Field Period: 10

Plasma Beta ($\beta$ %): 3.2%

Illustrative Future Certificate Output

Demo ready

MHD $\delta W$ Stability +0.142

KAM Surface Vol 94.2%

Coil Clearance 0.89 m

$\mathbf{B} \cdot \mathbf{n}$ Error 1.2 × 10⁻⁴

Simulated Future Lean 4 Proof Log:

-- Click "Preview illustrative audit" to test geometry...
-- Parameters: Aspect=6.5, Rotational Transform=0.85, Shaping=0.18
-- Field Coils/Period=10, Plasma Beta=3.2%

Lean Lake Command: lake env lean --run VerifyStellarator.lean

What is a Stellarator? Physics Concepts, Geometry & Importance

1. Toroidal Geometry & Helical Field Twist ($\iota$)

2. Tokamaks vs. Stellarators: Key Trade-offs & Physics Architecture

High Current, High Disruption Risk

External Field Twist & Steady-State Potential

Why Formal Verification (Lean 4) & Mathematical Theory are Essential

PlasmaLean: Formalizing Mathematical Theory for Constructible Stellarators

Explore & Contribute to the PlasmaLean Codebase

Theoretical Engine

AI Discovery & Synthesis

Machine-Checked Correctness

PlasmaLean Library Architecture & Layer Hierarchy

The Kernel

Boundary Checks

Theory Engine

AI Spec & Agents

Co-Design Studio

Referencing Recent Breakthroughs as Benchmark Sources

The Kernel: Axiom-Free Foundations of MHD Physics

1. Ideal MHD System & 2-Forms

2. Boozer Straight-Field-Line Charts

3. External Field Generators: Measure-Theoretic Biot-Savart

Boundary Checks: Degeneracies & Overdetermination Proofs

Grad-Shafranov Collapse

Vacuum Laplace Fields

Garren-Boozer Constraint

Garren-Boozer Order-by-Order Overdetermination Inspector