Proposition 3.1.1 — (anti-)self-dual connections are absolute minimizers of Yang-Mills (box version)

Proved

UhlenbeckGauge.selfDual_absolute_minimizer

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometrygauge-theorymathematical-physicsyang-mills

Let $a,b\in\mathbb R^4$ , $\Omega=[a,b]$ the closed box, and let $A$ , $B$ be smooth $SU(n)$ -connections on the trivial bundle with the same boundary data, $A=B$ at every point of $\partial\Omega$ . Suppose the curvature of $A$ is self-dual at every point of $\Omega$ , or anti-self-dual at every point of $\Omega$ . Then

\mathrm{Ym}_\Omega(A)=\int_\Omega|F_A|^2\,d\mathrm{vol}\ \le\ \int_\Omega|F_B|^2\,d\mathrm{vol}=\mathrm{Ym}_\Omega(B).

That is, solutions of the (anti-)self-dual Yang–Mills equations are absolute minimizers of the Yang–Mills functional among connections with the same boundary values.

Formalization Note The notes state the result within a topological class $c_2(P)=k$ on a general bundle over a four-manifold with boundary; here the bundle is the trivial $SU(n)$ -bundle over a closed axis-parallel box in Euclidean $\mathbb R^4$ , so there is a single topological class. Connections are smooth on all of $\mathbb R^4$ .

Preamble

import Definitions.Def_uhlenbeck_gauge_box_defs

open UhlenbeckGauge

Formal statement

namespace UhlenbeckGauge

theorem selfDual_absolute_minimizer {n : ℕ} (a b : R4) (A B : Connection n)
    (hA : IsSUConnection A) (hB : IsSUConnection B)
    (hbdry : ∀ x, OnBoxBoundary a b x → A x = B x)
    (hdual : (∀ x ∈ Set.Icc a b, IsSelfDual (curvature A x)) ∨
      (∀ x ∈ Set.Icc a b, IsAntiSelfDual (curvature A x))) :
    yangMills a b A ≤ yangMills a b B := by sorry

end UhlenbeckGauge

Source

K. Uhlenbeck, *Equations of Gauge Theory*, lecture notes by L. Fredrickson (Emil Grosswald Lectures, Temple University, February 7-9, 2012), Chapter 3, Section 3.1, pp. 29-32, Proposition 3.1.1 (p. 31)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent that drafted the statements; non-blind

Disclosure: this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, at the explicit direction of the proposal owner, with full knowledge of the source notes and of the intended meaning. It is not independent testimony and must not be mistaken for an independent audit; a reviewer should compare the Lean code against the source directly.

For every natural number $n$ , all $a,b\in\mathbb R^4$ (no ordering assumed; if $a_\mu>b_\mu$ for some $\mu$ the box is empty), and all maps $A,B:\mathbb R^4\to(\{0,1,2,3\}\to\mathrm{Mat}_n(\mathbb C))$ such that

$A$ and $B$ are $SU(n)$ -connections: every matrix entry of every coefficient is $C^\infty$ on all of $\mathbb R^4$ , and every coefficient at every point is skew-Hermitian with trace $0$ ;
$A(x)=B(x)$ (all four coefficients) at every point $x$ of the boundary of the box, i.e. every $x$ with $a_\mu\le x_\mu\le b_\mu$ for all $\mu$ and $x_\mu\in\{a_\mu,b_\mu\}$ for at least one $\mu$ ;
either $\star F_A(x)=F_A(x)$ for every $x$ in the closed box $[a,b]$ , or $\star F_A(x)=-F_A(x)$ for every $x\in[a,b]$ ,

the inequality

\int_{[a,b]}|F_A(x)|^2\,dx\ \le\ \int_{[a,b]}|F_B(x)|^2\,dx

holds. Here $F_A(x)_{\mu\nu}=\partial_\mu A_\nu-\partial_\nu A_\mu+A_\mu A_\nu-A_\nu A_\mu$ at $x$ , $(\star F)_{\mu\nu}=\tfrac12\sum_{\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}F_{\rho\sigma}$ , $|F|^2=\sum_{\mu<\nu}\operatorname{Re}\operatorname{tr}(F_{\mu\nu}F_{\mu\nu}^*)$ , and the integrals are Lebesgue integrals over the closed box. No condition on derivatives of $A,B$ at the boundary is imposed beyond equality of values there; no condition is placed on the curvature of $B$ . For an empty box both sides are $0$ . The zero connection satisfies all hypotheses on $A$ (its curvature is $0$ , which is both self-dual and anti-self-dual).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph