Fact 3.1.3 — $\int_M\operatorname{tr}(F_A\wedge F_A)=\int_{\partial M}CS(A)$ on a box

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):

Here $[a,b]$ is the closed coordinate box in $\mathbb R^4$ with Lebesgue measure, $a_{\hat\mu},b_{\hat\mu}\in\mathbb R^3$ are $a,b$ with coordinate $\mu$ removed, $\iota_\mu(t,y)\in\mathbb R^4$ is the point obtained by inserting $t$ as coordinate $\mu$ into $y\in\mathbb R^3$, the integrals over $\mathbb R^3$ use Lebesgue measure, $F_A$, $\operatorname{tr}(\cdot\wedge\cdot)$ and $K^\mu(A)$ are as defined in the definitions file ($K^\mu=\sum\varepsilon_{\mu\nu\rho\sigma}\operatorname{tr}(A_\nu\partial_\rho A_\sigma+\tfrac23A_\nu A_\rho A_\sigma)$), and all integrals are complex-valued Bochner integrals. Degenerate boxes ($a_\mu=b_\mu$ for some $\mu$) are allowed.