PlasmaLean Mathematical Exposition & Contributor Suite
PlasmaLean is an attempt to design a practical stellarator using Lean 4 verification to guarantee physical, geometric, and engineering correctness. By isolating core physical contracts and sanity checks into a small, human-auditable verification kernel, both human mathematicians and AI theorem-proving agents can build machine-checked stability and coil-tolerance certificates without specification drift.
The Four Pillar Expositions
Designed for drop-in integration with siddhartha-gadgil.github.io/PlasmaLean/, this suite bridges plasma physicists, Lean 4 formalizers, and pure mathematicians in topology, differential geometry, and complex geometry.
1. Physics ↔ Geometry ↔ Lean 4 Rosetta Stone
A searchable, filterable 3-way dictionary mapping 16 foundational stellarator physics concepts (flux surfaces, rotational transform $\iota$, Boozer coordinates, quasisymmetry, Bernstein $\delta^2 W$, Biot-Savart) into coordinate-free differential/complex geometry and exact Lean 4 kernel types.
2. Interactive Blueprint Dependency DAG
An interactive directed acyclic graph spanning all 12 handbook workstreams. Inspect every node to see its mathematical formulation, Lean 4 declaration signature, assumption ledger dependencies, and compilation status (Kernel Contract, Sanity Check, Compiled Proof, or Open Target).
3. Audit the Small Kernel in 10 Minutes
Why do we trust AI-generated or complex formal proofs of plasma stability? Because they target a tiny, self-contained kernel. Walk line-by-line through the core definitions and the non-vacuity sanity checks that prevent subtle specification bugs.
4. Anatomy of a Vacuum-Fixture Certificate
Follow a compiled physical guarantee from start to finish: from 3D modular coil curves $\gamma_i : S^1 \to \mathbb{R}^3$, through Fréchet derivatives of the Biot-Savart operator, to a verified interval certificate under $\epsilon$-manufacturing tolerances.
Onboarding Pure Mathematicians (Topology, Differential & Complex Geometry)
Foliations, Linking & Converse KAM
Magnetohydrostatic equilibria foliate 3-manifolds by nested 2-tori $T^2$. Contribute proofs on Poincaré-Hopf toroidal regularity, Gauss linking integrals for modular coils, and MacKay Converse KAM non-existence criteria for chaotic field regions.
View Topology Challenges →Hodge Theory, Beltrami Fields & Curves
Vacuum fields are harmonic 1-forms ($d\beta=0, d^*\beta=0$); force-free states are Beltrami contact forms ($\star d\beta = \lambda \beta$). Contribute proofs on Bishop frames for near-axis quasisymmetry, tubular reach bounds, and Littlejohn's guiding-center symplectic 2-form.
View Differential Geometry Challenges →Riemann Surfaces & Univalent Foliations
Each flux surface $\Sigma_\psi \cong \mathbb{C}/(\mathbb{Z} + \tau(\psi)\mathbb{Z})$ carries a complex modulus $\tau(\psi) \in \mathbb{H}$. Contribute proofs on Radó-Kneser-Choquet univalence for non-degenerate flux coordinate Jacobians and Hardy-space Fourier decay bounds.
View Complex Geometry Challenges →Repository Integration Map
| File in Suite | Format | Role in PlasmaLean Website / Repo |
|---|---|---|
rosetta-stone.html / markdown/ROSETTA_STONE.md |
Interactive HTML + Markdown | Links from index.html & handbook.html as the terminology bridge. |
blueprint-dag.html |
Interactive SVG DAG + Inspector | Embeds into or complements progress.html and roadmap.html. |
kernel-audit.html / markdown/KERNEL_AUDIT_GUIDE.md |
Split-Pane Audit + Markdown | Complements model-contracts.html and domain-library.html. |
certificate-anatomy.html / markdown/CERTIFICATE_WALKTHROUGH.md |
5-Stage Walkthrough + Calculator | Directly illustrates vacuum-demonstrator.html & verified-numerics.html. |
math-challenges.html + lean_stubs/*.lean |
Challenge Portal + 6 Lean 4 Files | Self-contained onboarding tasks for geometers & topologists. |
slides-onboarding.html |
Reveal.js Interactive Presentation | Colloquium & contributor slide deck alongside slides.html. |