Proposition 3.1.1 (equality case) — equality iff $F_A$ is self-dual or anti-self-dual

Proved

UhlenbeckGauge.yangMills_eq_boundaryChernSimons_iff

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

differential-geometrygauge-theorymathematical-physicsyang-mills

Let $a,b\in\mathbb R^4$ with $a_\mu<b_\mu$ for every $\mu$ , $\Omega=[a,b]$ , and let $A$ be a smooth $SU(n)$ -connection. Then

\mathrm{Ym}_\Omega(A)=-\operatorname{Re}\int_{\partial\Omega}CS(A)\iff \star F_A=F_A\text{ on }\Omega,

\mathrm{Ym}_\Omega(A)=\operatorname{Re}\int_{\partial\Omega}CS(A)\iff \star F_A=-F_A\text{ on }\Omega.

This is the equality statement "with equality if, and only if, $D_A$ is self-dual or anti-self-dual" in the proof of Proposition 3.1.1, for the trivial bundle over a non-degenerate box.

Preamble

import Definitions.Def_uhlenbeck_gauge_box_defs

open UhlenbeckGauge

Formal statement

namespace UhlenbeckGauge

theorem yangMills_eq_boundaryChernSimons_iff {n : ℕ} (a b : R4) (hab : ∀ μ, a μ < b μ)
    (A : Connection n) (hA : IsSUConnection A) :
    (yangMills a b A = -(boundaryChernSimons a b A).re ↔
        ∀ x ∈ Set.Icc a b, IsSelfDual (curvature A x)) ∧
      (yangMills a b A = (boundaryChernSimons a b A).re ↔
        ∀ x ∈ Set.Icc a b, IsAntiSelfDual (curvature A x)) := 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, proof of Proposition 3.1.1, equality case (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$ with $a_\mu<b_\mu$ strictly for every $\mu$ (so the box has positive volume), and every $SU(n)$ -connection $A$ (entries $C^\infty$ on $\mathbb R^4$ , values skew-Hermitian and traceless), with $\mathcal B=\operatorname{Re}\int_{\partial[a,b]}CS(A)$ as in the definitions file, both of the following equivalences hold:

$\mathrm{Ym}_{[a,b]}(A)=-\mathcal B$ if and only if, for every $x$ in the closed box $[a,b]$ , $\star F_A(x)=F_A(x)$ (equality of the whole $4\times4$ family of matrices);
$\mathrm{Ym}_{[a,b]}(A)=\mathcal B$ if and only if, for every $x\in[a,b]$ , $\star F_A(x)=-F_A(x)$ .

Here $(\star F)_{\mu\nu}=\tfrac12\sum\varepsilon_{\mu\nu\rho\sigma}F_{\rho\sigma}$ and $\mathrm{Ym}_{[a,b]}(A)=\int_{[a,b]}|F_A|^2$ . The conditions are required at every point of the closed box, including its boundary, not almost everywhere.

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

Proposition 3.1.1 (equality case) — equality iff FAF_AFA​ is self-dual or anti-self-dual

Proposition 3.1.1 (equality case) — equality iff $F_A$ is self-dual or anti-self-dual