Kernel + Sanity
Restricted equilibrium and thermal laws, consistent examples, and counterexamples to overbroad claims.
Progress briefing · Equilibria, stability criteria and confinement
01 / 11From a coil fixture to exact equilibria with proved confinement.
PlasmaLean is building a Lean library for stellarator design. This run proved exact finite-pressure equilibria — a toroidal Solov'ev one and a nonaxisymmetric helical one — satisfying the kernel force-balance law, with all-time particle confinement theorems and Suydam/Newcomb stability criteria.
- Lean modules
- 53
- Source theorems, including private helpers
- 618
- Project declarations in the last axiom audit
- 1730
Progress so far
P3 (confined orbits) and P4 (finite-pressure equilibrium) now have checked instances in idealized symmetric models; P5 has local and certificate-based building blocks. P2 for a coil design remains partial.
Claim boundary. No configuration is coil-produced; the helical model has no toroidal curvature and the Solov'ev one is axisymmetric. No all-mode MHD stability, 3.5 MeV alpha confinement, or hardware qualification.
01 · How the library earns a claim
02 / 11Small assumptions. Reusable proofs. One candidate.
Physical model laws are explicit hypotheses. Derived mathematics and candidate certificates live above that small domain kernel.
Theory
Geometry, fields and Maxwell identities, equilibrium, Suydam/Newcomb stability, Noether confinement and thermal consequences.
Certificates + Bridge
Exact arithmetic, sound checkers and contracts that require the same candidate and witnesses.
Design
The vacuum-pair fixture, a Suydam-stable screw pinch, and exact Solov'ev and helical equilibria with confinement theorems exercise the reusable library.
Progress so far
The public library separates all six layers. The last audit found only Lean/Mathlib's standard logical axioms, with no added domain axioms.
Claim boundary. A theorem proves a consequence of a model; it does not establish that empirical assumptions apply to a real machine.
02 · Reusable mathematical progress
03 / 11The foundations have executable proof content.
Simple models make the definitions testable before tackling three-dimensional plasma physics.
Equilibrium
Force balance implies field/current tangency to pressure. Uniform and nonzero-current force-free slab examples provide witnesses.
Energy & stability
Conditional energy conservation, coercivity and retained/tail form bounds. A neutral-mode example shows why energy need not control displacement.
Geometry & fields
Continuous clearance, arbitrarily placed circular coils, Biot–Savart integrals and an exact on-axis loop field.
Progress so far
These are compiled elementary results and sanity checks, not just declarations of future tasks.
Claim boundary. Zero pressure does not imply zero current. Abstract energy bounds do not yet establish a continuum MHD stability result.
03 · Exact numerical certificates
04 / 11From a numerical proposal to a proved bound.
Rational interval soundness and contraction arguments give small end-to-end tests of the verification path.
Nonlinear validation
A scalar x² = 2 example on [1, 2] exercises the contraction framework with exact constants.
Thermal margin
A slab boundary-value problem has a whole-input-box maximum of 44002/45 K, with 998/45 K margin below an invented 1000 K limit.
Sound arithmetic
Exact coefficient decoding and interval/checker proofs separate candidate generation from the trusted proof path.
Progress so far
Exact arithmetic is connected to mathematical soundness theorems and explicit test fixtures.
Claim boundary. The scalar example is not a plasma PDE solution. The thermal inputs are invented, not sourced material qualification data.
04 · The vacuum calibration fixture
05 / 11Two circular coils. Precisely stated regions.
The first device-specific object is a calibration fixture with symbolic positive reference current I and permeability μ₀. Its field model uses ideal filaments.
Nominal geometry
Each coil has radius 0.10 m, in the planes z = ±0.20 m, with the same angular orientation.
Two different regions
Field/error/derivative bounds cover the 5 cm observation ball. The positive axial-field certificate covers the smaller 1 mm probe ball.
Progress so far
Closure, regularity, one-turn simplicity, source separation and the nominal midpoint field have proofs.
Claim boundary. The diagram is schematic, not a field-line simulation or a construction drawing. Neither ball is a certified confinement region.
05 · What survives manufacturing uncertainty
06 / 11Margins for the same perturbed coils and currents.
Assume closed C¹ coils with position error ≤ 1 mm, independent tangent error ≤ 1 mm/radian, and independent current errors ≤ 1% of I.
Field error
Actual minus nominal field has norm at most μ₀I/4 throughout the 5 cm observation ball (SI lengths in metres).
Nonzero probe field
The actual axial component is at least μ₀I/4 throughout the 1 mm probe ball, for μ₀ > 0 and I > 0.
Tube clearance
The two 5 mm-radius envelopes around actual coil centrelines remain at least 97/250 m = 388 mm apart.
Progress so far
Manufacturing and current errors compose into continuous field and clearance certificates, not just sampled checks.
Claim boundary. These tolerances are invented test inputs. Tube envelopes do not prove embedded winding packs or a finite-conductor electromagnetic model.
06 · Fields and local stability
07 / 11Maxwell identities proved; interchange stability decided both ways.
The closed-filament Biot–Savart field is divergence- and curl-free off the coil. A sharp Hardy inequality gives the Suydam criterion with both sufficiency and an explicit unstable mode.
∇·B = 0, ∇×B = 0
For the actual Fréchet derivative of the continuous filament integral, away from the source; curl needs a closed curve, and the open-segment curl is computed exactly.
Suydam, both directions
F ≥ 0, F + 4G ≥ 0 gives a coercive margin; F + 4G < 0 gives an unstable localized mode in every neighbourhood of the resonance. Hardy's constant 4 is sharp.
Newcomb certificates
Picone/Riccati/Jacobi certificates for variable coefficients, discharged by an exact rational polynomial checker running in the kernel.
Progress so far
A realistic screw pinch (a = 1 m, R₀ = 4 m, 5 T, ⟨β⟩ = 2/75) satisfies Suydam everywhere with a 25% margin, and Newcomb-reduced δW ≥ 0 is certified for every mode with 1 ≤ |m| ≤ 6 (wall at the edge).
Claim boundary. The δW reductions are cited source results, not formalized; modes with |m| ≥ 7, km < 0 remain uncertified. Suydam alone is necessary, not sufficient.
07 · Finite-pressure equilibria
08 / 11Two exact equilibria satisfy the kernel law J × B = ∇p.
The current is computed as curl B/μ₀ from actual derivatives and checked against the unchanged kernel ForceBalance class.
Solov'ev torus
Axisymmetric (tokamak-like) exact equilibrium; ITER-like instance R₀ = 6 m, B = 5 T, β_axis = 147/5000; div B = 0, flux and current tangent to surfaces.
Helical equilibrium
Helically symmetric, nonaxisymmetric exact equilibrium found by symbolic search; SI instance with pitch length 2 m, B = 5 T, β_axis = 4%.
Model limits
Straight helix (no toroidal curvature); smooth pressure formula restricted to ψ ≤ ψ_b; neither field is matched to coils.
Progress so far
P4 now has checked smooth instances at realistic field strength and β.
Claim boundary. No free-boundary or coil matching, and no global stability analysis of these equilibria yet.
08 · Confinement for all time
09 / 11Symmetry plus Noether confines every slow enough orbit forever.
Canonical momentum m⟨K,v⟩ + qψ is conserved for any Killing symmetry K; with speed conservation and an intermediate-value argument, orbits stay in a flux region for all time.
Solov'ev orbits
Deuterons up to 400 keV starting in the inner region never leave the plasma torus.
Helical orbits
Deuterons ≤ 30 keV and alphas ≤ 60 keV stay at r < 0.71 m inside the 4% β plasma, for all time.
Broken symmetry
A symmetry defect δ gives confinement only for times ∝ 1/(δ|v|) — ballistic, far from slowing-down times. 3.5 MeV alphas are not covered.
Progress so far
P3 has checked full-orbit instances; field lines are confined by exact first integrals.
Claim boundary. Orbits are supplied, not constructed. Quasisymmetric toroidal stellarators need guiding-centre averaging, not yet formalized.
09 · From idealized models to a stellarator
10 / 11The remaining device work is explicit.
The vacuum-fixture work packages remain, now joined by an equilibrium/stability track. A four-circular-coil, CNT-inspired architecture is a reference direction, not a certified design.
VD1 · Freeze the candidate
Version the four coil placements, frames, radii, turns/current conventions and leads against a source dataset.
VD2 · Continuous fields
Maxwell identities are proved for closed filaments; extend fixture geometry/derivative work to the candidate coil set.
VD3–4 · Conductors & confinement
Model embedded finite winding packs, then certify an invariant barrier or a declared finite-time orbit bundle.
VD5 · Physical operation
Source conductor, supply, thermal, mechanical, protection and metrology envelopes for that same candidate.
Progress so far
Reusable mathematics now spans fields, equilibria, local stability and symmetric confinement. No practical build or energization specification has been released.
Claim boundary. Finite-pressure equilibrium, all-mode MHD, transport and reactor engineering are separate later obligations, not implied by a vacuum demonstrator.
10 · Keep every step reviewable
11 / 11The next run must leave evidence, not just a promise.
Next proof targets: global (Newcomb/Mercier) stability of the new equilibria, quasisymmetry defect bounds with guiding-centre averaging, and coil/free-boundary matching.
Implement & challenge
Choose a scoped theorem or candidate milestone, retain explicit assumptions, and test limiting cases and counterexamples.
Compile & audit
Build the Lean library and run the axiom audit. Record actual results and remaining physical/model gaps.
Report & refresh
Update the dated report, task status, this slideshow and the brief README summary after every run, including stalled runs.
Progress so far
The linked run records checked declarations, assumptions and validation. This slideshow is a summary of that evidence, not a new design certificate.
Claim boundary. A practical claim needs composed certificates for one candidate plus evidence that the physical models and supplied data apply.