Outcome
This run moves the library from a vacuum calibration fixture to exact finite-pressure MHD equilibria with all-time confinement theorems, plus the first stability criteria with both sufficiency and necessity. Twenty-one new Lean modules add 443 source theorems (including helpers). Highlights:
- Maxwell identities. The closed-filament Biot–Savart field satisfies ∇·B = 0 and ∇×B = 0 away from the coil, for the actual Fréchet derivative of the continuous integral. The run-2 boundary obligation is closed.
- Local interchange stability. A sharp Hardy inequality yields the Suydam criterion for the model radial form, both ways: sufficiency with a coercive margin, and an explicit unstable mode in every neighbourhood of the resonance when it fails. Newcomb/Picone/Riccati certificates generalize this to variable coefficients. An exact rational polynomial interval checker, run by the kernel without
native_decide, discharges such certificates. - Equilibria satisfying the domain-kernel law
ForceBalance(J × B = ∇p with the actual Ampère current): - an exact toroidal Solov'ev equilibrium (axisymmetric; ITER-like scale R₀ = 6 m, B = 5 T, β_axis = 147/5000);
- an exact helically symmetric, nonaxisymmetric equilibrium (straight-stellarator model; 5 T, β_axis = 4%, pitch length 2 m).
- Confinement for all time. Noether conservation of canonical momentum for any Killing symmetry, together with an intermediate-value trapping lemma, proves that every full Newton–Lorentz orbit below a stated rigidity stays in a stated flux region forever, in both equilibria. Field lines are confined by exact first integrals.
- Imperfect symmetry. A symmetry defect δ gives confinement for an explicit time ∝ 1/(δ|v|) (a ripple example). The run also records that this crude bound is far from reactor-relevant.
- Screw-pinch design. A realistic cylindrical screw pinch (a = 1 m, R₀ = 4 m, B ≈ 5 T, ⟨β⟩ = 2/75) satisfies Suydam's criterion everywhere with a 25% relative margin and q ≥ 5/4.
This is not a practical stellarator design. No configuration here is produced by coils, and the symmetric models exclude toroidal curvature (helical case) or nonaxisymmetry (Solov'ev case). For the cylindrical screw pinch, Newcomb-reduced ideal δW ≥ 0 is certified for all modes with 1 ≤ |m| ≤ 6 (wall at the edge), but not yet uniformly in m. No all-mode or global MHD stability certificate exists for the Solov'ev or helical equilibria. Gate status: P2 remains partial. P3 (confined reduced orbits) and P4 (finite-pressure equilibrium) now have checked instances in idealized symmetric models, not for a coil-produced stellarator. P5 has local (Suydam) and certificate-based (Newcomb) building blocks only.
Baseline checkout: b8641a11c5d9e8bfde98b3ef2711a327084890f2. Lean and Mathlib remain v4.34.1; there is no dependency change. The domain kernel (Kernel/*.lean) was re-audited and needed no correction or addition; every new equilibrium is checked against the existing ForceBalance class. No solver or floating-point output enters any proof. Python/sympy were used only to search for candidates (equilibrium ansätze, profile parameters, Jacobi polynomial certificates).
Implementation loops
- Re-audited the kernel, last report and roadmap. The selected targets were the Maxwell gap, local stability, field-line barriers and full-orbit dynamics, developed in parallel.
- Maxwell identities for filament fields (divergence and curl operators with sanity lemmas; FTC along the closed curve).
- Hardy inequality → Suydam sufficiency, sharpness and necessity (logarithmic test mode).
- First integrals and field-line barriers; a nonaxisymmetric analytic Clebsch torus. It was then shown to be divergence-free but not a vacuum field: its curl is nonzero throughout the region. One planned claim was corrected; see below.
- Newton–Lorentz energy conservation, exact gyration and realistic Larmor radii.
- Newcomb/Picone/Riccati certificates; an exact polynomial interval checker with soundness, wired to the certificates.
- Screw-pinch force balance, safety factor and Suydam criterion, with a realistic Suydam-stable exact profile.
- Canonical toroidal momentum: an all-time band, IVT trapping, a symmetry defect and a first-exit bootstrap for finite-time confinement.
- Observation: the polynomial flux function satisfies Δ*ψ = 3R², i.e. it is a Solov'ev Grad–Shafranov solution. This led to an exact toroidal equilibrium verified against the kernel, with an SI instance.
- Noether conservation for Killing fields; a helically symmetric rotating-ellipse field; then an exact helical ideal-MHD equilibrium found by symbolic search, ∇·B = 0, kernel force balance, and an SI reactor-scale instance.
- Newcomb (m,k) mode analysis of the screw-pinch example: coefficients extracted from Newcomb 1960 / Glasser et al. 2020 (Eq. 2) and cross-checked against Freidberg's form and the Suydam limit (weight Bθ²/B² recovered exactly). Every mode with 1 ≤ |m| ≤ 6 and every integer n is certified, by kernel-checked Picone certificates (9 resonant/kink-candidate modes) and potential checks (18 modes), plus uniform families.
New checked results
Names omit PlasmaLean.. Space is Euclidean ℝ³ with the Euclidean norm. All orbit results take a supplied classical Newton–Lorentz trajectory (non-relativistic, static fields, no collisions or radiation); existence of trajectories is not proved.
| Topic | Declarations | Assumptions and scope | ||
|---|---|---|---|---|
| Maxwell identities | Fields.filamentField_divergence, filamentField_curl, filamentField_vacuum_maxwell, filamentField_curl_open | Continuous source and tangent on [a,b]; source avoided; curl needs closure c a = c b and two-sided differentiability at the endpoints; the open-segment curl is computed exactly | ||
| Hardy/Suydam | Stability.hardy, hardy_sharp, suydamForm_coercive, suydam_necessary, suydam_unstable_near_resonance | Constant coefficients F, G; C¹ displacements vanishing at the ends; the model localized form, not a derivation from full δW | ||
| Newcomb certificates | Stability.picone_certificate, riccati_certificate, jacobi_certificate, suydam_from_picone | f ≥ 0 and continuous; φ = f·w may be singular-free at resonances; the necessity (Sturm) direction is not proved | ||
| Exact checker | Certificates.QPoly.checkOn_sound, riccati_poly_certificate, jacobi_poly_certificate, example_beyond_constant | Rational coefficient lists; first-order lower bound per piece; fixtures by decide +kernel | ||
| Field-line barriers | Fields.firstIntegral_conserved_forward, sublevel_confined, fieldLine_bounded, clebsch_divergence_free, uniform_no_bounded_firstIntegral | Supplied forward field lines; C² potentials for divergence | ||
| Clebsch torus | Design.ClebschTorus.fieldLine_stays_in_torus, field_divergence_free, field_not_vacuum, field_not_axisymmetric | Analytic, dimensionless, not coil-produced, not curl-free | ||
| Full orbits | Kinetic.energy_conserved, speed_conserved, helix_orbit, alpha_3_5MeV_5T | Electrostatic potential with ∇Φ = −E; supplied CODATA-rounded constants | ||
| Canonical momentum | Kinetic.canonicalMomentum_conserved, flux_band, trapped_of_gap, orbit_trapped, trapped_until, orbit_trapped_until | Explicit AxisymmetricFlux/FluxDefectOn hypotheses; E = 0 | ||
| Noether | Kinetic.noetherMomentum_conserved, noether_orbit_trapped, noether_orbit_trapped_until, symmetricFlux_of_cross, helicalK_killing | Killing field with antisymmetric derivative; ‖K‖ bounded on the region (z may be unbounded) | ||
| Polynomial tokamak | Design.PolyTokamak.orbit_confined, ripple_orbit_confined, ripple_not_axisymmetric | Dimensionless; rigidity ≤ 1/64; ripple confinement for 2 | ε | ‖v‖T ≤ 1/384 |
| Solov'ev equilibrium | Design.Solovev.force_balance, field_divergence_free, field_flux_tangent, current_flux_tangent, orbit_confined, iter_like_beta, iter_like_deuteron_confined | Off the vertical axis (R ≠ 0); axisymmetric; not matched to coils or a vacuum region | ||
| Screw pinch | Equilibrium.ScrewPinch.local_criterion, localized_stable, localized_unstable, Design.ScrewPinchExample.suydam_margin, safetyFactor_ge, beta_eq | Cylindrical balance law supplied (not derived from the 3-D kernel); Suydam is necessary, not sufficient | ||
| Helical equilibrium | Design.HelicalFamily.field_divergence_free, Design.HelicalEquilibrium.force_balance, orbit_confined, field_not_axisymmetric, Design.HelicalReactorScale.scaled_force_balance, reactor_beta_axis, reactor_deuteron_confined, reactor_alpha_confined | Straight helical symmetry (no toroidal curvature); claims restricted to ψ ≤ ψ_b, where p ≥ 0 | ||
| Screw-pinch modes | Stability.ScrewPinchModes.coefF_textbook, coefG_textbook, suydam_limit_weight, picone_lower, NewcombReduction.energy_nonneg, Design.ScrewPinchModes.stable_low_m, stable_uniform, mode_1n1 | Newcomb reduction supplied as an interface; fixed boundary, wall at the plasma edge; δW ≥ 0 (no coercive margin); m = 0 excluded; uncovered: | m | ≥ 7 with km < 0 and 5n² < 9m² |
Quantitative certificates
| Quantity | Verified result | ||||
|---|---|---|---|---|---|
| Larmor radius, 10 keV D at 5 T | < 4.1 mm | ||||
| Larmor radius, 3.5 MeV α at 5 T | between 5.3 and 5.5 cm | ||||
| Hardy constant | 4, sharp (hardy_sharp) | ||||
| Suydam log-mode energy | (π/(2k))(Fk² + F/4 + G), exactly | ||||
| Newcomb example, f = 1 + x², g = −21/2 | Q ≥ ∫ξ², via a degree-12 exact Jacobi certificate (beyond the constant-coefficient bound) | ||||
| Screw pinch (a = 1 m, R₀ = 4 m) | Bz(0) = 5 T; ⟨β⟩ = 2/75; Suydam shear term ≥ 1.25 × pressure drive on (0,1]; q ≥ 5/4; I_p between 2.49 and 2.51 MA | ||||
| Solov'ev (R₀ = 6 m) | B_axis = 5 T; β_axis = 147/5000; axis pressure between 292.0 and 292.6 kPa; plasma 4.24 m ≲ R ≲ 7.35 m | ||||
| Solov'ev orbits | Deuterons ≤ 400 keV starting in the inner region confined for all time; alphas ≤ 800 keV satisfy the rigidity hypothesis | ||||
| Helical equilibrium (L = 2 m) | B_axis = 5 T; β_axis = 1/25; peak pressure between 397.8 and 397.9 kPa; covered orbits stay at r < 0.71 m for all time | ||||
| Helical orbits | Deuterons ≤ 30 keV, alphas ≤ 60 keV | ||||
| Screw-pinch Newcomb modes (k = n/4) | ModeStable for all 1 ≤ | m | ≤ 6, all n ∈ ℤ; and every mode with km ≥ 0, | m | ≥ 2 or 5n² ≥ 9m² |
| Ripple (polynomial tokamak) | Confinement while 2 | ε | ‖v‖T ≤ 1/384 (dimensionless) |
Obstruction recorded. 3.5 MeV fusion alphas are not covered in either equilibrium. In the Solov'ev case their normalized rigidity is about 1/31, against the 1/64 required. The crude canonical-momentum band confines them only to ψ̃ ≲ 0.16, beyond the pressure boundary ψ̃ = 1/16. Under symmetry breaking, the full-orbit defect bound gives times ∝ 1/(δ|v|), a ballistic time scale far shorter than slowing-down times. Practical alpha confinement in a quasisymmetric stellarator needs guiding-centre averaging and orbit-width theory (roadmap R4, R6).
Corrections and challenged claims
- The Clebsch-torus field was first planned to have positive vertical curl throughout its region. That is false: the vertical curl changes sign at R² = 4/3, inside the region. Non-vacuum status is proved with the horizontal components instead.
- The screw-pinch exploration showed that p ∝ (1 − r²) or (1 − r²)² always violates Suydam near the axis, because p′ ∼ r while the shear term ∼ r³. The certified profile uses p ∝ (1 − r⁴).
- The helical equilibrium formula continues to negative pressure outside ψ_b. Setting p = 0 there with the same field is not an equilibrium, since (∇×B)×B ≠ 0, so a current sheet and a different exterior field would be needed. Claims are restricted to ψ ≤ ψ_b, which the covered orbits never leave. The orbit hypothesis is still stated for the smooth field on all of space.
- A helically symmetric rotating-ellipse family with F = −2ψ is also an equilibrium, but its field vanishes on the axis. The run used the second family (F = 4 + 2ψ, μ₀p′ = −4).
Assumption ledger
| Assumption | Kind | Where |
|---|---|---|
ForceBalance (J × B = ∇p) | Kernel model law (unchanged) | All equilibria are checked against it, with J = curl B/μ₀ from actual derivatives |
| Cylindrical radial balance | Supplied reduction (Freidberg) | Equilibrium.ScrewPinch.RadialBalance; derivation from the kernel is not formalized |
| Localized δW reduction to F x²ξ′² + Gξ² | Source result (Suydam 1958, Newcomb 1960), not formalized | Weight c = Bθ²/B², recovered from the Newcomb coefficients |
| Newcomb radial δW per (m,k) | Source result (Newcomb 1960; Glasser et al. 2020, Eq. 2), interface NewcombReduction | Cross-checked with Freidberg's form and the Suydam limit |
| Newton–Lorentz model | Model definition | Kinetic.LorentzOrbit; trajectories supplied |
| Physical constants (masses, e, μ₀ bounds) | Supplied rounded data | Explicit numerals in the theorem statements |
| Density 10²⁰ m⁻³ in temperature estimate | Illustrative input | ScrewPinchExample.peak_temperature |
Earlier results retained
All earlier results are still imported and building: force-balance/slab witnesses, energy/form lemmas, interval and block checkers, the contraction example, the synthetic thermal slab margin (998/45 K below an invented 1000 K limit), and the tolerance-aware two-coil vacuum fixture. That fixture has field-error budget μ₀I/4, a nonzero axial field in the 1 mm probe ball, 388 mm envelope clearance and a probe residence bound. The detailed fixture report remains in progress/2026-10-12-progress-2.md. Its synthetic inputs are still not material or hardware qualification data.
Validation
Final checks:
lake build: 2850 jobs, no warnings. 53 Lean modules underPlasmaLean/; 618 source theorems including private helpers.lake env lean scripts/check_axioms.lean: all 1730 project-owned declarations audited, using onlypropext,Classical.choiceandQuot.sound. New entry points also have explicit#print axiomslines.- Source scan: no
sorry,admit, projectaxiom,native_decideorunsafe. Kernel fixtures usedecide +kernel(plain kernel reduction). node scripts/generate_handbook.mjsandnode scripts/check_site.mjs: passed (see the end of this run).
Next boundary
- Stability of the new equilibria. Prove Mercier-/Suydam-type local criteria and Newcomb-type global certificates for the helical and Solov'ev equilibria. Formalize the δW reduction rather than citing it.
- Break the symmetry correctly. Move from exact helical symmetry to toroidal quasisymmetry. Bound the defect for a near-axis quasisymmetric configuration, and develop guiding-centre averaging so that the confinement time scales with the slowing-down time instead of the ballistic time.
- Coils. Couple an equilibrium boundary to a coil set (free-boundary/vacuum matching) using the now-proved Maxwell identities, and resume the four-coil VD1 dataset.
- Energetic alphas. Find configurations, or sharper orbit-width bounds, that cover 3.5 MeV alphas inside the plasma.