Literature and source-extraction guide

These are entry points for a coding agent, organized around the theorem backlogs in this directory. Prefer the primary paper, author's manuscript, publisher record, or official software documentation. Read the source before importing a theorem: a review, numerical demonstration, or bibliography entry does not supply missing hypotheses.

The guide was assembled on 2026-10-10. Publication metadata and primary entry points were checked where accessible; it is not a claim that every full text has been audited. Exact theorem/equation locators must be recorded during extraction, rather than invented from an abstract. Links to arXiv are unversioned entry points: pin the version actually used.

Contents

• Source extraction protocol
• Geometry, equilibrium, and symmetry
• Stability and kinetic theory
• Validated computation and analysis
• Design algorithms and software
• Engineering, materials, and experiment
• Reading order and theorem targets

Source extraction protocol

For each imported result, record:

1. Authors, title, year, DOI/arXiv version, stable URL, and access date.
2. Exact theorem, section, equation, or page, including any erratum.
3. Model, units, coordinate normalization, domain, boundary conditions, regularity, and parameter range.
4. All quantifiers and nondegeneracy/positivity assumptions; identify hidden existence, uniqueness, spectral, or convergence assumptions.
5. The precise conclusion and whether it is exact, asymptotic, conditional, numerical, or empirical.
6. The proposed Lean statement, definition correspondence, required Mathlib lemmas, and a sanity example.
7. Any gap between the source result and the desired design contract.

For data, additionally record material grade, experimental conditions, processing/version, uncertainty interpretation, interpolation domain, and conservative envelopes. For software, pin the release/commit, input conventions, normalization, and source of numerical error. A solver's self-reported residual is candidate data until its enclosure is checked.

Geometry, equilibrium, and symmetry

• Boozer81. A. H. Boozer (1981), Plasma equilibrium with rational magnetic surfaces, Physics of Fluids 24, 1999–2003. DOI: 10.1063/1.863297. Starting point for magnetic-coordinate conventions. Translate flux and angle normalization explicitly; construct charts on an annulus and handle the axis separately.

• GB91-field. D. A. Garren and A. H. Boozer (1991), Magnetic field strength of toroidal plasma equilibria, Physics of Fluids B 3, 2805–2821. DOI: 10.1063/1.859915. Extract near-axis expansion equations, ordering, and equilibrium compatibility conditions.

• GB91-existence. D. A. Garren and A. H. Boozer (1991), Existence of quasihelically symmetric stellarators, Physics of Fluids B 3, 2822–2834. DOI: 10.1063/1.859916. Extract the actual source-specific restrictions; do not turn a generic overdetermined expansion into a universal nonexistence claim.

• LS19. M. Landreman and W. Sengupta (2019), Constructing stellarators with quasisymmetry to high order. arXiv:1908.10253; publisher full text. Use the explicit near-axis construction and Appendix A, which identifies corrections and convention changes relative to the original Garren–Boozer formulas. Prove coefficient identities first; convergence and remainder bounds are separate targets.

• BKM20. J. W. Burby, N. Kallinikos, and R. S. MacKay (2020), Some mathematics for quasi-symmetry. arXiv:1912.06468. Useful for geometric definitions, reduced dynamics, and conservation laws. Extract which notion of quasisymmetry and which guiding-centre approximation each theorem uses.

• ELPS. A. Enciso, A. Luque, and D. Peralta-Salas, MHD equilibria with nonconstant pressure in nondegenerate toroidal domains, Journal of the European Mathematical Society 27 (2025), 2251–2291. DOI: 10.4171/JEMS/1410; arXiv:2104.08149. A rigorous existence reference involving piecewise-smooth equilibria and invariant structures. Preserve the interface regularity and nondegeneracy assumptions instead of claiming a global smooth nested equilibrium.

• CDG21. P. Constantin, T. D. Drivas, and D. Ginsberg (2021), On quasisymmetric plasma equilibria sustained by small force, Journal of Plasma Physics 87, 905870111. Publisher record. The additional force is part of the result. Quantifying or removing it requires another argument.

• MRxMHD12. S. R. Hudson et al. (2012), Computation of multi-region relaxed magnetohydrodynamic equilibria, Physics of Plasmas 19, 112502. DOI: 10.1063/1.4765691; arXiv:1211.3072. Defines a useful stepped-pressure/relaxed model and SPEC computation. Formalize interface conditions and distinguish this model from smooth ideal MHD.

• LP22. M. Landreman and E. Paul (2022), Magnetic fields with precise quasisymmetry for plasma confinement, Physical Review Letters 128, 035001. DOI: 10.1103/PhysRevLett.128.035001; arXiv:2108.03711. Numerical candidates and useful quantitative targets; numerical precision does not establish exact quasisymmetry or an all-orbit confinement theorem.

• EPS-relaxation. A. Enciso and D. Peralta-Salas, Obstructions to Topological Relaxation for Generic Magnetic Fields. arXiv:2308.15383; DOI: 10.1007/s00205-024-02078-5. Read the precise genericity, topology, and relaxation class before assuming arbitrary magnetic data can be relaxed to the desired equilibrium.

Stability and kinetic theory

• BFKK58. I. B. Bernstein, E. A. Frieman, M. D. Kruskal, and R. M. Kulsrud (1958), An energy principle for hydromagnetic stability problems, Proceedings of the Royal Society A 244, 17–40. DOI: 10.1098/rspa.1958.0023; institution-hosted scan. Start with Section 2 for linearization and Section 3 for the energy principle, including plasma, surface, and vacuum terms. Convert its rationalized Gaussian units to SI. Supply a modern functional-analytic treatment where the source's modal reasoning requires one.

• Freidberg14. J. P. Freidberg (2014), Ideal MHD, Cambridge University Press. DOI: 10.1017/CBO9780511795046. Main textbook entry point for equilibrium, energy-principle derivations, boundary conditions, and restricted stability criteria. Record the actual chapter/equation and sign conventions used.

• MG80. P. J. Morrison and J. M. Greene (1980), Noncanonical Hamiltonian Density Formulation of Hydrodynamics and Ideal Magnetohydrodynamics, Physical Review Letters 45, 790. Original DOI; erratum, Physical Review Letters 48, 569. An entry point for Hamiltonian/Casimir methods. A bracket or conserved functional alone does not prove coercivity, a nonlinear basin, or global existence.

• Littlejohn83. R. G. Littlejohn (1983), Variational principles of guiding centre motion, Journal of Plasma Physics 29, 111–125. DOI: 10.1017/S002237780000060X. Extract the variational model, ordering, symplectic structure, and reduced conservation laws. A guiding-centre theorem must retain its reduction assumptions.

• Helander14. P. Helander (2014), Theory of plasma confinement in non-axisymmetric magnetic fields, Reports on Progress in Physics 77, 087001. Original DOI; 2018 corrigendum. Main review for stellarator confinement, omnigenity, symmetry, and neoclassical theory. Use it to locate primary results and definitions; read the corrigendum before copying formulas.

• CS97. J. R. Cary and S. G. Shasharina (1997), Helical Plasma Confinement Devices with Good Confinement Properties, Physical Review Letters 78, 674. DOI: 10.1103/PhysRevLett.78.674. Starting point for omnigenity and its relationship to quasisymmetry. Follow the primary derivation of bounce-action constraints and the treatment of trapped/passing particles.

• BH07. A. J. Brizard and T. S. Hahm (2007), Foundations of nonlinear gyrokinetic theory, Reviews of Modern Physics 79, 421–468. DOI: 10.1103/RevModPhys.79.421. Extract ordering, field equations, polarization, and energy identities for one explicitly chosen gyrokinetic model; do not mix equations from different truncation orders.

• SFINCS14. M. Landreman, H. M. Smith, A. Mollén, and P. Helander (2014), Comparison of particle trajectories and collision operators for collisional transport in nonaxisymmetric plasmas, Physics of Plasmas 21, 042503. DOI: 10.1063/1.4870077; SFINCS source. Concrete drift-kinetic models, collision choices, and transport calculations. Prove nullspace/solvability and error bounds for the selected operator before certifying a flux.

• MaxJ12. J. H. E. Proll et al. (2012), Resilience of Quasi-Isodynamic Stellarators against Trapped-Particle Instabilities, Physical Review Letters 108, 245002. DOI: 10.1103/PhysRevLett.108.245002. A restricted kinetic stability result: extract species, gradient, frequency, and ordering assumptions rather than asserting stability to all microinstabilities.

• TP13. P. Helander, J. H. E. Proll, and G. G. Plunk (2013), Collisionless microinstabilities in stellarators. I. Analytical theory of trapped-particle modes, Physics of Plasmas 20, 122505. arXiv:1311.3095; 2017 erratum, 24, 039901. Read both before deriving a sign or stability criterion.

• TP17. G. G. Plunk, J. H. E. Proll, and P. Helander (2017), Collisionless microinstabilities in stellarators. IV. The ion-driven trapped-electron mode. arXiv:1708.04085. A useful check on the scope of simplified “maximum-J implies stability” claims.

Validated computation and analysis

• Rump10. S. M. Rump (2010), Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19, 287–449. DOI: 10.1017/S096249291000005X; author PDF. Basis for interval verification and matrix enclosures. An external verified numerical routine still needs a sound import/checker boundary in Lean.

• NPW19. M. T. Nakao, M. Plum, and Y. Watanabe (2019), Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations. DOI: 10.1007/978-981-13-7669-6. Source for analytic error bounds and verified PDE methods. Check whether the specific operator is coercive/elliptic; ideal MHD does not inherit that property automatically.

• Parameterization16. À. Haro, M. Canadell, J.-L. Figueras, A. Luque, and J. M. Mondelo (2016), The Parameterization Method for Invariant Manifolds: From Rigorous Results to Effective Computations. DOI: 10.1007/978-3-319-29662-3. Entry point for constructive invariant-manifold methods. For a KAM certificate, select a precise a posteriori theorem and extract every regularity, twist, and small-divisor constant.

• Lessard-tutorial. J.-P. Lessard's computer-assisted proof tutorial entry point. Use to locate explicit Newton/radii-polynomial arguments and their hypotheses. Retrieve the full document and establish the exact bibliographic/theorem locator before use; the existence of a tutorial does not validate an MHD operator.

• Ciarlet88. P. G. Ciarlet (1988), Mathematical Elasticity, Volume I: Three-Dimensional Elasticity, North-Holland. Publisher entry. Functional-analytic foundation for elasticity, boundary conditions, and existence questions. Use a linear supported-body submodel first; nonlinear/contact problems need their own assumptions.

Design algorithms and software

• Hirshman83. S. P. Hirshman and J. C. Whitson (1983), Steepest-descent moment method for three-dimensional magnetohydrodynamic equilibria, Physics of Fluids 26, 3553–3568. DOI: 10.1063/1.864116. VMEC's variational/computational starting point. Nested-surface assumptions and a computed stationary point do not supply continuum existence or stability.

• REGCOIL17. M. Landreman (2017), An improved current potential method for fast computation of stellarator coil shapes, Nuclear Fusion 57, 046003. arXiv:1609.04378; official documentation. Surface-current inverse design and regularization. Keep normal-field mismatch, current density, and realizable finite-coil geometry as separate quantities.

• Coils22. F. Wechsung, M. Landreman, A. Giuliani, A. Cerfon, and G. Stadler (2022), Precise stellarator quasi-symmetry can be achieved with electromagnetic coils, PNAS 119, e2202084119. Primary article; reproduction repository. Useful candidate-generation and finite-coil examples. Recheck continuous clearance, finite conductor field, tolerance, and orbit claims.

• SingleStage22. A. Giuliani, F. Wechsung, A. Cerfon, G. Stadler, and M. Landreman (2022), Single-stage gradient-based stellarator coil design: Optimization for near-axis quasi-symmetry. Publisher article. Shows an optimization route coupling coil design and near-axis objectives; optimizer convergence is evidence about a candidate rather than a proof certificate.

• Direct23. A. Giuliani, F. Wechsung, A. Cerfon, M. Landreman, and G. Stadler, Direct stellarator coil optimization for nested magnetic surfaces with precise quasi-symmetry. arXiv:2210.03248. Check the nested-surface representation and residual measure before choosing what to certify.

• DESC23. D. Panici, R. Conlin, D. W. Dudt, K. Unalmis, and E. Kolemen (2023), The DESC stellarator code suite. Part 1. Quick and accurate equilibria computations, Journal of Plasma Physics 89, 955890303. DOI: 10.1017/S0022377823000272; arXiv:2203.17173. An equilibrium candidate generator with explicit discretization conventions, not a checked continuum proof.

Official implementation/documentation entry points:

Pin versions and read their conventions. None is automatically part of the trusted Lean theorem path.

Engineering, materials, and experiment

• KMM16. J. Knaster, A. Moeslang, and T. Muroga (2016), Materials research for fusion. DOI: 10.1038/nphys3735; author-institution record. Map irradiation, thermal, and mechanical challenges to material-law inputs and explicit validity limits.

• DEMO18. J.-H. You et al. (2018), European divertor target concepts for DEMO: Design rationales and high heat flux performance, Nuclear Materials and Energy 16, 1–11. DOI: 10.1016/j.nme.2018.05.012; author-institution record. A concrete source for component models, cooling concepts, and load tests. Transfer a numerical limit only with the original geometry/material/operation assumptions.

• REBCO25. P. Huslage et al. (2025), Strain optimisation for ReBCO high-temperature superconducting stellarator coils in SIMSOPT, Journal of Plasma Physics 91, E71. DOI: 10.1017/S0022377825000224; arXiv:2409.01925. Source for tape-frame, hard-way bending, and torsion objectives. Full conductor critical-surface, irradiation, pack mechanics, and quench constraints still require additional data/models.

• HELIAS13. F. Schauer et al. (2013), HELIAS 5-B magnet system structure and maintenance concept. DOI: 10.1016/j.fusengdes.2013.01.035; author-institution record. Reactor magnet/support/maintenance integration; source design-specific requirements instead of imposing universal clearances.

• W7X-transport21. C. D. Beidler et al. (2021), Demonstration of reduced neoclassical energy transport in Wendelstein 7-X, Nature 596, 221–226. DOI: 10.1038/s41586-021-03687-w; primary article. Validation evidence for selected transport predictions and regimes, not a theorem for arbitrary future stellarators.

• W7X-divertor21. M. Jakubowski et al. (2021), Overview of the results from divertor experiments with attached and detached plasmas at Wendelstein 7-X and their implications for steady-state operation, Nuclear Fusion 61, 106003. DOI: 10.1088/1741-4326/ac1b68; author-institution record. Source edge/exhaust operating envelopes and their measured conditions.

• BH92-reactivity. H.-S. Bosch and G. M. Hale (1992), Improved formulas for fusion cross-sections and thermal reactivities, Nuclear Fusion 32, 611–631. Original DOI; 1993 corrigendum. Useful fit for a declared fuel/temperature domain. Preserve units, species conventions, coefficients, and fit uncertainty; do not treat the fit as an exact physical law.

• FENDL-data. IAEA, Fusion Evaluated Nuclear Data Library. Pin the dataset release, nuclide files, processing, energy groups, and response definitions. Evaluated cross sections are supplied physical data; a deterministic proof needs declared envelopes, while a probabilistic claim needs its statistical assumptions.

These references establish starting points rather than a complete component qualification dataset. For a chosen material/device, additionally retrieve the primary conductivity, critical-current, fracture/fatigue, irradiation, coolant, and joint data. Formalize the envelope interpretation before consuming it in a design proof.

Reading order and theorem targets

Use 08-roadmap.md to select a milestone. Existing literature supports substantial parts of the program; the research targets require separate novelty review and new mathematics where the available hypotheses or quantitative conclusions fall short.