seiberg-witten

The Seiberg–Witten solution of N=2 SU(2) super-Yang–Mills, formalized in Lean 4.

No rigorous proof of this result exists — it presupposes constructing the interacting 4d quantum field theory. What a proof assistant can do is treat the physics argument rigorously: state the physical inputs as explicit, named postulates (H0–H7) and dictionary transcriptions carried in theorem types — never as axioms — and machine-check that the Seiberg–Witten solution follows. The trusted base is then Lean's three logical axioms plus a short, named list of classical mathematics, tracked per theorem by a golden #print axioms certificate. The companion paper is docs/paper1.tex.

The library is self-contained on pinned Mathlib and sorry-free.

The claim

For SU(2)/genus one, the compiled development proves the listed Seiberg–Witten consequences without sorry and without hidden physics axioms; physics enters through explicit H0–H7 predicates, structures, definitions, and stated dictionary transcriptions. The remaining trusted inputs beyond Lean's standard three are explicitly named classical-mathematics axioms, tracked per theorem by audit/axiom-report.txt. The higher-rank SU(N) headline is a proved skeleton modulo the coarse period-geometry axiom periodRigidityAxiom, whose discharge is future work.

What is proved (highlights)

• Uniqueness up to Γ(2) duality (SU2.sw_su2_unique, sw_su2_unique_coulomb): footprint = standard-3 + the Γ(2) covering/lift pair — nothing else. The full chain is formal: qualitative cusp data (SWModulusData) ⟹ the developing formula λ(τ(u)) = 2Λ²/(u+Λ²) including its normalization (swModulusData_eq_crossRatio, axiom-free) ⟹ uniqueness; and the cusp data itself follows from an H4-style atlas plus parabolic cusp lifts with non-extension (swModulusData_of_atlas_and_lifts).
• The explicit coupling (su2_coupling_exists, special coordinates, da_D/da = τ, the one-loop running): classical Jacobi inversion (AX_elliptic_inversion) as the one extra input.
• Why exactly one monopole–dyon pair (singularity_count_pinch): the Euler/mod-12 counting alone allows n ≡ 1 (mod 6) — the K3 loophole is witnessed — and the R-spurion covariance (H7, through its curve transcription) pinches n = 1. Axiom-free.
• SU(2) SQCD (matter): the coupling's uniqueness on the same classical basis (matter_coupling_rigidity); the Argyres–Douglas locus nonempty axiom-free (matter_argyresDouglasLocus_nonempty), via the development's first constructed period chart and an exact discriminant factorization.
• The θ/λ layer: λ = θ₂⁴/θ₃⁴ proved Γ(2)-invariant, the S/T laws, λ omitting {0,1}, λ → 0 at the cusp — on two citable Jacobi-θ identities.

What is assumed

• Physics: the named postulates H0–H7 below (predicates and structures in theorem types — there is no physical axiom anywhere) and their stated curve/Kodaira transcriptions, each validated per audit/FIDELITY_REVIEW.md.
• Classical mathematics, as named axioms (citable, numerically vetted): the Γ(2) covering/lift pair, Jacobi inversion, and two Jacobi-θ identities.
• Higher rank only: periodRigidityAxiom (Gauss–Manin period geometry) — the declared future work.

Full inventory: AXIOM_AUDIT.md.

The postulates H0–H7

	Postulate	One-line content	Lean carrier
H0	The carrier	Coulomb-branch data: special coordinates a, a_D, coupling τ, and the Dirac-paired charge lattice, on the punctured moduli space	PeriodBase / PeriodChart
H1	Special geometry	One holomorphic prepotential F with a_D = ∂F/∂a, τ = ∂²F/∂a², and Im τ ≻ 0 (unitarity)	SpecialGeometry
H2	BPS singularities	A singularity of the effective theory is a charged BPS state going massless, Z → 0	PeriodsDegenerateOnBoundary
H3	Monodromy	Around such a point the periods undergo the symplectic Picard–Lefschetz transvection in the light state's charge (one-loop log + Witten effect)	PicardLefschetzAtGenericStratum
H4	EM duality	Charts glue by Sp(2r,ℤ) preserving the Dirac pairing and the central charge	SymplecticReframing / PeriodAtlas
H5	R-symmetry	The anomaly-surviving discrete U(1)_R acts on the moduli with order dividing 2N and permutes the singular locus	HasFiniteOrderAutomorphism
H6	Weak-coupling asymptotics	The prepotential is one-loop exact up to a Λ^{2N}-weighted instanton series of prescribed scaling weights	HasPrescribedAsymptotics
H7	Spurionic U(1)_R covariance of the Λ-family	Rescaling Λ is an RG transformation, F(tΛ)(t·a) = t²F(Λ)(a); Λ → ζΛ with ζ^{2N} = 1 (the θ-angle shift) changes F only by one integer EM frame shift ½aᵀBa, constant across the family	SpurionCovariantFamily

H0–H6 constrain the theory at fixed Λ (bundled as IsPolarizedPeriodChart, with H4 at the atlas level); H7 ties the Λ-family together. Physical justification: paper §4.2 and Appendix A; definitions: SeibergWitten/Physics/Hypotheses.lean.

Verify it yourself

lake build                                # pinned Mathlib; no other dependency
bash audit/gen_axiom_report.sh --check    # the golden #print axioms certificate
python3 audit/check_faithfulness.py       # paper-facing quotes match the source
for f in audit/numerical/validate_*.py; do python3 "$f"; done   # 9 oracle suites, 278 checks

Reviewing the project? Start at audit/REVIEWER.md — the claims, what each rests on, and the evidence per claim. The method follows math-commons/formalization-assurance: faithfulness digests with machine-verified quotes, fidelity review with independent numeric cross-checks, difficult points recorded, adversarial statement review before adoption.

Layout

SeibergWitten/          the library (physics layer: Physics/)
RiemannPeriods/         weight-1 VHS bootstrap (Mathlib-only)
HigherGenus/            higher-genus Riemann-surface layer — NOT built (see below)
audit/                  certificate, checkers, oracles, V&V documents
docs/paper1.tex         the companion paper

Higher genus and jacobian-challenge

The general-SU(N) story (genus N−1 proved, Riemann-bilinear positivity Im τ ≻ 0) lives in HigherGenus/, which builds against the external Riemann-surface / period / Jacobian library jacobian-challenge and is kept outside the certified build — the main library and every footprint in the paper are Mathlib-only. HigherGenus/README.md has the re-enable recipe; discharging periodRigidityAxiom through that layer is the roadmap in audit/PERIOD_LAYER_DISCHARGE.md.

Acknowledgments

The certified library depends only on Mathlib; it is the higher-genus skeleton (HigherGenus/, outside the build) that builds against jacobian-challenge, which in turn vendors Rado Kirov's Dolbeault/Riemann-surface development. This project owes much to that library and its contributors — Kevin Buzzard, Rado Kirov, and the other contributors. See the paper's acknowledgments for the full list of colleagues whose reviews and discussions shaped the project.

License

Copyright 2026 Michael R. Douglas. Released under the Apache License 2.0 (the Lean/Mathlib ecosystem convention).

---

Comparator-verified (Lean FRO comparator, commit 75bb75b, 2026-07-07, via lean4export@v4.30.0; macOS fake-landrun): all no-sorry, kernel-replayed, axioms exactly as printed.

• Axiom-clean (standard-3 only): matter_argyresDouglasLocus_nonempty, betaFunction_weakCoupling, and the SU(2)-from-postulate pair SU2.sw_su2_unique_of_periodLayer / sw_su2_exists_of_periodLayer.
• Concrete SU(2) headline family (standard-3 + the classical inputs AX_thrice_punctured_uniformization, AX_developing_map_rigidity, AX_elliptic_inversion): SU2.sw_su2_unique, su2_coupling_exists, su2_coupling_canonical, swAD_tendsto_zero_monopole (H2), swA_weakCoupling (H6), swAD_deriv_eq_swTau_mul_swA_deriv, swTau_logDeriv_weakCoupling.