\documentclass{article}
\pdfoutput=1

% Axioms for physical reasoning: codifying the Seiberg-Witten solution in Lean.
% Companion working paper to mrdouglasny/seiberg-witten and the ICML 2026 talk.
% Formatting follows the OSforGFF "Formalization of QFT" paper (authblk, amsplain
% BibTeX bibliography). Compile with pdflatex (the Unicode in the verbatim Lean
% appendices is handled by \DeclareUnicodeCharacter below); run bibtex for the
% references.

\usepackage[margin=1in]{geometry}
\usepackage{amsmath, amssymb, amsthm, amsfonts, mathtools}
\usepackage{microtype}
\usepackage{authblk}
\usepackage{xcolor}
\usepackage[colorlinks=true,linkcolor=blue,urlcolor=blue,citecolor=blue]{hyperref}

\bibliographystyle{amsplain}

\renewcommand\Authfont{\normalsize}
\renewcommand\Affilfont{\itshape\small}
\setlength{\affilsep}{0.5em}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{prop}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{cor}[theorem]{Corollary}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{axiomenv}[theorem]{Axiom}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{equation}{section}

% Long unhyphenatable Lean identifiers: give the line breaker some slack
\emergencystretch=1.5em

\newcommand{\C}{\mathbb{C}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\HH}{\mathbb{H}}
\newcommand{\Sp}{\operatorname{Sp}}
\newcommand{\Imag}{\operatorname{Im}}
\newcommand{\code}[1]{\texttt{#1}}

% pdflatex font setup: T1-encoded Latin Modern; the Lean verbatim blocks contain
% Unicode math symbols, mapped to math-mode glyphs by the declarations below
% (\DeclareUnicodeCharacter applies inside fancyvrb Verbatim as well).
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{fancyvrb}
\fvset{fontsize=\footnotesize,xleftmargin=0.5em}

% Blackboard-bold sets
\DeclareUnicodeCharacter{2102}{\ensuremath{\mathbb{C}}}   % ℂ
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}   % ℕ
\DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}}   % ℝ
\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}}   % ℤ
\DeclareUnicodeCharacter{210D}{\ensuremath{\mathbb{H}}}   % ℍ
% Greek
\DeclareUnicodeCharacter{0391}{\ensuremath{A}}            % Α
\DeclareUnicodeCharacter{0393}{\ensuremath{\Gamma}}       % Γ
\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}}       % Δ
\DeclareUnicodeCharacter{039B}{\ensuremath{\Lambda}}      % Λ
\DeclareUnicodeCharacter{03A3}{\ensuremath{\Sigma}}       % Σ
\DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}}       % α
\DeclareUnicodeCharacter{03B2}{\ensuremath{\beta}}        % β
\DeclareUnicodeCharacter{03B3}{\ensuremath{\gamma}}       % γ
\DeclareUnicodeCharacter{03B4}{\ensuremath{\delta}}       % δ
\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}}      % λ
\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}}         % τ
\DeclareUnicodeCharacter{03C9}{\ensuremath{\omega}}       % ω
% Quantifiers, logic, set theory
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}      % ∀
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}      % ∃
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}       % ∧
\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}}         % ∨
\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}}         % ¬
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}}          % ∈
\DeclareUnicodeCharacter{2209}{\ensuremath{\notin}}       % ∉
\DeclareUnicodeCharacter{2229}{\ensuremath{\cap}}         % ∩
\DeclareUnicodeCharacter{222A}{\ensuremath{\cup}}         % ∪
\DeclareUnicodeCharacter{2286}{\ensuremath{\subseteq}}    % ⊆
% Relations
\DeclareUnicodeCharacter{2260}{\ensuremath{\ne}}          % ≠
\DeclareUnicodeCharacter{2264}{\ensuremath{\le}}          % ≤
\DeclareUnicodeCharacter{2265}{\ensuremath{\ge}}          % ≥
\DeclareUnicodeCharacter{2243}{\ensuremath{\simeq}}       % ≃
\DeclareUnicodeCharacter{2245}{\ensuremath{\cong}}        % ≅
\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}}         % ∣
% Arrows
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}          % →
\DeclareUnicodeCharacter{2194}{\ensuremath{\leftrightarrow}} % ↔
\DeclareUnicodeCharacter{21D1}{\ensuremath{\Uparrow}}     % ⇑ (Lean coercion)
\DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}}  % ⇒
% Operators
\DeclareUnicodeCharacter{2202}{\ensuremath{\partial}}     % ∂
\DeclareUnicodeCharacter{2211}{\ensuremath{\sum}}         % ∑
\DeclareUnicodeCharacter{2218}{\ensuremath{\circ}}        % ∘
\DeclareUnicodeCharacter{2022}{\ensuremath{\bullet}}      % • (Lean scalar action)
\DeclareUnicodeCharacter{2212}{\ensuremath{-}}            % − (minus sign)
% Sub/superscripts
\DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}}         % ₀
\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}}         % ₁
\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}}         % ₂
\DeclareUnicodeCharacter{2097}{\ensuremath{{}_l}}         % ₗ
\DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}}         % ²
\DeclareUnicodeCharacter{1D9C}{\ensuremath{{}^{c}}}       % ᶜ (complement)
\DeclareUnicodeCharacter{1DA0}{\ensuremath{{}^{f}}}       % ᶠ (eventually-equal)
% Punctuation
\DeclareUnicodeCharacter{2014}{---}                       % — em dash
\DeclareUnicodeCharacter{03B8}{\ensuremath{\theta}}       % θ
\DeclareUnicodeCharacter{03B6}{\ensuremath{\zeta}}        % ζ

\title{Axioms for physical reasoning:\\ codifying the Seiberg--Witten solution in Lean%
  \thanks{Working paper, draft. Companion to the formal development at
  \href{https://github.com/mrdouglasny/seiberg-witten}{\code{mrdouglasny/seiberg-witten}}
  and to the ICML 2026 talk \emph{Validation of AI-generated results in theoretical physics}.}}
\author[1]{Michael R. Douglas \thanks{mdouglas@cmsa.fas.harvard.edu}}
\affil[1]{Center Of Mathematical Sciences And Applications, Harvard University, Cambridge, MA 02138 USA}
\date{July 2026}

\begin{document}
\maketitle

\begin{abstract}
Mathematicians have embraced interactive theorem provers with growing enthusiasm---building large
shared libraries and machine-checking a string of landmark results. Theoretical physics is
different: most of its results are not theorems but justified by arguments the community trusts
without a rigorous proof. For many---the one we treat here among them---no rigorous
proof is within reach. For 4d Yang--Mills theory, deriving exact rigorous results from first principles
would first require constructing the interacting theory nonperturbatively, which is a sizable piece of
one of the Clay Millennium prize problems. 

We argue here that an interactive theorem prover can be used to verify some non-rigorous physics arguments.
The method is to postulate a short list of \textbf{explicit, named physical
postulates}, which imply the physical results by virtue of a machine-checkable proof.
The trust that remains then rests on that short, inspectable list, and the prover can
report, for any downstream result, exactly which assumptions it used. We carry this out for
the Seiberg--Witten solution of $\mathcal{N}=2$ $SU(2)$ super-Yang--Mills---the genus-one
case---formalized in Lean 4; the higher-genus $SU(N)$ generalization is developed in the same
repository as an axiomatized skeleton and left to future work. We describe what is proved, what is assumed, how the assumptions are checked---external
review and an independent numerical oracle---and why this discipline is a sound standard for
validating AI-generated results in theoretical physics. What we offer is a \emph{discipline},
reviewable on its own terms: a reader may take the Seiberg--Witten mathematics on trust and
still assess the formalization method.
\end{abstract}

\tableofcontents

\section{Introduction}

Most of what theoretical physics asserts is not rigorously proved. Across the field, the results we build on
are typically not theorems but conclusions of \emph{arguments}---chains of physical reasoning
trusted because they cohere internally, because independent routes to the same quantity agree, and
ultimately because they account for experiment. A result can be as certain as anything in science
and still have no rigorous proof from first principles; certainty in physics rests on a different footing
than in mathematics.

In quantum field theory the gap is very wide. There the deepest results---the spectrum of a
gauge theory, its phase structure, an exact low-energy effective action---follow from reasoning
based on principles like symmetry, locality, dualities and consistency. The {Seiberg--Witten
solution}~\cite{SeibergWitten1994a,SeibergWitten1994b}, our
subject below, is a paradigmatic example.  A rigorous proof is out of reach: it would require first
constructing the interacting theory nonperturbatively, on the scale of the Yang--Mills
Millennium Prize. Such results are as certain as anything in physics, yet they are not theorems.

This gap has become pressing for a new reason: AI systems now generate physical derivations, and
their characteristic error is not a wrong algebra step---these can be caught automatically---but a
\emph{hallucinated assumption}, an unphysical premise or a dropped subtlety presented as if derived.
The possibility of such errors leads many to insist that AI-generated proofs require human auditing, but 
reading the entire proof is often not practical. 
What one wants instead is a way to make an
argument's assumptions explicit and machine-auditable, cleanly separating what is genuinely derived
from what is taken on faith.

Interactive theorem provers are built for exactly that separation. A technology from computer
science---which grew out of hardware and software verification---proof assistants have lately
drawn intense interest in mathematics, with fast-growing libraries and a number of landmark theorems now machine-checked.
Introductions to and reviews of the use of interactive theorem proving in mathematics
include~\cite{Buzzard2022,Avigad2024,Tao2025}, and in physics
include~\cite{ToobySmith2025,ToobySmith2025Perspective,douglas_formalization_2026};
a recent formalization of physics reasoning in Lean---adjacent in spirit to the present
work---poses model-building questions as formal statements~\cite{KrippendorfToobySmith2026}.
We will demonstrate here how to apply these tools to a physics argument. A proof assistant such as \textbf{Lean 4} is a
language in which one writes definitions and proofs that a small, fixed {kernel}---a few
thousand lines of code, audited once and then trusted---checks line by line. A statement the kernel accepts is correct \emph{relative to its
inputs}: the handful of logical axioms built in,\footnote{Examples are the axiom of choice, and excluded middle:
for any proposition $P$, either $P$ or $\mbox{not}\,P$ must be true.
} 
plus any further {axioms} the author explicitly declares. 

Throughout this paper, ``axiom'' is meant in the logician's sense --- a \emph{formalized, named, audited
assumption} the kernel tracks.\footnote{  In Lean this can be done in several ways; as an
explicit \code{axiom} stating the assumption; by using the \code{sorry} tactic which accepts an intermediate result
without proof; or as hypotheses which are not assumed globally but on which the results of interest are proven conditionally.
%While the choice depends on details, generally if the assumption is provisional and the intent is to later discharge (prove) it,
%the first two would be used, while if the intent is to exhibit the explicit dependence on assumptions then a conditional proof would be in order.  
In this introduction we use ``axiom'' to refer to any of these methods.}
%
Our work here will use assumptions of two kinds, and we name them differently:
\textbf{mathematical axioms} --- true classical mathematics assumed without formal proof --- and
\textbf{physical postulates}, the formal translations of physical assumptions. (The title's
``axioms'' is the umbrella, logician's sense just described; within it, these two names
distinguish what kind of trust each assumption asks for.) The distinction is
enforced by the architecture, not just the prose: in the development the Lean \code{axiom}
keyword carries only mathematics, while the physical postulates are predicates carried in the
theorems' types.
To explain the first, in formalizing a mathematical proof, one sometimes provisionally assumes provable intermediate steps as axioms, in order
to check that the final theorem is provable before going back to complete these intermediate steps.  For example,
in our OSforGFF project \cite{douglas_formalization_2026} we assumed Minlos' theorem in our first release, and proved it in the second.
This leads to practical issues but, given that we only axiomatize provable correct results, no new issues of principle.

The physical postulates are formal translations of physical assumptions.   We will explain the ones we use here in detail below,
but they include the basic definitions of physical concepts in mathematical terms and their accepted properties.  These might
be provable from more basic physical assumptions; they might encode empirical data; they might be believed because they
are true in many previously studied cases; or they might be pure leaps of intuition.  The point here is that
by stating these postulates formally,
they become {precise, finite, named, and dependency-tracked}. 

The combination of mathematical axioms and physical postulates 
assumed in deriving a result is the {trusted base}---everything one must believe in
order to believe the result---and the Lean prover can print it: for any theorem, the command
\code{\#print axioms} reports exactly which axioms it used, and nothing reaches that list without
being named. Modern provers ship with large formal libraries of mathematics---Lean's is
\textbf{Mathlib}~\cite{mathlib}, several hundred thousand theorems---so one formalizes atop real
analysis, algebra and geometry rather than from scratch.

The point of this paper is to turn that machinery on a physics result that \emph{cannot} be proved,
and to use it honestly. We do not try to rigorously prove the Seiberg--Witten solution; that is beyond reach.
Instead we \textbf{state the physical reasoning as a short list of explicit, named postulates, prove
every mathematical consequence of them in Lean, and let the kernel verify the relation between the two.}
The residual trust is then concentrated on that named list.  
The \code{\#print axioms} command audits, for any downstream claim, precisely which
physical inputs it rests on. 
In principle, the kernel could expose contradictions
hidden among the axioms (a logical contradiction implies all propositions including manifestly false ones).
Justifying the axioms is still the physicist's task---here, external
review and an independent numerical oracle---but it becomes a finite, inspectable one rather than a
diffuse act of faith.

We chose the {Seiberg--Witten solution} as a test case for many
reasons.  It is a
celebrated, universally trusted result, unprovable by present-day mathematics, yet mathematically precise
in content---it identifies the exact low-energy physics with the period geometry of a specific family
of algebraic curves, so both the physical assumptions and their mathematical consequences are crisp
enough to formalize. Around it we obtain a clean split: a proved mathematical spine (the curve, its
genus, positivity of the special-K\"ahler metric, the explicit genus-one solution with its
special coordinates and one-loop running), the physical hypotheses as named predicates, and the
headline statements---existence, and uniqueness up to duality---proved from those hypotheses
plus classical, citable mathematical inputs. We treat the genus-one ($SU(2)$) case in full;
the higher-genus family is future work (\S6).

The rest of the paper proceeds as follows. \S2 sets out the two kinds of formalization a physics
result calls for and the bookkeeping discipline they impose. \S3 states the Seiberg--Witten solution
compactly. \S4 is the formalization proper---the math$\leftrightarrow$physics dictionary, what is assumed (the
hypotheses, with their physical origins), what is proved, what formalizing forced into the open, and a worked axiom-free check
(Argyres--Douglas points in a worked matter example).
\S5 describes how we check the axioms. \S6 lays out the remaining mathematical debt and our
posture toward it---the genus-one classical axioms we deliberately keep, and the higher-genus
programme we leave to future work---and \S7 the prospects for deriving the physical assumptions
themselves from deeper principles.
\S8 concludes. Two appendices give the Lean statements of the physical
hypotheses (A) and the residual mathematical axioms (B).

\section{Two kinds of formalization}

A mathematician who formalizes a theorem has a proof to formalize; a physicist who formalizes a
\emph{result} usually has none. The two situations call for two different kinds of formalization:

\begin{center}
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{@{}p{0.26\textwidth}p{0.30\textwidth}p{0.34\textwidth}@{}}
\hline
& \textbf{What it is} & \textbf{Examples} \\
\hline
\textbf{Mathematical physics} & A rigorous statement exists; you prove it. & Stability of
matter; constructive QFT; the lattice-gauge mass gap---\emph{and the proved spine of this
project}: the curve, its genus, special-K\"ahler positivity, the period matrix. \\
\textbf{Foundations for physical reasoning} & Codifying the \emph{non-rigorous} reasoning the
community trusts, where no proof is within reach. &
\emph{The Seiberg--Witten argument itself.} \\
\hline
\end{tabular}
\end{center}

Mathematical physics formulates and proves physical results within the accepted foundations of mathematics,
so the first kind of formalization can follow existing practice for formalizing mathematics.
But Seiberg--Witten requires the second kind: to date, there is no rigorous derivation that the low-energy
physics on the Coulomb branch of $\mathcal{N}=2$ $SU(N)$ gauge theory is governed by the curve
$y^2 = P_N(x)^2 - \Lambda^{2N}$~\cite{KLYT1995,ArgyresFaraggi1995}. In its place stands an \emph{argument}---holomorphy from
supersymmetry, the exact pattern of singularities, electric--magnetic duality, the weak-coupling
asymptotics---that together single out that curve.  This result was confirmed by independent arguments, most notably
Nekrasov's instanton computation of the prepotential \cite{Nekrasov2003}.  This calculation and
the proof that it reproduces the original Seiberg-Witten solution has been made rigorous
\cite{NekrasovOkounkov2006,NakajimaYoshioka2005,BravermanEtingof2006}; however the claim that it actually
describes $N=2$  super Yang-Mills rests on the physical assumption that the instanton expansion produces an exact result,
whose rigorous statement and proof would require some rigorous definition of $N=2$  super Yang-Mills,
so is out of reach.

We call the practices and axioms used in this second category of formalization
\textbf{foundations for physical reasoning}, by analogy with
foundations of mathematics.
This distinction is not a value judgment; as we have discussed at length elsewhere \cite{douglas2011foundations}, both
non-rigorous and rigorous arguments have their advantages and disadvantages.  The paradigm we propose here could be considered
a hybrid approach, making as much of the physics argument as possible rigorous, and making explicit all the ingredients which go beyond
mathematical rigor as it exists now.

To realize this explicitness, a certain discipline should be followed.  No physical input should hide in a mathematical definition,
so {no mathematical axiom may use physical vocabulary}. Since not all of the mathematics needed for Seiberg-Witten has been formalized,
we postulate mathematical axioms, but these name only mathematics
(periods, the period matrix, monodromy in $\Sp(2g,\Z)$, asymptotics).
Every physical quantity---effective coupling, central charge, electric--magnetic duality, beta function---will have an
\textbf{explicit definition} identifying it with a mathematical object, collected in one dictionary
and never silently equated. The trusted mathematical base is then logic plus \emph{purely mathematical} axioms;
physics enters only through inspectable definitions and the named hypotheses H0--H7. 

An example is the beta function for the effective
coupling.  The mathematical input---the logarithmic weak-coupling running of the period
ratio---is a \emph{theorem}: for the explicit genus-one coupling,
$u\,d\tau/du \to i/\pi$ is proved, a corollary of the (also proved) Legendre relation.  The
identifications \code{coupling} $:=$ period ratio and
\code{betaFunction} $:= \Lambda\, d/d\Lambda\, \tau$ are definitions, and the one-loop value
$b_0 = 2N - N_f$ follows as a theorem of the three logical axioms. The consolidated period axiom of Appendix~B is in this form too: it is a
purely \emph{mathematical} statement---the existence and rigidity of the period geometry of the curve
family $y^2 = P^2 - \Lambda^{2N}$ (period charts, polarized period data, monodromy in $\Sp$,
prescribed asymptotics)---whose physical reading, that this data \emph{is} the SW effective theory
with electric--magnetic duality the symplectic reframing, is supplied entirely by the dictionary
(\S4.1). What is \emph{not} done is \textbf{discharging} it---constructing that
higher-genus period geometry. At genus one the corresponding layer \emph{is}
constructed: the explicit elliptic-integral periods and special coordinates of \S4.3,
with Jacobi inversion the one classical input. For $SU(N)$ it is the remaining
mathematical debt of \S6 and Appendix~B.1---but that is a matter of proof, not of the
math--physics separation.

To summarize the differences between mathematical and our proposed physical style of formalization:
\begin{itemize}
\item There is no rigorous proof to formalize, so the
question is not ``is the proof correct?'' but ``are the assumptions explicit and the derivations
sound?''
\item The physical lore becomes \textbf{named hypotheses}---predicates a theorem takes in its
signature. 
\item The residual trust then localizes onto a short list, and \code{\#print axioms} of any
result audits exactly which assumptions it used.
\end{itemize}
Finally, this approach is not specific to physics, it could be applied in many other disciplines.
The point is to formalize an \emph{argument the community trusts} rather than \emph{a theorem with a proof}.

\section{The Seiberg--Witten solution in two paragraphs}

\emph{For a reader outside physics: the SW solution maps the exact low-energy behavior of a
quantum system to the geometry of a specific family of algebraic curves. What matters for the
formalization is less the physical meaning of the terms below than the rigid mathematical data
they impose.}

On the Coulomb branch---coordinates $u_2,\dots,u_N$, rank $r = N-1$---the low-energy theory is
abelian $U(1)^r$ gauge theory. Its data are the special coordinates $a_i$ and their duals
$a_{D,i}$ (periods of a meromorphic differential), the coupling matrix $\tau_{ij}$, and the
central charge $Z = n_e\cdot a + n_m\cdot a_D$ of a BPS state, whose modulus is its mass. The
SW claim is that all of this \emph{is} the period geometry of $y^2 = P_N(x)^2 - \Lambda^{2N}$.
Here $P_N$ denotes a family of degree-$N$ polynomials in a coordinate $x$,
the identification of $P_N$'s coefficients with the $u$'s is part of the claim.

The assumptions that single out that family of curves are: holomorphy / non-renormalization (one holomorphic
prepotential $\mathcal{F}$, one-loop-exact perturbation theory); the exact singularity
structure (the branch is singular exactly where a BPS state goes massless, and nowhere else);
electric--magnetic duality ($\Sp(2r,\Z)$ monodromy); the $\Z_{2N}$ $R$-symmetry fixing the
singularities; and matching to the one-loop-plus-instanton expansion at weak coupling.
For pedagogical reviews see~\cite{Lerche1997,Bilal1996}.

This paper treats the original genus-one case $N = 2$ in full---there the curve is elliptic,
the period geometry is classical elliptic-function theory, and the trusted base can be made
entirely classical and citable. The higher-genus family is formalized in the same repository
as an axiomatized skeleton (one consolidated period axiom; \S B.1) and is future work.

\section{The formalization}

\subsection{The dictionary: physical concepts as mathematical objects}

We fix the translation first. Each physical concept is a \emph{named mathematical object}; the
statements throughout \S4 and the appendices use the mathematical names (\code{\#print axioms}
reports them), with the physics reading given here. In Lean these are machine-linked
(\code{Dictionary.lean}: \code{abbrev Sheet := PeriodChart}, etc.), so the physics names denote
\emph{exactly} the math objects --- physics never enters silently, only through this dictionary and
the named hypotheses H0--H7.

\begin{center}\small
\begin{tabular}{ll}
\hline
math (primary) & physics term\\
\hline
\code{PeriodBase} & the Coulomb branch (moduli minus singular locus)\\
\code{PeriodChart} & a sheet of the low-energy effective theory\\
\code{PeriodChart.a}, \code{.aD}, \code{.tau} & special coordinates $a, a_D$; coupling $\tau$\\
\code{PeriodChart.periodCombination}, \code{.periodNorm} & BPS central charge $Z_n$; BPS mass\\
\code{CycleLattice}, \code{intersectionForm} & charge lattice $H_1(\Sigma,\mathbb{Z})$; Dirac (EM) pairing\\
\code{SymplecticReframing} & electric--magnetic duality\\
\code{IsPolarizedPeriodChart} & a Seiberg--Witten effective theory (H1--H6)\\
\code{PeriodRigidity} / \code{periodRigidityAxiom} & the period-geometry layer / its axiom\\
\code{PicardLefschetzAtGenericStratum} & monodromy from massless charged states\\
\code{NonLocalDegenerationLocus} & Argyres--Douglas points\\
\code{betaFunction}, \code{oneLoopCoefficient} & beta function $\Lambda\,d/d\Lambda\,\tau$; $b_0=2N-N_f$\\
\hline
\end{tabular}
\end{center}

\subsection{What is assumed}

The physical content is the hypotheses \textbf{H0--H7}, each a named Lean \textbf{predicate or
structure} (never a global axiom: a theorem that uses the physics carries them in its
\emph{type} --- the fixed-$\Lambda$ content bundled as \code{IsPolarizedPeriodChart}, one
local branch of the low-energy SW effective theory; H4 in the atlas gluing; H7 as the
family-level \code{SpurionCovariantFamily} --- so the assumptions live in theorem types, not
the trusted base). They are \textbf{not} physically independent postulates: in principle they could be derived from the more fundamental postulates of
\textbf{N=2 supersymmetry}, together with the gauge data
($SU(N)$, asymptotic freedom) and unitarity. We give each with its physical origin and Lean carrier:

\begin{itemize}
\item \textbf{H0 --- the carrier} (\emph{N=2 SUSY $+$ Coulomb-phase Higgsing}). A generic adjoint
vev breaks $SU(N)\to U(1)^{N-1}$, leaving $r=N-1$ abelian N=2 vector multiplets; their special
coordinates $a, a_D$, coupling $\tau$, and the charge lattice with its Dirac pairing are the data
(\code{PeriodBase}/\code{PeriodChart}), on the universal cover of the moduli space minus its singularities.
\item \textbf{H1 --- special geometry} (\emph{N=2 SUSY; unitarity}). Eight supercharges force the
Coulomb branch to be rigid special K\"ahler: one holomorphic prepotential $F$ with
$a_D = \partial F/\partial a$, $\tau = \partial^2 F/\partial a^2$; $\Imag\tau\succ 0$ is positivity
of the gauge kinetic term, the no-ghost (unitarity) condition (\code{PeriodChart.SpecialGeometry}).
\item \textbf{H2 --- BPS singularities} (\emph{the central-charge BPS bound}). The N=2 algebra
carries a central charge $Z$; all states obey $M\ge|Z|$, saturated by BPS states. A singularity of
the effective theory is a charged BPS state going massless, $Z_n\to 0$
(\code{PeriodChart.PeriodsDegenerateOnBoundary}).
\item \textbf{H3 --- monodromy from massless charged states} (\emph{the SW monodromy: one-loop
running $+$ the Witten effect}). Encircling a point where the BPS state of charge $n$ becomes
massless, the periods undergo the symplectic Picard--Lefschetz transvection in $n$ --- fixed by the
light state's one-loop logarithm (its $\beta$-function) and the Witten-effect $\theta\leftrightarrow$
charge shift (\code{PicardLefschetzAtGenericStratum}).
\item \textbf{H4 --- electric--magnetic duality} (\emph{Montonen--Olive / Seiberg--Witten duality}).
The freedom in which charges count as ``electric'' is the symplectic group $\Sp(2r,\Z)$ preserving
the Dirac pairing and the central charge; charts glue by it (\code{SymplecticReframing}; sheets form a
duality-glued \code{PeriodAtlas}).
\item \textbf{H5 --- R-symmetry} (\emph{the anomalous $U(1)_R$}). The classical $U(1)_R$ is broken
by instantons to a discrete subgroup ($\Z_{4N}$ on the fields, acting through $\Z_{2N}$ on the
adjoint scalar), acting on the moduli with order dividing $2N$ and permuting the singular locus
(\code{HasFiniteOrderAutomorphism}).
\item \textbf{H6 --- weak-coupling asymptotics} (\emph{N=2 nonrenormalization $+$ asymptotic
freedom}). The prepotential is \textbf{one-loop exact} in perturbation theory; the remainder is a
sum of instanton corrections weighted by the dynamical scale $\Lambda^{2N}$, with coefficients of
the prescribed scaling weight $2 - 2Nk$ --- the fixed-$\Lambda$ expression of their
$\Lambda$-\emph{independence}, without which the clause is vacuous (\S4.4)
(\code{PeriodChart.HasPrescribedAsymptotics}).
\item \textbf{H7 --- spurionic $U(1)_R$ covariance of the $\Lambda$-family}
(\emph{dimensional transmutation $+$ $\theta$-angle periodicity through the anomaly}).
H0--H6 constrain the theory at fixed $\Lambda$; H7 ties the family together. Rescaling
$\Lambda$ is an RG transformation: $F(t\Lambda)(t\,a) = t^2 F(\Lambda)(a)$. And for any
$2N$-th root of unity $\zeta$, the rotation $\Lambda \to \zeta\Lambda$ preserves the
instanton factor $\Lambda^{2N}$---for the primitive root this is the $\theta$-angle shift
$\theta \to \theta + 2\pi$ ($\arg\Lambda^{2N} = \theta$), a symmetry by
instanton-number quantization, with the anomaly coefficient one-loop exact
(Adler--Bardeen). At the prepotential level it holds \emph{up to an integer
electric--magnetic frame shift} (the Witten effect): $F \to F + \tfrac12\,a^{T}Ba$ with
$B$ an integer symmetric matrix \emph{constant across the family}---the existential sits
outside all quantifiers, so it can absorb nothing (the lesson of \S4.4). H5 and H6's
homogeneity clause are its fixed-$\Lambda$ shadows (the instanton remainder is
weighted-homogeneous across the family, \code{instanton\_remainder\_covariant}, with the
classical and one-loop pieces exactly covariant---the logarithm enters only through the
scale-invariant ratio); its curve-level transcription is \code{RSpurionCovariant}
(\S4.3). Being a family-level statement, it is carried separately from the fixed-$\Lambda$
bundle \code{IsPolarizedPeriodChart} (\code{SpurionCovariantFamily}).
\end{itemize}

\paragraph{The uniqueness claim, stated exhaustively.} The genus-one headline is best read
in two steps. First, the structure that \emph{defines} the SW special geometry---the curve
family, the SW differential $\lambda_{\mathrm{SW}} = x^2\,dx/y$, and its closed-form
periods---is a \emph{definition} (\S4.1, \S5): the constructed candidate then provably
satisfies special geometry, the singularity structure, and positivity. Second, the theorem
is that this is the \textbf{unique} special geometry compatible with the physics, and its
hypotheses carry \textbf{no physical content beyond H0--H7}. In detail: the rank-1 chain
consumes the H1 shadows directly (holomorphy of $\tau(u)$ and $\Imag\tau > 0$); H4 enters
as an atlas of local couplings glued by the monodromy group (\code{IsSWCouplingAtlas});
H2$+$H3 enter as a parabolic universal-cover lift at each of the three punctures, genuinely
singular in the sense of \emph{non-extension}---H2's massless state at $\pm\Lambda^2$,
asymptotic freedom (the qualitative content of H6) at $\infty$
(\code{IsGenuineCuspLift}); the rest is domain bookkeeping (an open, connected, nonempty
chart), discharged by proved facts on the maximal domain $\C\setminus\{\pm\Lambda^2\}$.
From exactly this data, everything that once looked like an extra postulate is a theorem:
the modulus observable $J = \lambda\circ\tau$ is single-valued with the three qualitative
cusp limits (\code{swModulusData\_of\_atlas\_and\_lifts} --- descent through the proved
$\Gamma(2)$-invariance, plus a removable-singularity dichotomy; no Picard theorems); the
developing formula $\lambda(\tau(u)) = 2\Lambda^2/(u+\Lambda^2)$, including its degree,
cusp rates, and normalization, follows (\code{swModulusData\_eq\_crossRatio}; footprint
standard-3, no axioms), with the base map pinned independently against the curve's periods
(\S5); and uniqueness \textbf{up to a $\Gamma(2)$ duality frame} follows on a footprint of
the covering pair alone (\code{sw\_su2\_unique\_of\_modulusData}), the canonical
representative within the frame being fixed by the one-loop asymptotics (H6). Each clause
is load-bearing and machine-checked in both directions: the cross-ratio itself carries the
cusp data (\code{swModulusData\_swCrossRatio}), while the degree-two candidate
$4\Lambda^4/(u+\Lambda^2)^2$ satisfies every clause except omitting the value $1$, failing
at the smooth point $u = -3\Lambda^2$---an extra would-be singularity. Beyond H0--H7 the
input is exactly one: the classical mathematical axioms of Appendix B. (H7 enters the
singularity count through its curve-level transcription \code{RSpurionCovariant},
\S4.3---a definition-level shadow, like the H4 atlas and the H2$+$H3 cusp lifts.)
\code{\#print axioms} certifies that this list is complete. Full Lean definitions are in Appendix A, which also discusses factoring these as
one general N=2 special-geometry structure that \code{IsPolarizedPeriodChart} specializes.

\subsection{What is proved}

At a glance, before any Lean names --- what is settled and what remains:

\begin{center}\small
\begin{tabular}{ll}
\hline
SW ingredient & status\\
\hline
curve and genus ($g=N-1$) & \textbf{proved} (standard-3)\\
period-matrix positivity ($\tau=\tau^{T}$, $\Imag\tau\succ0$) & \textbf{proved}, modulo the inherited period-basis axiom\\
the physical assumptions H0--H7 & \textbf{explicit predicates}, not hidden\\
$SU(2)$: existence \& uniqueness up to $\Gamma(2)$ duality & \textbf{theorems}, from classical citable axioms\\
$SU(2)$: explicit solution ($a$, $a_D$, $\tau$; $da_D/da=\tau$; running) & \textbf{proved} (\S6)\\
$SU(N)$ headline \& Gauss--Manin period variation & axiomatized skeleton; \textbf{future work}\\
\hline
\end{tabular}
\end{center}

From the hypotheses of \S4.2 (with the mathematical inputs of Appendix B), the following are
\textbf{sorry-free theorems}, and \code{\#print axioms} reports exactly what each rests on:

\begin{itemize}
\item \textbf{The headline --- existence and uniqueness up to duality, at genus one.} The
$SU(2)$ effective coupling is \emph{constructed}---$\tau(u) = iK'/K$ at the curve's modulus,
proved to exist on an open chart (\code{su2\_coupling\_exists})---and the hypotheses fix it
\textbf{uniquely up to a $\Gamma(2)$ duality frame}: every candidate coupling agrees with the
constructed one up to a literal M\"obius frame change
(\code{su2\_coupling\_canonical}; rigidity form \code{sw\_su2\_unique}), formalizing the
monodromy argument of~\cite{SeibergWitten1994a}. The footprints are the three logical axioms
plus classical, citable mathematics only---Jacobi inversion and the $\Gamma(2)$-covering
pair---and the physics enters as a \emph{defined} hypothesis, not an axiom. The general-$N$
statements (\code{sw\_curve\_admits\_\allowbreak effective\_theory},
\code{sw\_effective\_theory\_\allowbreak unique\_up\_to\_duality}, extended to $SU(N)$
in~\cite{KLYT1995,ArgyresFaraggi1995}) are proved in the same repository from one consolidated
period input, \code{periodRigidityAxiom} (the Gauss--Manin / Picard--Fuchs period-variation
theorem); constructing that higher-genus period geometry is future work (\S6, \S B.1).

\emph{The uniqueness argument, informally.} The smooth $SU(2)$ Coulomb branch is the $u$-plane
minus the monopole and dyon points---a thrice-punctured sphere. Any candidate effective
coupling $\tau(u)$ is holomorphic, valued in the upper half-plane $\HH$, and carries the SW
monodromy around the punctures; in our formalization the last condition is the statement that
$\tau$ \emph{develops the curve's modulus}: $\lambda(\tau(u)) = 2\Lambda^2/(u+\Lambda^2)$,
where $\lambda = \theta_2^4/\theta_3^4$ is the modular function exhibiting
$\HH/\Gamma(2) \cong \C\setminus\{0,1\}$ (the modulus map itself is \emph{pinned by
computation} against the curve's periods, \S5). So any two candidate couplings are two
\emph{lifts of the same map} through the $\Gamma(2)$ covering. Covering theory then says two
lifts agree near a point up to a deck transformation---an element of $\Gamma(2)$, acting by
M\"obius maps, which is physically an electric--magnetic duality frame change---and the
identity theorem for holomorphic functions propagates that local agreement across the connected
chart. That is the whole argument: uniqueness up to a $\Gamma(2)$ frame. Each step has its
formal counterpart---the developing condition is the definition \code{SameSWMonodromy}, the
covering and the lift-uniqueness step are the two classical axioms of \S B.2, and the
propagation is the proved identity theorem---so \code{\#print axioms} reporting exactly the
covering pair is the machine's confirmation that the informal argument used nothing else.

\emph{Why exactly three punctures.} The count itself---one weak-coupling puncture plus a
single monopole--dyon pair, \emph{assumed} in~\cite{SeibergWitten1994a}---is also a theorem,
within the algebraic Weierstrass ansatz class---a \emph{conditional} theorem, in the same
sense as everything else in this section: its physical inputs are H2$+$H3 and H7
\emph{through their stated curve/Kodaira transcriptions} (explicit hypotheses of the
theorem statement), with \textbf{no new axioms} and no additions to the
postulate roster (\code{SingularityCount.lean}; footprint standard-3). Transcribe each
finite singularity as a Kodaira $I_1$ fiber (one massless BPS hypermultiplet: the
discriminant has a simple zero and $g_2 \neq 0$ there) and the weak-coupling behavior as
$I^*_4$ (the one-loop monodromy $-T^4$); both transcriptions are \emph{definitions},
justified by Kodaira's table, and no Lean statement mentions monodromy. Polynomial degree
arithmetic then gives the Euler-number counting: the number of finite singularities is
$12\ell - 10$, with $\ell$ the twist at infinity. So monodromy data plus positivity alone
yield only $n \equiv 1 \pmod 6$ pairs---the $\ell = 2$ loophole, an elliptic K3 carrying
$I^*_4$ plus \emph{fourteen} $I_1$ fibers, is realized by an explicit polynomial witness in
the numerical audit (\code{validate\_singcount.py}), so no refinement of the monodromy
argument can ever pin $n = 1$ by itself. What closes the gap is the anomaly grading
$g_2 \in \mathrm{span}\{u^2, \Lambda^4\}$ (\code{AnomalyGraded})---itself a
\emph{theorem} (\code{anomalyGraded\_of\_rSpurionCovariant}) from the R-spurion covariance
of the curve family (\code{RSpurionCovariant}---the curve-level transcription of
\textbf{H7}, \S4.2), three manifestly physical clauses: scale
covariance (mass dimensions---$\Lambda$ is the only scale), invariance under
$\Lambda \to i\Lambda$ (the anomalous $U(1)_R$ exact with the instanton factor $\Lambda^4$
as spurion; the anomaly coefficient is one-loop exact, so this is microscopically
computable), and weak-coupling regularity (Seiberg holomorphy). The odd coefficients vanish
algebraically---$t = i$ in the scaling law contradicts quantization, the half-instanton
argument---and coefficients above $u^2$ would blow up at weak coupling. With
$\deg_u g_2 \le 2$, $\ell = 1$ is forced
(\code{singularity\_count\_pinch}): exactly two singular values, proved to be
$\{\pm\Lambda^2\}$ (\code{sw\_singular\_values}), consistent with the discriminant bullet
below. Neither ingredient suffices alone---the dimension count still allows $n = 2$, which
the mod-12 constraint kills---and the formalization makes this division of labor exact.

\item the $SU(N)$ curve~\cite{KLYT1995,ArgyresFaraggi1995} has \textbf{genus $N-1$}, and its
period matrix $\tau$ is \textbf{symmetric with $\Imag\tau \succ 0$}---positivity of the
special-K\"ahler metric, the physical no-ghost condition~\cite{SeibergWitten1994a,Lerche1997}.
These two are proved in the repository's \emph{higher-genus layer} (\code{HigherGenus/}),
which builds against the external Riemann-surface library \code{jacobian-challenge} and is
kept outside the certified build: the main library, and every footprint reported in this
paper, is self-contained on Mathlib;
\item for $SU(2)$, the curve is singular at \textbf{exactly $u = \pm\Lambda^2$}---the monopole and
dyon points of~\cite{SeibergWitten1994a}, by a discriminant computation, not lore;
\item the Picard--Lefschetz monodromy of a vanishing cycle is \textbf{symplectic}---why the
monodromy group sits in $\Sp(2r,\Z)$~\cite{Lerche1997};
\item the rank-1 modular function $\lambda = \theta_2^4/\theta_3^4$~\cite{Bilal1996} (from Mathlib's Jacobi thetas)
is proved \textbf{$\Gamma(2)$-invariant} (the generator $T^2$ directly; $S$ and $ST^2S^{-1}$ modulo the
$\theta$-identity axioms), with the cusp relation $1-\lambda = \theta_4^4/\theta_3^4$. That $\lambda$
realizes the \emph{full} covering $\mathbb{H}/\Gamma(2)\cong\mathbb{C}\setminus\{0,1\}$ is \textbf{not}
proved --- it remains the axiom \code{AX\_thrice\_punctured\_uniformization} (\S B.2).
\end{itemize}

The genus-one headline's machine-checked dependency, in full---logic plus two classical
covering facts, nothing else:

\begin{Verbatim}
#print axioms sw_su2_unique
-- depends on axioms:
--   [propext, Classical.choice, Quot.sound,   -- logic
--    AX_thrice_punctured_uniformization,      -- the Γ(2) covering  (classical)
--    AX_developing_map_rigidity]              -- lift uniqueness    (classical)
\end{Verbatim}

\noindent The exact statements, the higher-genus skeleton, and \code{periodRigidityAxiom} itself are in
Appendix B.

\subsection{What formalizing forces into the open}

Several times, making a statement precise enough for
the kernel exposed something the prose slides over.

\paragraph{The type system refuses a convenient falsehood.} Our first attempt made the periods
$a, a_D$ and the coupling $\tau$ single-valued functions of the moduli. External review flagged this
as \emph{vacuous}: a single-valued holomorphic map to the Siegel upper half-space---a bounded
domain---is bounded near the singular locus, extends across it by the Riemann removable-singularity
theorem, and is then constant by Liouville's theorem: a free theory. The data must instead live on the universal cover
of the moduli space minus its singular locus, and the corrected types encode exactly that.

\paragraph{The hypotheses kept coming out vacuously true.} The kernel does not object to an
assumption that says nothing, but a vacuous hypothesis makes the headline assert less---so each
predicate had to be hardened until it bites. A first pass wrote H3 as ``there exists a lattice map
equal to the Picard--Lefschetz transvection''---true by fiat. It now demands an \emph{actual} deck
transformation to an adjacent sheet under which the central charge transforms covariantly, a real
constraint on the periods; H2 demands a \emph{nonzero} charge become massless; H5 demands a
nontrivial finite-order linear symmetry of the moduli fixing the singularities. The most recent
instance was caught after all this hardening: H6's instanton expansion, with free holomorphic
coefficients at fixed $\Lambda$, fit \emph{any} prepotential --- the single coefficient
$c_1 := (F - F_{\rm cl} - F_1)/\Lambda^{2N}$ absorbs everything. The physical content, that the
coefficients do not depend on $\Lambda$, is invisible at one $\Lambda$ until the family's scale
covariance converts it into a weighted-homogeneity clause $c_k(ta) = t^{2-2Nk}c_k(a)$ --- now part
of the definition. The heuristic that found it: for every existential inside a hypothesis, ask
what stops the witness from being reverse-engineered from the thing being constrained.
Formalizing is what
forces the question ``could this be satisfied trivially?'' of every assumption, every time.

\paragraph{Hardening one of them caught a genuine subtlety.} Pinning H5 to ``order exactly $2N$''
then revealed that, \emph{as a statement about the moduli space}, it fails at rank~1. The
anomaly leaves $\mathbb{Z}_{4N}$ unbroken on the fields, acting on the adjoint scalar $\varphi$
through a faithful $\mathbb{Z}_{2N}$; but the Coulomb-branch coordinates are the Casimirs
$u \sim \varphi^2,\dots$---so the induced action on the moduli can have smaller order still: for
$SU(2)$, $u \to -u$, order~2, not~4. The faithful $2N$-action lives on
the $\varphi$-cover, not the $u$-plane; the textbook phrase ``the $\mathbb{Z}_{2N}$ R-symmetry acts
on the Coulomb branch'' quietly conflates the two. We found this only by trying to verify the
predicate, and corrected it: H5 now asks for a nontrivial $\mathbb{C}$-linear symmetry of order
\emph{dividing} $2N$ fixing $\Delta$---provably satisfied by the physical reflection $u \to -u$
(\code{hasFiniteOrderAutomorphism\_of\_neg\_invariant}, standard-3), no longer the unsatisfiable
``exactly $2N$''. An honest by-product of demanding non-vacuity.

\paragraph{A surprise comes out derived, not assumed.} Argyres--Douglas
points~\cite{ArgyresDouglas1995}---where the theory
becomes an interacting CFT with no Lagrangian---look as though they need their own postulate. In the
formalization they are instead a \emph{definition}: the locus where two \textbf{mutually non-local}
BPS charges (nonzero Dirac pairing) go massless together, built from the central charge and the
charge lattice already in hand. It is \emph{empty} for pure $SU(2)$---the monopole and dyon go
massless at the two different points $\pm\Lambda^2$---but the definition is general, and \S4.5
exhibits the matter case where it is provably nonempty. A phenomenon the theory should explain falls
out as a consequence---a check the axioms pass rather than a cost they incur.

\subsection{A worked check: Argyres--Douglas points from matter, axiom-free}

The sharpest test of that derived \texttt{NonLocalDegenerationLocus} is a case where it is \emph{not}
empty. Adding $N_f$ fundamental hypermultiplets deforms the curve to~\cite{SeibergWitten1994b}
(in our conventions)
\[
  y^2 = (x^2 - u)^2 - \Lambda^{4-N_f}\,\textstyle\prod_i (x - m_i)
  \qquad (N_f = 0 \text{ recovers the pure curve}),
\]
and an Argyres--Douglas point is where the curve develops a \textbf{cusp}---a triple root in $x$, two
mutually non-local singularities colliding into an interacting superconformal theory; these points
were found in $SU(2)$ SQCD by Argyres, Plesser, Seiberg and Witten~\cite{APSW1996}. Two short Lean
theorems, both \textbf{axiom-free} (standard-3, pure algebra), settle the dichotomy:
\begin{itemize}
\item with one flavour, at the tuned point $(u,m) = (\tfrac34\Lambda^2, -\tfrac34\Lambda)$ the curve
  factors \emph{exactly} as $(x + \tfrac12\Lambda)^3 (x - \tfrac32\Lambda)$---a triple root, hence a
  cusp (\texttt{swCurveMatter\_nf1\_ad}, closed by \texttt{ring});
\item pure $SU(2)$ admits \textbf{no} triple root, for any $u$: $(x^2-u)^2 - \Lambda^4$ never
  degenerates to a cusp (\texttt{not\_\allowbreak isCuspOf\_nf0}).
\end{itemize}
So in this worked example the interacting AD theory appears with matter and is algebraically absent
for pure SU(2)---the $N_f{=}1$ cusp and the pure-SU(2) no-cusp are theorems (a worked instance, not a
general iff)---and the framework's \texttt{NonLocalDegenerationLocus}, defined from data already
in hand, is non-vacuous, witnessed by an exact factorization rather than asserted. That this
tuned point \emph{lies in} \texttt{NonLocalDegenerationLocus}---the colliding states genuinely
mutually non-local---is a theorem at \textbf{standard-3}
(\code{matter\_argyresDouglasLocus\_nonempty}): the repository constructs an explicit period
chart (its first) on a ball tangent to the AD point inside the exact two-point singular locus
$\{3\Lambda^2/4,\, -15\Lambda^2/16\}$ --- the discriminant factors as
$-\Lambda^6(u - 3\Lambda^2/4)^2(u + 15\Lambda^2/16)$, by a general quartic-discriminant
bridge (\code{monic\_quartic\_squarefree\_iff\_disc}) --- with the AD point the provably
\emph{unique} cusp and the electric and magnetic unit charges (Dirac pairing $1$) both of
vanishing central charge there. One caveat, stated where the construction lives: the chart's
data is a \emph{witness}, not the SQCD solution; \code{IsMatterPolarizedPeriodChart} (special
geometry $+$ the discriminant tie) admits it, which makes formal that this predicate does not
yet pin the genuine theory --- strengthening it and constructing the quartic-period chart is
future work. The \emph{uniqueness} side needs no such construction at all: the matter
coupling's rigidity is a theorem on the classical basis --- two couplings developing the matter
curve's $j$-invariant agree on a chart up to a modular frame
(\texttt{matter\_coupling\_rigidity}, footprint: the $\theta$ pair and the covering pair
only), with the Argyres--Douglas point also characterized invariantly as $g_2 = g_3 = 0$
(axiom-free).

\section{Checking the axioms: validation by independent agreement}

Concentrating trust onto named axioms is worthwhile only if those axioms are then checked. We
use three tools, cheapest first.

\paragraph{An independent numerical oracle.} Where a statement has computable content, we
evaluate it in a separate engine (mpmath / numpy) that shares no code or authorship with the
Lean. Nine oracle suites---278 checks in all, at 30--40-digit precision---confirm the assumed
theta-function identities ($\theta_3^4 = \theta_2^4 + \theta_4^4$, $\theta_3 \neq 0$), verify that
the proved $\lambda$ transformation laws are \emph{faithful} (catching any sign or shift error),
anchor the normalizations ($\lambda(i) = \tfrac12$; the self-dual point $\tau = i$), check the
$SU(2)$ singularity locus, vet the elliptic-integral axioms of the in-progress rank-1
restructuring (\S7), and \emph{determine}---rather than take from the literature---the
identification of the curve's modulus, $m(u) = 2\Lambda^2/(u+\Lambda^2)$, by branch-tracked
quadrature of the curve's periods tested against all six M\"obius candidates. Twice the method
caught an error \textbf{in the checking apparatus itself}---a fractional power evaluated on the
wrong branch; a cycle normalization off by a factor of two, exposed by the self-dual
anchor---before agreeing with the Lean to full precision.
A numerical pass is necessary, not sufficient; it validates values, not logical structure.

\paragraph{Cross-model and self-review} against the pinned sources, recorded per result,
separating ``is it proved?'' from ``does it say what the source says?''---and from a third
question the project learned to ask separately: ``can the intended theorems be \emph{derived}
from it?''. The sharpest instance: a proposed set of elliptic-integral axioms (\S6)
passed 62 numerical checks at 40-digit precision and was still rejected by an adversarial
model review, which found three statement-level gaps invisible to sampling---a pointwise
existence supplying no holomorphic choice, missing boundary limits, and a covering axiom that
does not label which parabolic generator sits at which cusp. The corrected statements were
re-vetted and only then admitted. Sampling bounds falsity; statement-level review bounds
fitness for purpose.

\paragraph{Validating a transcription.} A dictionary entry---a \emph{definition}---cannot
be proved correct; it can be validated, and the discipline above applies to it directly. The
worked example is the singularity count's Kodaira transcription (\S4.3): ``$k$ mutually local
BPS states go massless at $u_0$'' is transcribed as the valuation data
$v(\Delta) = k$, $g_2(u_0) \neq 0$, and the one-loop monodromy $-T^m$ at infinity as the
triple $(2, 3, m{+}6)$. The bridge between the physics reading and the mathematics is
\textbf{Kodaira's classification} (fiber type $\Leftrightarrow$ valuations
$\Leftrightarrow$ monodromy class)---a citable classical theorem, referenced rather than
formalized. Four independent checks then guard the entry. \emph{Instantiation}: the actual SW
curve satisfies the transcribed predicates with the physically expected values in \emph{both}
frames ($I_1$ at $\pm\Lambda^2$ with $I_4^*$ at infinity, Euler $10{+}1{+}1 = 12$, the
rational elliptic surface; $I_2$/$I_2^*$ in the doubled frame), the two frames consistent
through the Landen 2-isogeny. The \emph{oracle} verifies the dictionary's internal joints
($j$-pole order $=$ discriminant multiplicity; $3\deg g_2 - \deg\Delta = m$ at infinity;
the Euler totals). \emph{Agreement with independently proved results}: the count reproduces
the direct discriminant computation of \S4.3 with no Kodaira input, and the proved monodromy
matrices---parabolic, in $\Gamma(2)$, with $M_{\mathrm{mono}}M_{\mathrm{dyon}} = M_\infty$
and width-2 cusps matching $\lambda \approx 16e^{i\pi\tau}$---carry exactly the classes
the transcription assigns. \emph{Adversarial content}: the predicates are falsifiable and
were once falsified---a hyperbolic $\Gamma(2)$ matrix briefly occupied a parabolic slot,
passing every property the proofs consumed (determinant, mod-2 reduction, the factorization,
$\lambda$-invariance) while violating the physics; the repair added parabolicity as a proved
lemma and an oracle check, and the lesson---pin the invariants that \emph{classify} a
transcribed object, not just those the downstream proofs use---is recorded in the audit. What
remains on trust is then two named bridges, listed rather than hidden: Kodaira's table itself,
and H3 $\Rightarrow$ the local monodromy class.

\paragraph{The physicist's triangle.} The deepest reason the SW lore is trusted is that three
independent routes to the prepotential agree: weak-coupling perturbation theory, the instanton
expansion (Nekrasov's partition function~\cite{Nekrasov2003}, itself later made
rigorous~\cite{NekrasovOkounkov2006}), and the exact periods of
the curve. This independent agreement is the empirical content behind the axioms, and our
protocol attaches it as a cross-check rather than asserting it.

\section{Remaining mathematical debt, and future work}

The discipline makes the remaining \emph{mathematical} debt legible, and lets us state our
posture toward it: the goal is a \textbf{standard} trusted base, not an empty one. At genus one
the trusted base consists of five named axioms, every one a consumed, textbook-citable classical
theorem: the $\Gamma(2)$ covering $\HH/\Gamma(2)\cong\C\setminus\{0,1\}$ and its
lift-uniqueness companion (constructed in~\cite{Ahlfors1979}; covering-space theory as
in~\cite{Forster1981}); the two $\theta$-identities, corollaries of the Jacobi triple
product~\cite{WhittakerWatson1927}; and Jacobi's inversion theorem (the $\theta$-bridge
$K = \tfrac{\pi}{2}\theta_3^2$, $\tau = iK'/K$; Whittaker--Watson \S\S21--22). We
deliberately \emph{keep these as axioms}. Proving them is a library-building exercise---worth
doing but not strictly necessary to make our points. (The covering rests on the Riemann mapping
theorem and Schwarz reflection, absent from Lean though RMT is formalized in
Isabelle/HOL~\cite{PaulsonRiemannMapping}; the repository proves the triple product's
convergence, functional equation, and non-vanishing as a head start.) None of the five resembles
the theorems it supports.

\medskip
\noindent What runs on that base is the complete analytic layer of the genus-one solution,
machine-checked. The effective coupling $\tau(u) = iK'/K$ at the curve's modulus
$m(u) = 2\Lambda^2/(u+\Lambda^2)$ is \emph{constructed} and exists on an open chart
(\code{su2\_coupling\_exists}; footprint: the three logical axioms plus Jacobi inversion
alone), and every candidate coupling agrees with it up to a literal $\Gamma(2)$ M\"obius frame
(\code{su2\_coupling\_canonical}, adding only the covering pair); the monodromy input
\code{SameSWMonodromy} is a definition, not a postulate (\S B.2), so no physical assumption sits on
this footprint. The special coordinates are closed forms,
$a = \tfrac{\sqrt2}{\pi}\sqrt{u+\Lambda^2}\,E(m)$ and
$a_D = \tfrac{\sqrt2}{\pi}i\sqrt{u+\Lambda^2}\,(K(1-m)-E(1-m))$ (pinned by contour
quadrature of $\oint\lambda_{SW}$ before formalization), and satisfy machine-checked theorems:
$a_D \to 0$ at the monopole in exactly H2's filter shape (axiom-free); the derivatives
$da/du$, $da_D/du$ in closed form, from Legendre ODEs proved by differentiation under the
integral and a formalized integration by parts (axiom-free); the special-geometry relation
$da_D/da = \tau$ on the chart (consuming only the $K \neq 0$ clause of Jacobi inversion); the
Legendre relation $EK' + E'K - KK' = \pi/2$ itself and the Wronskian formula
$d\tau/dm = -i\pi/(4m(1-m)K^2)$ it implies; and the weak-coupling statements
$a/\sqrt{u+\Lambda^2} \to 1/\sqrt2$ (axiom-free) and $u\,d\tau/du \to i/\pi$, the
one-loop running of the actual coupling. The genus-one items still open are the prepotential
and the H3 (monodromy-label) verification; the cusp-label statement the latter needs is
recorded in the repository as a named, \emph{unasserted} specification---no theorem consumes
it, so it is not an axiom.

\medskip
\noindent The \textbf{higher-genus} debt is of a different order: the Gauss--Manin /
variation-of-Hodge-structure layer over the moduli space, behind the consolidated
\code{periodRigidityAxiom} on which the $SU(N)$ skeleton runs (\S B.1). That is \textbf{future
work}. The point of the discipline is that ``is this physics right?'' becomes a precise,
prioritized list of theorems---and a documented decision about which of them are worth
building.

\section{Prospects: deriving the physical assumptions}

The hypotheses of \S4.2 are themselves \emph{consequences} of the microscopic definition of N=2
super-Yang--Mills, reached by physical arguments of varying rigor. Some of them are, on inspection,
\textbf{theorems}---and formalizing those would push the assumed frontier one level deeper, deriving
the parent N=2 structure from inputs more primitive than its own data. Three tiers.

\paragraph{Already within reach.} The \textbf{BPS bound} $M \ge |Z|$ is a positivity lemma about the
centrally-extended N=2 algebra: a Hermitian combination of supercharges has a positive-semidefinite
anticommutator matrix whose eigenvalues are $M \pm |Z|$, the BPS (short-multiplet) case being its
kernel. This is finite-dimensional linear algebra---Mathlib's positive-semidefinite API
suffices---and it derives the core of H2 from the algebra alone, with no quantum field theory.
\textbf{Dirac--Schwinger--Zwanziger quantization} splits into a theorem and a postulate: the
electromagnetic field angular momentum of a dyon pair is the antisymmetric pairing
$(q_1 g_2 - q_2 g_1)/4\pi$ (an explicit $\int \mathbf{x}\times(\mathbf{E}\times\mathbf{B})$), and
requiring angular momentum to be quantized forces that pairing into $\Z$---the integer symplectic
structure of the charge lattice (H0), with the duality group $\Sp(2r,\Z)$ (H4) its automorphisms
preserving the central charge. The computation is formalizable; the quantization is one further
named postulate, in the spirit of the others.

\paragraph{Formalizable, but needing infrastructure.} Special geometry (H1) follows from N=2
superspace invariance of the vector-multiplet action---formalizable once N=2 superspace is built;
the one-loop exactness behind H6 rests on holomorphy and nonrenormalization (more tractable than the
loop integral it constrains); the discrete R-symmetry (H5) is what the chiral anomaly leaves of
$U(1)_R$, an index computation. The family covariance (H7) factors unusually well across these
tiers: its $\theta$-periodicity clause is \textbf{instanton-number quantization}---$\int
\mathrm{tr}\,F\wedge F/8\pi^2 \in \Z$, a Chern--Weil integrality statement, mathematics in
disguise like the Dirac pairing, formalizable given characteristic-class infrastructure---combined
with the \emph{same} one-loop-exact anomaly coefficient as H5 (Adler--Bardeen); and that the
Witten-effect shift is an \emph{integer symplectic} matrix then follows from H4, only its value
being dynamical. Its scale clause is dimensional transmutation, definitional once the
$\Lambda$-family is presented as an RG orbit---the residual assumption being that $\Lambda$ is
the \emph{only} coupling. Real, but substantial.

\paragraph{Beyond reach, for now.} That N=2 SYM \emph{exists} as an interacting four-dimensional
theory, with these multiplets and a BPS spectrum carried by genuine states, presupposes constructing
the quantum field theory---the same barrier as the solution itself. The algebra is exactly what one
gets to \emph{assume}; its realization is what cannot yet be assumed away.

\medskip
The lesson mirrors the body. Just as the headline reduced to physics plus standard mathematics, the
physics itself partly reduces: the BPS bound and the Dirac pairing are mathematics in disguise, and
formalizing them would move the frontier from ``assume special geometry, the BPS bound, and a
symplectic lattice'' to ``assume the supersymmetry algebra and angular-momentum quantization.'' Each
such step shrinks what must be taken on trust.

\section{Conclusion}

A rigorous proof of the Seiberg--Witten solution lies beyond reach---it presupposes
constructing the quantum field theory itself---yet the result is as certain as anything in
physics. A proof assistant can still treat it rigorously: by separating the machine-checked
consequences from the physical lore, turning the lore into auditable postulates, and validating those
postulates by independent agreement. Proved and assumed as separate, machine-checked columns; trust
narrowed to a short vetted list; faithfulness enforced by types and by an independent oracle:
this, we argue, is an effective standard for validating AI-generated results in theoretical
physics. The present work is a proof of concept; as AI-generated results grow in size and
scope, validation will become increasingly important.
A natural follow-up is to enlarge the scope from a paper to a broader subtopic within physics, and
identify and formalize a standard set of physical
postulates (this is work in progress for quantum field theory).

\section*{Acknowledgments}
This formalization and paper were developed with heavy use of Claude (Anthropic), and with
Gemini (Google) and Codex (OpenAI) for cross-checking, second opinions, and review. I thank
Jeremy Avigad and Sergey Cherkis for reading the manuscript and for helpful discussions, Sven Krippendorf and Joseph Tooby-Smith
for a helpful survey of the state of physics formalization at the Aspen Center for Physics, and
David Kosower and Jesse Thaler for discussions at IHES on the validation of amplitude computations for
collider physics, which informed the broader perspective on validation taken here.  I also thank
the contributors to {\tt mrdouglasny/jacobian-challenge} and especially Rado Kirov, whose results 
were helpful for this project.

\bibliography{swrefs}

\appendix

\section{The physics hypotheses (H0--H7) --- predicates, not axioms}

The physical inputs are \textbf{contentful predicates and
structures},  they are \emph{assumed as hypotheses} (bundled in
\code{IsPolarizedPeriodChart}) by the results that use them, so they never enter the trusted base.
The carrier itself \emph{is} the data of an N=2 $U(1)^{N-1}$ EFT (H0). None of the following is
an \code{axiom}.

\paragraph{One principle, specialized.} The eight are not independent postulates but facets of
\textbf{N=2 supersymmetry} read off the Coulomb branch: Coulomb-phase Higgsing furnishes the
carrier (H0); SUSY fixes the special-K\"ahler prepotential
(H1) and the central-charge BPS bound (H2); the BPS spectrum then dictates the monodromy (H3) and,
with the symplectic charge lattice, electric--magnetic duality (H4); the chiral anomaly fixes the
discrete R-symmetry (H5); the N=2 nonrenormalization theorem fixes the weak-coupling form (H6);
and, read at the level of the $\Lambda$-family, dimensional transmutation and $\theta$-angle
periodicity through the anomaly give the spurion covariance (H7).
Only the \emph{gauge data}---the group $SU(N)$, its one-loop $\beta$-function coefficient (asymptotic
freedom), and the dynamical scale $\Lambda$---is added to single out this theory. A natural refactor,
flagged as future work, is to formalize that parent \textbf{once}: an abstract N=2 special-geometry /
BPS Coulomb branch (special coordinates, charge lattice with Dirac pairing, central charge with the
BPS bound, anomaly-discrete R-symmetry, nonrenormalized prepotential), with \code{IsPolarizedPeriodChart}
obtained as its specialization at $SU(N)$, $\Lambda$. The hypotheses below would then be \emph{derived
projections} of one structure rather than eight siblings, and the matter and higher-rank theories
would follow by changing only the gauge data.

\begin{Verbatim}
-- H0  carrier = the data of an N=2 U(1)^{N-1} EFT
structure PeriodBase (r : ℕ) where
  Δ : Set (Fin r → ℂ); U : Set (Fin r → ℂ)
  hUopen : IsOpen U; hUsmooth : U = Δᶜ
structure PeriodChart (B : PeriodBase r) where
  V : Set (Fin r → ℂ); hVopen : IsOpen V; hVsub : V ⊆ B.U
  hVsc : SimplyConnectedSpace V
  a aD : (Fin r → ℂ) → (Fin r → ℂ)      -- special coordinates and duals (holomorphic)
  tau  : (Fin r → ℂ) → SiegelUpperHalfSpace r   -- coupling τ (Im > 0 typed)

-- H1  special geometry: a prepotential F with aD = ∂F/∂a, τ = ∂²F/∂a²
def PeriodChart.SpecialGeometry (s : PeriodChart B) : Prop :=
  ∃ F, ContDiffOn ℂ 2 F (s.a '' s.V) ∧
    (∀ u ∈ s.V, ∀ i, s.aD u i = partialDeriv F i (s.a u)) ∧
    (∀ u ∈ s.V, ∀ i j, (s.tau u).val i j = partialDeriv2 F i j (s.a u))

-- H2  massless on Δ as the limit Z_n → 0; massive off Δ
def PeriodChart.PeriodVanishesAt (s) (u₀) (n) : Prop :=
  Tendsto (fun u => s.periodCombination u n) (nhdsWithin s.V u₀) (nhds 0)
def PeriodChart.PeriodsDegenerateOnBoundary (s) : Prop :=
  (∀ u ∈ s.V, ∀ n ≠ 0, s.periodCombination u n ≠ 0) ∧
  (∀ u₀ ∈ closure s.V ∩ B.Δ, ∃ n ≠ 0, s.PeriodVanishesAt u₀ n)

-- H3  Picard-Lefschetz: the monodromy IS an actual deck transformation acting as the
--     reflection in the SAME vanishing charge n as H2 (not the vacuous ∃ g, g = transvection n)
def PicardLefschetzAtGenericStratum (s : PeriodChart B) : Prop :=
  ∀ u₀ ∈ closure s.V ∩ B.Δ, ∀ n, n ≠ 0 → s.PeriodVanishesAt u₀ n →
    ∃ (s' : PeriodChart B) (D : SymplecticReframing s s'), D.g = transvection n

-- H4  duality gluing: a ℤ-linear (Sp(2r,ℤ)) charge automorphism, covariant central charge
structure SymplecticReframing (s s' : PeriodChart B) where
  g : CycleLattice r ≃ₗ[ℤ] CycleLattice r
  symplectic : ∀ n n', intersectionForm (g n) (g n') = intersectionForm n n'
  covariant  : ∀ u ∈ s.V ∩ s'.V, ∀ n, s'.periodCombination u (g n) = s.periodCombination u n

-- H5  R-symmetry: a nontrivial ℂ-linear automorphism of order dividing 2N, fixing Δ
def HasFiniteOrderAutomorphism (B : PeriodBase r) (N : ℕ) : Prop :=
  ∃ ω : (Fin r → ℂ) →ₗ[ℂ] (Fin r → ℂ), ω ≠ LinearMap.id ∧
    (∃ k, 0 < k ∧ k ∣ 2*N ∧ (⇑ω)^[k] = id) ∧ (⇑ω) '' B.Δ = B.Δ

-- H6  one-loop over ROOTS (eigenvalue differences; nonzero for SU(2)) + instantonic tail
def Instantonic (Λ) (N) (F) : Prop :=     -- fixed classical part, Λ≠0, holomorphic coeffs
  Λ ≠ 0 ∧ ∃ c, (∀ k, Differentiable ℂ (c k)) ∧
    (∀ k t, t ≠ 0 → ∀ a,                       -- weight 2−2Nk: the coefficients'
      c k (t • a) = t^(2 - 2*N*k : ℤ) * c k a) ∧  --   Λ-independence, at fixed Λ
    ∀ a, F a - classicalPrepotential a - oneLoopPrepotential Λ a
         = ∑' k, c (k+1) a * (Λ^(2*N))^(k+1)
def PeriodChart.HasPrescribedAsymptotics (s) (Λ) (N) : Prop :=    -- H1's F + non-renormalized form
  ∃ F, (... the H1 relations for F ...) ∧ Instantonic Λ N F

-- H7  spurion covariance of the Λ-family: transmutation + θ-periodicity, the Witten
--     frame shift an integer symmetric matrix CONSTANT across the family
structure SpurionCovariantFamily (N) (F : ℂ → (Fin r → ℂ) → ℂ) : Prop where
  scale       : ∀ t Λ, t ≠ 0 → ∀ a, F (t*Λ) (t • a) = t^2 * F Λ a
  theta_shift : ∀ ζ, ζ^(2*N) = 1 → ∃ B : Matrix (Fin r) (Fin r) ℤ, B.IsSymm ∧
                  ∀ Λ a, F (ζ*Λ) a = F Λ a + (1/2) * ∑ i, ∑ j, (B i j : ℂ) * a i * a j

-- H0-H6, bundled at fixed Λ (H7 is family-level, carried separately):
--   an N=2 U(1)^{N-1} Seiberg-Witten effective theory
structure IsPolarizedPeriodChart (s : PeriodChart B) (Λ : ℂ) (N : ℕ) : Prop where
  specialGeometry : s.SpecialGeometry            -- H1
  singularities   : s.PeriodsDegenerateOnBoundary        -- H2
  picardLefschetz : PicardLefschetzAtGenericStratum s   -- H3
  matching        : s.HasPrescribedAsymptotics Λ N     -- H6
  rSymmetry       : HasFiniteOrderAutomorphism B N                -- H5
\end{Verbatim}

\noindent \code{SymplecticReframing} (H4) relates sheets and is proved to make the BPS mass descend to the
base (\code{SymplecticReframing.periodNorm\_eq}). PeriodCharts are organized into an \code{PeriodAtlas} (covering \code{B.U},
overlaps \code{SymplecticReframing}-glued), so the duality gluing H4 is \emph{part of the theory} and uniqueness
is stated at the atlas level (\code{sw\_unique\_up\_to\_duality}). The rank-1 \emph{monodromy}
input \code{SameSWMonodromy} is a \emph{definition}: two
candidate couplings $f,g$ both develop the curve's modulus $2\Lambda^2/(u+\Lambda^2)$ on the
chart---physically, which BPS state (monopole at $+\Lambda^2$, dyon at $-\Lambda^2$) goes
massless where---the hypothesis of the rank-1 rigidity theorem \code{sw\_su2\_unique}, whose
kernel footprint carries no physical postulate --- only mathematical axioms.

\section{The residual mathematical axioms and the headline theorems}

With the physics in predicates (Appendix A), the global axioms beyond the three
logical ones (\code{propext, Classical.choice, Quot.sound}) are \emph{mathematical} --- all of
them: the monodromy input \code{SameSWMonodromy} is a definition
(\S B.2). The genus-one theorems of this paper run on the classical covering/lift/$\theta$/inversion
axioms of \S B.2 alone. The higher-genus skeleton (B.1) proves the general-$N$ headline
implications (no \code{sorry}) from the physical hypotheses plus a single consolidated math
axiom---\code{periodRigidityAxiom}; constructing that period geometry is future work.

\medskip
\medskip
\noindent\textbf{B.0 --- Dictionary.} The math$\leftrightarrow$physics translation is in \S4.1; the
axioms and statements below use the mathematical names (\code{\#print axioms} reports them).

\medskip
\noindent\textbf{B.1 --- Higher genus (future work): the $SU(N)$ headline theorems and the consolidated period axiom.} The period-level
(Picard--Fuchs / Gauss--Manin) geometry of the SW curve family is taken as one axiom --- a
\textbf{coarse} package: its \code{realize} clause still bundles the period construction
($\oint\lambda_{SW}$ and the H1--H6 verification, \S B.3), not yet itemized. The headline follows, \code{\#print axioms} $=$ standard-3 $+$ \code{periodRigidityAxiom} (no \code{sorry}):

\begin{Verbatim}
-- the single consolidated period-level math axiom (the SW period geometry exists)
axiom periodRigidityAxiom (N : ℕ) (Λ : ℂ) (hN : 2 ≤ N) : PeriodRigidity N Λ

-- HEADLINE (proved): uniqueness up to Sp(2(N-1),ℤ) duality, on a connected chart overlap
theorem sw_effective_theory_unique_up_to_duality (hN : 2 ≤ N) (s s' : PeriodChart B)
    (hconn : IsConnected (s.V ∩ s'.V))
    (h : IsPolarizedPeriodChart s Λ N) (h' : IsPolarizedPeriodChart s' Λ N) :
    Nonempty (SymplecticReframing s s') :=
  sw_unique_of_swPeriodLayer (periodRigidityAxiom N Λ hN) s s' hconn h h'

-- HEADLINE (proved): existence — the SW curve (P monic, degree N, trace-free) realizes a theory
theorem sw_curve_admits_effective_theory (hN : 2 ≤ N) (P : Polynomial ℂ)
    (hPm : P.Monic) (hPdeg : P.natDegree = N) (hPtr : P.coeff (N - 1) = 0)
    (hsf : Squarefree (P ^ 2 - Polynomial.C (Λ ^ (2 * N)))) :
    ∃ (B : PeriodBase (N - 1)) (s : PeriodChart B), IsPolarizedPeriodChart s Λ N ∧
      B.Δ = {u | ¬ Squarefree (swCurvePoly N Λ u)} ∧ swModulus N P ∈ s.V :=
  sw_exists_of_swPeriodLayer (periodRigidityAxiom N Λ hN) P hPm hPdeg hPtr hsf

-- PROVED (standard-3): the classical Coulomb branch has dimension N − 1 (the rank)
theorem coulombBranchDim (N : ℕ) : Module.finrank ℂ (Fin (N - 1) → ℂ) = N - 1
\end{Verbatim}

\medskip
\noindent\textbf{B.2 --- Classical mathematics not yet in Mathlib} --- the only remaining global
axioms, to discharge by porting (the covering is packaged as a structure):

\begin{Verbatim}
structure ThricePuncturedUniformization where
  cover : UpperHalfPlane → {v : ℂ // v ∉ ({0, 1} : Set ℂ)}      -- the developing map λ
  gamma2_invariant : ∀ γ ∈ Gamma2, ∀ τ, cover (γ • τ) = cover τ
  surjective : Function.Surjective cover
  fiber : ∀ τ τ', cover τ = cover τ' ↔ ∃ γ ∈ Gamma2, γ • τ = τ' -- fibres = Γ(2)-orbits

-- the Γ(2) covering ℍ/Γ(2) ≅ ℂ\{0,1} exists   (discharge: Schwarz reflection ⇒ RMT ⇒ cover)
axiom AX_thrice_punctured_uniformization : Nonempty ThricePuncturedUniformization

-- lift uniqueness: same-monodromy developing maps agree up to a modular frame change
-- (discharge: classical; Forster, Ahlfors)
-- SameSWMonodromy is a DEFINITION: both maps are developing maps of the pinned
-- modulus (holomorphic, ℍ-valued, λ∘f = swCrossRatio; every clause load-bearing)
def IsSWDevelopingMap (Λ : ℂ) (D : Set ℂ) (f : ℂ → ℂ) : Prop :=
  AnalyticOnNhd ℂ f D ∧ (∀ u ∈ D, 0 < (f u).im) ∧ DevelopsSWCrossRatio Λ D f
def SameSWMonodromy (Λ : ℂ) (D : Set ℂ) (f g : ℂ → ℂ) : Prop :=
  IsSWDevelopingMap Λ D f ∧ IsSWDevelopingMap Λ D g

-- (v2: generic base map — two analytic ℍ-valued lifts with the same λ-image
--  agree near a point up to a Γ(2) deck transformation; the SW-specialized
--  form is recovered at the call site by unpacking SameSWMonodromy)
axiom AX_developing_map_rigidity
    {D : Set ℂ} {u₀ : ℂ} {f g : ℂ → ℂ}
    (U : ThricePuncturedUniformization) (hD : IsOpen D) (hu₀ : u₀ ∈ D)
    (hf : AnalyticOnNhd ℂ f D) (hfH : ∀ u ∈ D, 0 < (f u).im)
    (hg : AnalyticOnNhd ℂ g D) (hgH : ∀ u ∈ D, 0 < (g u).im)
    (hbase : ∀ u ∈ D, modularLambdaFn (f u) = modularLambdaFn (g u)) :
    ∃ γ ∈ Gamma2, f =ᶠ[nhds u₀] fun u => moebiusOn γ (g u)

-- Jacobi quartic identity and  theta3 ≠ 0      (discharge: Jacobi triple product)
axiom AX_jacobi_quartic (τ : UpperHalfPlane) :
    theta3 (τ : ℂ) ^ 4 = theta2 (τ : ℂ) ^ 4 + theta4 (τ : ℂ) ^ 4
axiom AX_theta3_ne_zero (τ : UpperHalfPlane) : theta3 (τ : ℂ) ≠ 0

-- the family's local monodromy is the Picard-Lefschetz transvection
-- (discharge: Gauss-Manin / local-system layer over the moduli space)
axiom localMonodromy : ∀ {r : ℕ}, CycleLattice r → (CycleLattice r → CycleLattice r)
axiom AX_picard_lefschetz_local {r : ℕ} (γ : CycleLattice r) :
    localMonodromy γ = transvection γ

\end{Verbatim}

\noindent Each of these is classical mathematics with a standard source: the $\Gamma(2)$ covering
$\HH/\Gamma(2)\cong\C\setminus\{0,1\}$ and the modular $\lambda$ function are constructed
in~\cite{Ahlfors1979}; the lifting/rigidity of developing maps is covering-space theory as
in~\cite{Forster1981}; the Jacobi quartic identity and the non-vanishing of $\theta_3$ follow from
the Jacobi triple product~\cite{WhittakerWatson1927} (of which the repository proves the
product's convergence, functional equation, and non-vanishing; the identity itself is kept as an
axiom by decision); and the Picard--Lefschetz formula is
in~\cite{AGZV1988}. The beta function needs no axiom at all: its mathematical input, the
weak-coupling logarithmic running of the period ratio, is a theorem---proved both in an
existential form and in the curve-tied form $u\,d\tau/du \to i/\pi$ for the explicit genus-one
coupling---so \code{betaFunction\_weakCoupling} rests on the three logical axioms alone. (The
audit records a fidelity finding from this proof: the original existential statement had never
been formally tied to the curve, which is what the curve-tied form repairs.)

\medskip
\noindent\emph{Repository note.} The development additionally declares one
elliptic-integral axiom, \code{AX\_\allowbreak elliptic\_\allowbreak inversion}
(Jacobi's inversion theorem), belonging to the rank-1 classical basis described in
\S6 --- Whittaker--Watson-citable, numerically vetted, adversarially reviewed. It is
\textbf{not on the footprint of the rank-1 rigidity headline} (\code{sw\_su2\_unique}
reports the covering pair only); it \emph{is} the classical input of the explicit
genus-one coupling layer --- existence (\code{su2\_coupling\_exists}), the canonical
form, and the special-coordinate and running results of \S4.3 report it, as the golden
trace records. The cusp-label
statement \code{AX\_tau\_\allowbreak cusp\_zero} is a named but \emph{unasserted}
specification (no theorem consumes it, so it is not an axiom). The Legendre relation
and the $K'$ logarithmic cusp asymptotic are \emph{theorems}: the former rests on
the three logical axioms alone (Legendre ODEs by differentiation under the integral
and a formalized integration by parts, constancy on the star-shaped parameter
domain, the cusp constant), the latter is proved by an elementary-model comparison.

\medskip
\noindent The machine's dependency printout for the rank-1 uniqueness theorem makes the separation
literal---logic, classical-math debt, and the one physical input, in five lines:

\begin{Verbatim}
#print axioms sw_su2_unique
-- 'sw_su2_unique' depends on axioms:
--   [propext, Classical.choice, Quot.sound,      -- logic
--    AX_thrice_punctured_uniformization,         -- classical math (Γ(2) covering)
--    AX_developing_map_rigidity]                  -- classical math (lift uniqueness)
-- (the physics — SameSWMonodromy — is a defined hypothesis in the type, not an axiom)
\end{Verbatim}

\noindent The $SU(2)$ uniqueness theorem \code{sw\_su2\_unique} rests on exactly the two
covering/lift axioms (\code{AX\_\allowbreak thrice\_\allowbreak punctured\_\allowbreak uniformization},
\code{AX\_developing\_map\_\allowbreak rigidity})---and the three
logical axioms (\code{propext}, \code{Classical.choice}, \code{Quot.sound}), which underlie
everything and belong to neither list. Its physics input, \code{SameSWMonodromy}, is a
\emph{definition} carried in the theorem's type, and its conclusion is a literal
$\Gamma(2)$ deck transformation ($\exists\, \gamma \in \Gamma(2)$ acting as a M\"obius map)
--- not an unconstrained reframing function. (The physical refinement \code{H4'Duality} and its
derived consequence \code{metric\_posDef\_of\_h4'}---electric--magnetic duality keeps the
special-K\"ahler metric positive along the whole monodromy orbit---are proved, standard-3.)

\medskip
\noindent\textbf{B.3 --- The period-level layer (a structure; its existence is \S B.1's single axiom).} The monodromy content behind
\code{SameSWMonodromy}'s definition is itself the conclusion of the \emph{periods} of the SW
curve---their Picard--Fuchs equation and Gauss--Manin monodromy. We package that layer as a structure and prove
the B.1 goals modulo it, for SU(2) and for general SU($N$):

\begin{Verbatim}
-- the period-level debt, bundled as a *hypothesis* (so the theorems stay standard-3)
structure PeriodRigidity (N : ℕ) (Λ : ℂ) where
  hN : 2 ≤ N                                            -- SU(N) needs rank N-1 ≥ 1
  rigidity : ∀ {B : PeriodBase (N-1)} (s s' : PeriodChart B), IsConnected (s.V ∩ s'.V) →
      IsPolarizedPeriodChart s Λ N → IsPolarizedPeriodChart s' Λ N → Nonempty (SymplecticReframing s s')
  realize  : ∀ P : Polynomial ℂ, P.Monic → P.natDegree = N → P.coeff (N-1) = 0 →
      Squarefree (P^2 - Polynomial.C (Λ^(2*N))) → ∃ (B : PeriodBase (N-1)) (s : PeriodChart B),
        IsPolarizedPeriodChart s Λ N ∧ B.Δ = {u | ¬ Squarefree (swCurvePoly N Λ u)} ∧ ...

-- the B.1 goals, now THEOREMS modulo the layer (all standard-3):
theorem sw_unique_of_swPeriodLayer (PL : PeriodRigidity N Λ) ... : Nonempty (SymplecticReframing s s')
theorem sw_exists_of_swPeriodLayer (PL : PeriodRigidity N Λ) ... : ∃ B s, IsPolarizedPeriodChart ...

-- rank-1 uniqueness routes through an AXIOM-FREE lemma (frame builds the gluing; covariance
-- proved from det = 1):
theorem su2_deck_of_periodFrame (s s' : PeriodChart B) (α β γ δ : ℤ) (hdet : α*δ - β*γ = 1)
    (hper : ...period frame on the overlap...) : Nonempty (SymplecticReframing s s')  -- 3 logical axioms only
\end{Verbatim}

\noindent So ``period frame $\Rightarrow$ duality equivalence'' is \emph{proved}; only the period
frame (the layer's \code{rigidity}) is assumed, as honest math debt. Taking the layer's
\emph{existence} as the single axiom \code{periodRigidityAxiom} (\S B.1) discharges that hypothesis once,
so the \textbf{named} headline theorems are closed, with \code{\#print axioms} $=$ standard-3 $+$
\code{periodRigidityAxiom}. Discharging the layer---the
period map $\oint \lambda_{SW}$, its Picard--Fuchs ODE and Gauss--Manin monodromy, the rigidity
argument---is a few weeks at genus 1 (the elliptic case, where the $\lambda$/$\theta$ machinery
already exists) and a Mathlib-scale variation-of-Hodge-structure project in general genus. A first
version was caught (adversarial review) asserting a single globally-constant $SL(2,\mathbb{Z})$
frame across a possibly-disconnected overlap, and quantifying over the U($N$) rather than SU($N$)
family; both are corrected (\code{IsConnected} overlaps; monic trace-free $P$).

\medskip
\noindent\textbf{The mathematical input, stated plainly.} Collected, the headline's entire
mathematical debt is \emph{one} classical object---the \textbf{variation of Hodge structure of the
Seiberg--Witten curve family}: the periods $\oint \lambda_{SW}$ varying holomorphically over the
moduli $u$, with their Picard--Fuchs equation and $Sp(2r,\mathbb{Z})$ Gauss--Manin monodromy. The
B.2 axioms are not independent inputs; they are exactly its \textbf{genus-1 classical pieces}---the
$\Gamma(2)$ uniformization $\mathbb{H}/\Gamma(2)\cong\mathbb{C}\setminus\{0,1\}$ and developing-map
rigidity (the rank-1 period map and its monodromy/rigidity), the Picard--Lefschetz transvection,
and two Jacobi $\theta$ identities---and B.3 packages the same object as a structure at all ranks.
The fiber side already exists: the SW curve embeds in \code{jacobian-challenge}'s hyperelliptic
type with genus 1 proved (\code{swEllipticData\_genus}, in the unbuilt \code{HigherGenus/}
layer), and that library supplies the
per-fiber periods, Riemann-bilinear positivity~\cite{GriffithsHarris1978}, Siegel/$\theta$. The single capability that
remains---at \emph{every} rank---is the \textbf{variation}: that period integrals move
holomorphically with a flat Gauss--Manin connection ($Sp$-monodromy), not yet formalized in Lean.
The whole result reduces to that one capability: a few months at genus 1 (on the existing
$\mathbb{H}$/modular/$\lambda$/$\theta$ machinery), a Mathlib-scale project for general SU($N$).

\end{document}
