Fact 3.1.3 (local form) — $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$

Proved

UhlenbeckGauge.trWedge_curvature_eq_div_chernSimons

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

differential-geometrygauge-theorymathematical-physicsyang-mills

Let $A$ be a smooth $SU(n)$ -connection on the trivial bundle over $\mathbb R^4$ , with curvature $F_A$ , and let $K^\mu(A)=\sum_{\nu,\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(A_\nu\partial_\rho A_\sigma+\tfrac23A_\nu A_\rho A_\sigma)$ be the components of the Chern–Simons three-form $CS(A)=\operatorname{tr}(A\wedge dA+\tfrac23A\wedge A\wedge A)$ . Then at every point $x\in\mathbb R^4$

\operatorname{tr}(F_A\wedge F_A)(x)=\sum_{\mu=0}^{3}\partial_\mu K^\mu(A)(x),

that is, $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$ . This is the local identity that makes $\operatorname{tr}(F_A\wedge F_A)$ a "topological term" which integrates to a boundary contribution.

Formalization Note The Chern–Simons form uses the standard coefficient $\tfrac23$ (equivalently $\operatorname{tr}(A\wedge F_A)-\tfrac13\operatorname{tr}(A\wedge A\wedge A)$ ); the $\tfrac16$ printed on p. 32 of the notes does not satisfy $d\,CS=\operatorname{tr}(F\wedge F)$ with $F_A=dA+A\wedge A$ .

Preamble

import Definitions.Def_uhlenbeck_gauge_box_defs

open UhlenbeckGauge

Formal statement

namespace UhlenbeckGauge

theorem trWedge_curvature_eq_div_chernSimons {n : ℕ} (A : Connection n)
    (hA : IsSUConnection A) (x : R4) :
    trWedge (curvature A x) =
      ∑ μ : Fin 4, fderiv ℝ (chernSimonsCurrent A μ) x (Pi.single μ 1) := 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, discussion of Fact 3.1.3 and the Chern-Simons three-form (p. 32)

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$ , every map $A:\mathbb R^4\to(\{0,1,2,3\}\to\mathrm{Mat}_n(\mathbb C))$ that is an $SU(n)$ -connection — every entry $x\mapsto A_\mu(x)_{ij}$ is $C^\infty$ on $\mathbb R^4$ , and every $A_\mu(x)$ is skew-Hermitian with trace $0$ — and every point $x\in\mathbb R^4$ :

\operatorname{tr}(F_A(x)\wedge F_A(x))=\sum_{\mu=0}^{3}\frac{\partial}{\partial x_\mu}K^\mu(A)(x).

Here $F_A(x)_{\mu\nu}=\partial_\mu A_\nu(x)-\partial_\nu A_\mu(x)+A_\mu(x)A_\nu(x)-A_\nu(x)A_\mu(x)$ (entrywise partial derivatives), $\operatorname{tr}(G\wedge G)=\tfrac14\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(G_{\mu\nu}G_{\rho\sigma})$ , and $K^\mu(A)(y)=\sum_{\nu,\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}\big(A_\nu(y)\,\partial_\rho A_\sigma(y)+\tfrac23A_\nu(y)A_\rho(y)A_\sigma(y)\big)$ , a complex-valued function on $\mathbb R^4$ ; the right-hand side is the Fréchet derivative of $K^\mu(A)$ at $x$ (as a map of real vector spaces) applied to the $\mu$ -th standard basis vector, summed over $\mu$ . Both sides are complex numbers. The $\mathfrak{su}(n)$ hypothesis is present even though the stated identity does not obviously require it.

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

Fact 3.1.3 (local form) — tr⁡(FA∧FA)=d CS(A)\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)tr(FA​∧FA​)=dCS(A)

Fact 3.1.3 (local form) — $\operatorname{tr}(F_A\wedge F_A)=d\,CS(A)$