Proposition 3.1.1 (energy bound) — $\mathrm{Ym}(D_A)\ge\mp\int_{\partial M}CS(A)$ on a box

Proved

UhlenbeckGauge.yangMills_ge_boundaryChernSimons

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

differential-geometrygauge-theorymathematical-physicsyang-mills

Let $a\le b$ in $\mathbb R^4$ , $\Omega=[a,b]$ , and let $A$ be a smooth $SU(n)$ -connection. Then

\mathrm{Ym}_\Omega(A)\ge-\operatorname{Re}\int_{\partial\Omega}CS(A)\qquad\text{and}\qquad \mathrm{Ym}_\Omega(A)\ge\operatorname{Re}\int_{\partial\Omega}CS(A).

Thus the Yang–Mills energy is bounded below by a quantity depending only on the boundary values of the connection; this is the inequality $\mathrm{Ym}(D_A)\ge8\pi^2c_2(P)+\int_{\partial M}CS(A)$ of the proof of Proposition 3.1.1, in both sign versions, for the trivial bundle over a box.

Preamble

import Definitions.Def_uhlenbeck_gauge_box_defs

open UhlenbeckGauge

Formal statement

namespace UhlenbeckGauge

theorem yangMills_ge_boundaryChernSimons {n : ℕ} (a b : R4) (hab : a ≤ b)
    (A : Connection n) (hA : IsSUConnection A) :
    -(boundaryChernSimons a b A).re ≤ yangMills a b A ∧
      (boundaryChernSimons a b A).re ≤ yangMills a b A := 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 (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\le b_\mu$ for every $\mu$ , and every $SU(n)$ -connection $A$ (entries $C^\infty$ on $\mathbb R^4$ , values skew-Hermitian and traceless), writing $\mathcal B=\operatorname{Re}\big(\int_{\partial[a,b]}CS(A)\big)$ for the real part of the boundary Chern–Simons term (the oriented sum over $\mu$ of the integrals of $K^\mu(A)$ over the face $x_\mu=b_\mu$ minus the face $x_\mu=a_\mu$ , as in the definitions file), both

-\mathcal B\le\mathrm{Ym}_{[a,b]}(A)\qquad\text{and}\qquad\mathcal B\le\mathrm{Ym}_{[a,b]}(A)

hold, where $\mathrm{Ym}_{[a,b]}(A)=\int_{[a,b]}|F_A(x)|^2\,dx$ is a real number. Equivalently $|\mathcal B|\le\mathrm{Ym}_{[a,b]}(A)$ . Only the real part of the complex boundary term appears; nothing is asserted about its imaginary part. Degenerate boxes are allowed.

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 (energy bound) — Ym(DA)≥∓∫∂MCS(A)\mathrm{Ym}(D_A)\ge\mp\int_{\partial M}CS(A)Ym(DA​)≥∓∫∂M​CS(A) on a box

Proposition 3.1.1 (energy bound) — $\mathrm{Ym}(D_A)\ge\mp\int_{\partial M}CS(A)$ on a box