Lemma 3.1.2 — $|F\pm\star F|^2=2|F|^2\mp2\operatorname{tr}(F\wedge F)$

Proved

UhlenbeckGauge.norm_add_hodgeStar_sq

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

differential-geometrygauge-theorymathematical-physicsyang-mills

Let $F=(F_{\mu\nu})$ be an antisymmetric $\mathfrak{su}(n)$ -valued two-form on $\mathbb R^4$ (at a point), $\star$ the Euclidean Hodge star, $|\cdot|^2$ the pointwise norm and $\operatorname{tr}(F\wedge F)$ the Chern–Weil density. Then

|F+\star F|^2=2|F|^2-2\operatorname{tr}(F\wedge F),\qquad |F-\star F|^2=2|F|^2+2\operatorname{tr}(F\wedge F).

In particular $\operatorname{tr}(F\wedge F)$ is real. This is the pointwise identity behind the decomposition of the Yang–Mills energy into an (anti-)self-duality defect and a topological term.

Formalization Note The printed statement in the notes has $\pm2\operatorname{tr}(F_A\wedge F_A)$ ; its proof on p. 32 arrives at $\mp2\operatorname{tr}(F_A\wedge F_A)$ using $B^*=-B$ on $\mathfrak{su}(n)$ . The formalization follows the proof. The identity is stated in $\mathbb C$ .

Preamble

import Definitions.Def_uhlenbeck_gauge_box_defs

open UhlenbeckGauge

Formal statement

namespace UhlenbeckGauge

theorem norm_add_hodgeStar_sq {n : ℕ} (F : TwoForm n) (hF : IsAntisymm F)
    (hsu : IsSuNValued F) :
    ((normSq (F + hodgeStar F) : ℝ) : ℂ) = 2 * (normSq F : ℂ) - 2 * trWedge F ∧
    ((normSq (F - hodgeStar F) : ℝ) : ℂ) = 2 * (normSq F : ℂ) + 2 * trWedge F := 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, Lemma 3.1.2 and its proof (p. 31-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$ (including $0$ ) and every family $F=(F_{\mu\nu})_{\mu,\nu\in\{0,1,2,3\}}$ of complex $n\times n$ matrices satisfying

antisymmetry: $F_{\nu\mu}=-F_{\mu\nu}$ for all $\mu,\nu$ , and
every $F_{\mu\nu}$ is skew-Hermitian ( $F_{\mu\nu}^*=-F_{\mu\nu}$ ) and traceless,

the following two equalities of complex numbers hold:

|F+\star F|^2=2|F|^2-2\,\operatorname{tr}(F\wedge F),\qquad |F-\star F|^2=2|F|^2+2\,\operatorname{tr}(F\wedge F).

Here $F\pm\star F$ is the entrywise sum/difference of families, $(\star F)_{\mu\nu}=\tfrac12\sum_{\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}F_{\rho\sigma}$ with $\varepsilon$ the Levi-Civita symbol ( $\varepsilon_{0123}=1$ ), $|G|^2=\sum_{\mu<\nu}\operatorname{Re}\operatorname{tr}(G_{\mu\nu}G_{\mu\nu}^*)$ is a real number (viewed in $\mathbb C$ on the left-hand side), and $\operatorname{tr}(F\wedge F)=\tfrac14\sum_{\mu,\nu,\rho,\sigma}\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(F_{\mu\nu}F_{\rho\sigma})\in\mathbb C$ . Because the equalities are in $\mathbb C$ and the norms are real, the statement implies that $\operatorname{tr}(F\wedge F)$ has zero imaginary part. For $n=0$ all quantities are $0$ . No derivative, connection or integral is involved: this is a statement about a single matrix family.

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

Lemma 3.1.2 — ∣F±⋆F∣2=2∣F∣2∓2tr⁡(F∧F)|F\pm\star F|^2=2|F|^2\mp2\operatorname{tr}(F\wedge F)∣F±⋆F∣2=2∣F∣2∓2tr(F∧F)

Lemma 3.1.2 — $|F\pm\star F|^2=2|F|^2\mp2\operatorname{tr}(F\wedge F)$