PlasmaLean roadmap: from foundational lemmas to practical design

Prepared against commit 466920416e97561e4669759ab4077b9a23281ebd on 10 October 2026. The repository is at the starter stage. This roadmap describes work to do; it does not mark the proposed modules or certificates as implemented.

Contents

• Success criteria
• Parallel mathematical tracks
• Milestones and evidence gates
• The first coding sequence
• Substantial existing mathematics to formalize
• Ambitious research problems
• AI theory-development loop
• Progress records

Success criteria

A useful final artifact is a concrete coil/plasma/component design with:

1. a mathematical model of its fields and equilibrium;
2. the specified plasma stability and confinement/transport bounds;
3. continuous geometric and engineering margins;
4. operating/manufacturing/material uncertainty handled with correct quantifiers;
5. explicit model/data assumptions and evidence for their applicability;
6. Lean declarations and checked certificates attached to one decoded candidate.

The final scientific claim is as strong as that conjunction and the validated applicability of its models. Keep optional goals such as global optimality separate. Proving feasibility of one valuable design is already a substantial outcome.

Use task labels:

• F — Formalization: an established theorem or elementary deduction, after exact source/hypothesis extraction.
• V — Validation development: a new checker or constructive estimate connecting numerical candidates to an established mathematical theorem.
• R — Research: a new theorem or a substantial unresolved instance/class needed for stronger design claims.

An R label is a proposed research target, not an assertion that every related problem is open. Recheck the current literature before claiming novelty or unresolved status. The formulations below deliberately specify classes and weaker alternatives rather than asserting impossible universal guarantees.

Parallel mathematical tracks

The library should develop several mathematical tracks; work in one does not depend on completing every other track.

Dependency structure:

flowchart TD
    A["Models and geometry"] --> B["Equilibrium and stability"]
    A --> C["Particles and transport"]
    A --> D["Coils and materials"]
    E["Checked computations"] --> B
    E --> C
    E --> D
    B --> F["Common design certificate"]
    C --> F
    D --> F

The arrows are proof interfaces, not merely software imports. Bootstrap current, deformation, and heat sources also create feedback loops; close them with a common solution or controlled error/envelope theorem.

Milestones and evidence gates

These gates need not be completed in table order. For example, component theory can proceed from conservative load envelopes while the MHD theorem is still under development. A vacuum demonstrator can be an achievable product before a finite-beta reactor design.

At P5, accept a sound nonnegative-energy/observable conclusion if a full positive spectral gap is mathematically unavailable; name the conclusion accurately. At P8, a fixed-boundary result cannot silently become free-boundary stability.

The first coding sequence

Use the six project skills. Read 00 for contracts and 09 for sources.

Then select one short end-to-end example: a documented simple coil field with certified geometry plus a reduced orbit property, or a thermal/material component bound linked to a sourced load envelope. Keep mathematical toy examples and physical candidate examples labelled separately.

Compile only the Lean code actually written. These Markdown specifications are not evidence that a future declaration compiles. Search the pinned Mathlib/TauCeti sources before committing to analytic API dependencies.

Substantial existing mathematics to formalize

1. Flux-form/divergence equivalence, pressure-surface topology under complete hypotheses, Boozer reciprocal-basis identities.
2. Fixed-boundary MHD linearization and energy principle with a modern closed form/operator formulation.
3. Source-specific local interchange/ballooning criteria.
4. Noether invariants and the precise quasisymmetry/omnigeneity implications in reduced guiding-centre dynamics.
5. A posteriori invariant-torus/KAM results with explicit nondegeneracy and Diophantine constants.
6. Piecewise smooth toroidal MHD existence theorems, particularly Enciso–Luque–Peralta-Salas.
7. Generic validated fixed-point, ODE, PDE and form/eigenvalue bounds in the function spaces actually used.
8. Conservation/positivity/coercivity results for heat, elasticity, circuits, and transport/inventory models.

Formalize theorem prerequisites in reusable mathematical libraries where appropriate. A physical law in a typeclass is not a substitute for any of these derivations.

Ambitious research problems

R1. Constructive three-dimensional finite-pressure equilibrium

For a specified genuinely nonaxisymmetric toroidal geometry and nonconstant pressure/current class, prove an a posteriori existence theorem with explicit, usable constants, including small-divisor/resonance compatibility, boundary conditions, and profile constraints. Validate a solution or branch generated by a real equilibrium solver.

Starting points: Enciso et al., SPEC, Boozer, and Constantin et al.. Piecewise smooth/stepped-pressure results are already available in important classes. A theorem for those classes is a useful milestone; continuously nested smooth solutions require their own analysis. If the proposed class is obstructed, characterize the obstruction and adopt a justified weak or modified model.

R2. All-mode stability in a nonaxisymmetric practical class

Find a geometry-sensitive sufficient condition for nonnegative or quantitatively controlled ideal-MHD energy on the correct admissible space, with a free plasma boundary when required. Handle neutral modes and continuous spectrum instead of assuming a generic elliptic spectral gap.

Target a physically useful finite-beta/current range and coil tolerance budget. A robust observable bound or restricted perturbation theorem may be more appropriate than coercivity in the full H¹ norm.

R3. Nonlinear stability with a useful basin

Establish a constrained conserved/Lyapunov functional controlling an appropriate distance to a three-dimensional equilibrium family, including a quantitative nonlinear remainder and well-posedness/continuation assumptions. For an all-time result, prove the needed continuation rather than assuming that the linear energy calculation prevents singularities.

A major target is a model/class with global orbital control; a finite-time nonlinear bound under quantified regularity is an intermediate result. Do not present arbitrary three-dimensional ideal-MHD global regularity as a routine library task.

R4. Quantitative imperfect-symmetry confinement and transport

Relate a derivative-sensitive quasisymmetry/omnigeneity defect and field perturbation to finite-time loss or a loss-measure bound for a specified energetic-particle initial distribution. Handle or explicitly exclude separatrix/resonance classes and include finite-gyroradius/reduction error.

Then connect the defect to a rigorous neoclassical transport/current bound in the relevant collision regime. An L² symmetry objective alone is not the desired theorem.

R5. Geometry-based kinetic stability and heat-flux bounds

Extend restricted maximum-J/energy results to a specified multispecies, gradient, collision, electromagnetic and forcing regime. Prove bounds on growth or nonlinear time-averaged heat flux useful in the operating envelope, rather than requiring every microinstability to vanish.

Couple the result to profile evolution and exhaust. This is a substantial open research direction, and a verified reduced model with explicit limitations is worthwhile progress.

R6. Controlled model reduction for design

Prove explicit finite-time and norm/observable error bounds between full Lorentz and guiding-centre trajectories, between kinetic and selected fluid/profile models, or between finite-width conductors and filament models. Transfer certificates through margins exceeding these errors.

Singular limits, collisions, boundaries, and long operating horizons can invalidate naive perturbation arguments. Start with restricted smooth regimes and strengthen only through proved estimates.

R7. Coupled robust operation and lifetime

Construct an invariant operating set or a time-dependent safe envelope for the coupled plasma/current/heat/stress/material evolution under bounded disturbances and a specified controller. Account for profile response, coil deformation, critical-current change, erosion and irradiation degradation.

Prove feasibility for all histories in the declared input class and return a conservative service interval. Statistical material data and model discrepancy remain explicit interfaces.

R8. Scalable proof certificates for practical resolution

Develop proof-producing compressed certificates that scale to realistic coil geometry, equilibrium modes, transport discretizations, and material meshes. Prove decoding, domain coverage, tail/control estimates and soundness; use GPU/AI search to generate certificates without enlarging the trusted mathematical boundary.

These targets can reveal new mathematics rather than merely reimplement numerical codes.

AI theory-development loop

For each missing design implication:

1. State a precise useful lemma and its assumptions.
2. Search/extract the closest existing theorem.
3. Try a proof and look for counterexamples.
4. Repair an overbroad claim by a justified hypothesis or weaker conclusion.
5. Formalize a complete proof; prove limiting cases and useful corollaries.
6. Attach its quantitative output to the next design contract.
7. Repeat, or record a precise obstruction/research problem.

Use experiments to find structure, witnesses, and failures. Preserve the priority on theoretical advances. Do not replace theory with repeated floating-point optimization when the missing step is an all-mode inequality or a continuum existence theorem.

Progress records

Keep a table of task ID, mathematical statement, dependencies, source locator, assumptions, status, declaration, build result, example certificate, margin, and next task. Mark proved informally, published theorem extracted, Lean verified, numerically observed, and conjectured distinctly.

For each design candidate record the highest gate actually passed, the exact supported claims, and the remaining gaps. A proof failure can mean insufficient bounds, wrong representation, or a genuine mathematical obstruction; it is not automatically physical instability.