# PlasmaLean Rosetta Stone: Stellarator Physics ↔ Pure Geometry ↔ Lean 4 Kernel
This reference maps standard magnetic confinement fusion terminology into coordinate-free **Topology**, **Differential Geometry**, and **Complex Geometry**, alongside the corresponding **Lean 4** kernel declarations in `PlasmaLean`.
| Stellarator Physics Concept | Pure Mathematical Formulation (Topology / Diff. & Complex Geometry) | Lean 4 Kernel Contract / Signature |
| :--- | :--- | :--- |
| **Magnetic Flux Surface (ψ = const)**
_A toroidal surface inside the plasma onto which magnetic field lines B are everywhere tangent (B · ∇ψ = 0), confining nested layers of plasma pressure._ | **[Topology & Foliations]**
Compact connected regular level set Σ_c = ψ⁻¹(c) ≅ T² of a smooth first integral ψ : M → ℝ of a nowhere-vanishing divergence-free vector field B (Lie derivative ℒ_B ψ = 0). By Poincaré–Hopf, χ(Σ_c) = 0 forces Σ_c to be a 2-torus. | `structure IsFluxSurface (B : VectorField ℝ³) (ψ : ℝ³ → ℝ) (c : ℝ) : Prop where
is_regular : ∀ x ∈ ψ ⁻¹' {c}, fderiv ℝ ψ x ≠ 0
compact_connected : IsCompact (ψ ⁻¹' {c}) ∧ IsConnected (ψ ⁻¹' {c})
tangent_field : ∀ x ∈ ψ ⁻¹' {c}, ⟪B x, grad ψ x⟫_ℝ = 0` |
| **Solenoidal Magnetic Field (∇ · B = 0)**
_Absence of magnetic monopoles; magnetic flux through any closed surface vanishes._ | **[Differential Geometry]**
Closed 2-form ω_B = ι_B vol_g ∈ Ω²(M) satisfying dω_B = 0, or co-closed 1-form β = B^♭ satisfying d*β = 0. On contractible domains or via de Rham cohomology H²(M), ω_B = dα for a magnetic vector potential 1-form α ∈ Ω¹(M). | `def IsSolenoidal (B : ℝ³ → ℝ³) : Prop :=
∀ x : ℝ³, divergence B x = 0
structure MagneticTwoForm (M : Type*) [SmoothManifold M] where
ω : DifferentialForm M 2
is_closed : extDeriv ω = 0` |
| **Vacuum Magnetic Field (∇ · B = 0, ∇ × B = 0)**
_Magnetic field in the current-free region outside coils (J = 0), determined purely by external coil currents and toroidal/poloidal periods._ | **[Differential & Complex Geometry]**
Harmonic 1-form β ∈ ℋ¹(M, g) on a Riemannian 3-manifold with toroidal boundary (dβ = 0 and d*β = 0, hence Δ_H β = 0). By Hodge–Morrey–Friedrichs decomposition, the space of vacuum fields with tangent boundary conditions is isomorphic to H¹_dR(M; ℝ) ≅ ℝ^g. | `structure IsVacuumField (U : Set ℝ³) (B : ℝ³ → ℝ³) : Prop where
open_domain : IsOpen U
div_zero : ∀ x ∈ U, divergence B x = 0
curl_zero : ∀ x ∈ U, curl B x = 0` |
| **Rotational Transform ι(ψ) and Safety Factor q = 1/ι**
_Average number of poloidal turns a magnetic field line makes per toroidal turn around a flux surface._ | **[Topology & Dynamical Systems]**
Poincaré rotation number ρ(f_ψ) ∈ ℝ / ℤ of the orientation-preserving circle diffeomorphism f_ψ : S¹ → S¹ induced by the first-return map of the flow of B on a transverse poloidal section Σ_φ₀ ∩ ψ⁻¹(c). Irrational Diophantine ι guarantees dense ergodic orbits (KAM tori); rational ι = n/m permits resonant island chains. | `noncomputable def RotationalTransform
(flowMap : S1 → S1) (h_lift : ℝ → ℝ) : ℝ :=
limUnder atTop (fun n : ℕ => (h_lift^[n] 0) / (n : ℝ))` |
| **Magnetohydrostatic (MHS) Equilibrium (J × B = ∇p)**
_Macroscopic force balance where Lorentz magnetic forces balance the plasma kinetic pressure gradient._ | **[Differential & Symplectic Geometry]**
Stationary Euler-like equation ι_B dβ = dp (where β = B^♭ and J = ⋆dβ). Equivalently, B and J lie in the kernel of dp, forcing both vector fields to commute along level sets of p in Hamada coordinates. When ∇p = 0, reduces to a Beltrami field ⋆dβ = λβ (contact geometry when λ ≠ 0). | `structure IsMHSEquilibrium (B J : ℝ³ → ℝ³) (p : ℝ³ → ℝ) : Prop where
ampere_law : ∀ x, curl B x = μ₀ • J x
div_free : ∀ x, divergence B x = 0
force_balance : ∀ x, crossProduct (J x) (B x) = grad p x` |
| **Boozer Coordinates (ψ, θ_B, φ_B)**
_Special magnetic flux coordinates in which magnetic field lines are straight AND the covariant representation of B involves only surface quantities._ | **[Differential Geometry]**
Canonical coordinate chart on a foliated Riemannian 3-manifold (M, g) adapted to the foliation ψ such that the pullback of both the closed 2-form ω_B = dψ ∧ (dθ_B - ι(ψ) dφ_B) (contravariant straightness) and the 1-form β = I(ψ) dθ_B + G(ψ) dφ_B + ν(ψ,θ_B,φ_B) dψ (covariant periods) have surface-constant coefficients. | `structure BoozerChart (U : Set ℝ³) where
ψ : ℝ³ → ℝ
θ : ℝ³ → Real.Angle
φ : ℝ³ → Real.Angle
ι G I : ℝ → ℝ
covariant_rep : ∀ x ∈ U, B_oneForm x =
G (ψ x) • dφ x + I (ψ x) • dθ x + ν x • dψ x
contravariant_rep : ∀ x ∈ U, B_twoForm x =
wedge (dψ x) (dθ x - ι (ψ x) • dφ x)` |
| **Quasisymmetry (QA, QH, QP)**
_Hidden 3D symmetry where the magnetic field strength |B(ψ, θ_B, φ_B)| = B(ψ, Mθ_B - Nφ_B) depends only on a single helical angle combination in Boozer coordinates, restoring guiding-center conservation laws._ | **[Differential & Symplectic Geometry]**
Existence of a nowhere-vanishing vector field u on M (a 'flux-surface symmetry' rather than an ambient Euclidean Killing field) such that: (1) ℒ_u ψ = 0 (tangent to flux surfaces), (2) ℒ_u |B| = 0 (preserves field magnitude), and (3) ℒ_u ω_B = 0 (preserves magnetic flux 2-form). Generates a conserved momentum P_u via Noether's theorem for guiding-center Hamiltonian dynamics. | `structure IsQuasisymmetric (bc : BoozerChart U) (B_mag : ℝ³ → ℝ)
(M N : ℤ) (hMN : M ≠ 0 ∨ N ≠ 0) : Prop where
helical_invariance : ∃ f : ℝ → Real.Angle → ℝ,
∀ x ∈ U, B_mag x = f (bc.ψ x) (M • bc.θ x - N • bc.φ x)` |
| **Near-Axis Expansion (Garren–Boozer / Landreman–Sengupta)**
_Asymptotic power-series construction of 3D MHD equilibria and quasisymmetric fields in powers of distance r = √ψ from a closed 3D curve (the magnetic axis)._ | **[Differential Geometry of Curves]**
Jet expansion in tubular neighborhood coordinates (s, x₁, x₂) around an embedded closed curve γ : S¹ → ℝ³ with curvature κ(s) > 0 and torsion τ(s) (or parallel Bishop frame). First-order quasisymmetry reduces to a nonlinear periodic ODE (Riccati equation) for the rotating cross-section ellipse eccentricity σ(s) driven by κ(s) and τ(s). | `structure MagneticAxis where
γ : ℝ → ℝ³
periodic : Function.Periodic γ L
unit_speed : ∀ s, ‖deriv γ s‖ = 1
curvature_pos : ∀ s, ‖deriv (deriv γ) s‖ > 0` |
| **Guiding-Center Drift Motion & Bounce Invariant J_∥**
_Averaged trajectory of a charged particle gyrating rapidly around magnetic field lines, subject to ∇B and curvature drifts._ | **[Symplectic & Poisson Geometry]**
Hamiltonian system (P, Ω_GC, H_GC) on a 4D phase space P = M × ℝ_v∥ equipped with Littlejohn's non-canonical symplectic 2-form Ω_GC = e dA + m d(v_∥ b^♭) and Hamiltonian H_GC = ½ m v_∥² + μ |B| + e Φ. The longitudinal adiabatic invariant J_∥ = ∮ v_∥ dl is the action integral along trapped-particle orbits. | `structure GuidingCenterSystem (M : Type*) [SmoothManifold M] where
Ω_GC : DifferentialForm (M × ℝ) 2
symplectic : extDeriv Ω_GC = 0 ∧ IsNonDegenerate Ω_GC
H_GC : M × ℝ → ℝ` |
| **Ideal MHD Stability & Bernstein Energy Principle (δ²W > 0)**
_Variational criterion stating an equilibrium is linearly stable to ideal MHD modes iff every physical plasma displacement ξ increases potential energy δ²W(ξ, ξ) > 0._ | **[Spectral Geometry & Calculus of Variations]**
Positivity (coercivity) of the Hessian quadratic form δ²W(ξ, ξ) = -½ ∫_M ⟨ξ, F(ξ)⟩ vol_g of the magnetic + internal energy functional restricted to a single coadjoint orbit of the infinite-dimensional Lie group SDiff(M) of volume-preserving diffeomorphisms. F is a formally self-adjoint second-order partial differential operator. | `def IsLinearlyMHDStable (δ2W : DisplacementField → ℝ) : Prop :=
∀ ξ : DisplacementField, ξ ≠ 0 → δ2W ξ > 0` |
| **Non-Overlapping Flux Surfaces & Positive Jacobian (√g > 0)**
_Requirement that nested flux surfaces parameterized by double Fourier series R(s,θ,φ), Z(s,θ,φ) do not self-intersect or fold over inside the plasma volume._ | **[Complex Geometry & Harmonic Mappings]**
Strict positivity of the Jacobian determinant det(DΦ) > 0 for the diffeomorphism Φ : D² × S¹ → M. Slice-by-slice in φ, certifying that a Fourier-series map from the unit disk D² ⊂ ℂ to the poloidal cross-section is a diffeomorphism reduces to univalence criteria for planar harmonic/quasiconformal maps (Radó–Kneser–Choquet theorem, Becker/Nehari bounds, and Hardy space H^∞ analytic continuation). | `def ValidFluxCoordinateMap (Φ : PolarToroidalDomain → ℝ³) : Prop :=
Injective Φ ∧ ∀ x ∈ interiorDomain, (jacobianDet Φ x) > 0` |
| **Biot–Savart Law & Field Derivatives for 3D Coils**
_Integral formula computing B(x) and its spatial/shape derivatives from 3D filamentary current loops γ_i._ | **[Integral Geometry & Operator Calculus]**
Singular integral operator linking 1-chains (closed curves γ_i) to harmonic 1-forms on ℝ³ \ ∪ im(γ_i): B(x) = (μ₀ I / 4π) ∮ (γ'(s) × (x - γ(s))) / |x - γ(s)|³ ds. Its topological invariant with another loop C is the Gauss linking integral Lk(γ, C). Fréchet derivatives w.r.t. coil perturbations δγ control manufacturing tolerance certificates. | `noncomputable def biotSavartKernel (x y tangent : ℝ³) : ℝ³ :=
(‖x - y‖ ^ 3)⁻¹ • crossProduct tangent (x - y)
theorem biotSavart_lipschitz_on_clearance
(h_dist : ∀ s, ‖x - γ s‖ ≥ d_min) (hd : d_min > 0) :
‖fderiv ℝ (biotSavartField x) γ‖ ≤ C_bound / d_min ^ 3` |
| **Coil Complexity: Maximum Curvature κ_max & Minimum Clearance d_min**
_Engineering constraints ensuring 3D HTS superconducting magnets can be wound without strain damage and mounted without colliding._ | **[Metric & Submanifold Geometry]**
Upper bound on geodesic/extrinsic curvature κ(s) ≤ κ_max and positive lower bound on the Federated 'reach' (tubular neighborhood injectivity radius) reach(∪ γ_i) ≥ r_tube > 0. By Federer's reach theorem, the normal bundle map of radius r < reach(γ) is an embedding. | `structure ConstructibleCoilSet (coils : Fin n → SpaceCurve) : Prop where
curvature_bound : ∀ i s, curvature (coils i) s ≤ κ_max
coil_clearance : ∀ i j s t, i ≠ j →
‖(coils i).γ s - (coils j).γ t‖ ≥ d_coil_min` |
| **Flux-Surface Metric & Susceptibility Matrix**
_Geometric coefficients relating poloidal/toroidal magnetic fluxes to currents on each nested toroidal surface._ | **[Complex Geometry (Riemann Surfaces)]**
The induced Riemannian metric g|_{Σ_ψ} defines a conformal structure on T², turning each flux surface into a 1D complex torus (elliptic curve) ℂ / (ℤ + τ(ψ)ℤ) with modular parameter τ(ψ) ∈ ℍ (upper half-plane). The Hodge star ⋆_Σ on 1-forms depends only on the conformal class τ(ψ), determining the 2×2 period/inductance matrix. | `structure ConformalTorusMetric (Σ : Type*) [TopologicalSpace Σ] where
τ : UpperHalfPlane
isothermal_chart : Σ → ℂ ⧸ Lattice2D 1 τ` |
| **Omnigeneity & Maximum-J Criterion (∂_ψ J_∥ < 0)**
_Condition that bounce-averaged radial drift of trapped particles vanishes (∂_α J_∥ = 0) and radial derivative is negative (∂_ψ J_∥ < 0), stabilizing Trapped Electron Mode (TEM) microturbulence._ | **[Symplectic Geometry & Action-Angle Theory]**
In Clebsch coordinates B = ∇ψ × ∇alpha, longitudinal action integral J_∥ = m v ∫ sqrt(1 - λ B) dl generates bounce-averaged guiding-center motion via symplectic form q dψ ∧ dalpha. Omnigeneity requires ∂_α J_∥ = 0; Maximum-J requires strict radial monotonicity ∂_ψ J_∥ < 0. | `structure IsMaximumJ (J_par : ℝ → ℝ → ℝ → ℝ) (U_trap : Set (ℝ × ℝ × ℝ)) : Prop where
omnigenous : ∀ ⟨ψ, α, λ⟩ ∈ U_trap, deriv (fun α' => J_par ψ α' λ) α = 0
radial_dec : ∀ ⟨ψ, α, λ⟩ ∈ U_trap, deriv (fun ψ' => J_par ψ' α λ) ψ < 0` |
| **Available Energy of Microturbulence (A / Æ)**
_Thermodynamic upper bound on thermal plasma energy convertible into nonlinear drift-wave / TEM turbulent fluctuations under phase-space rearrangements._ | **[Optimal Transport & Symplectic Rearrangements]**
Available Energy A = ∫ E (f_0 - f_ground) dΓ is the supremum of extractable energy under volume-preserving rearrangements preserving adiabatic invariants (μ, J_∥). Reduces in thin flux tubes to an explicit positive-part integral over pitch angle of Theta(omega_* (omega_* - omega_alpha)). | `noncomputable def AvailableEnergyFluxTube
(ω_star ω_drift : PitchAngle → ℝ) (measure_λ : Measure PitchAngle) : ℝ :=
∫ λ, max 0 (ω_star λ * (ω_star λ - ω_drift λ)) ∂measure_λ` |