Strong Defect Functional

The defect functional Δ restricted to the strong (C) sector. Measures deviation from the C-sector’s canonical form. Non-trivial gauge configurations have Δ_C > 0.

Strong Defect Functional

Summary

The defect functional Δ restricted to the strong (C) sector. Measures deviation from the C-sector’s canonical form. Non-trivial gauge configurations have Δ_C > 0.

Statement

\label{def:strong-defect-functional}
Let $\mathfrak{g}_k = (U_k, \phi_k^C, \mathfrak{c}_k)$ be $\tau$-admissible gauge data at primorial depth~$k$ (Definition~\ref{def:tau-admissible-gauge-data}, Ch.~38). The \emph{strong defect functional} is
\begin{equation}
\Delta_C(\mathfrak{g}_k, n) \;=\;
\bigl\| \phi_k^C\big|_{\operatorname{Prim}(n)} - (\phi_k^C)^{\mathrm{can}}\big|_{\operatorname{Prim}(n)} \bigr\|^2,
\label{eq:ch40-strong-defect}
\end{equation}
where $(\phi_k^C)^{\mathrm{can}}$ is the NF-stabilized form of $\phi_k^C$ in the C-sector at primorial depth~$n$, and $\|\cdot\|$ is the $L^2$-norm on $\mathbb{Z}/\operatorname{Prim}(n)\mathbb{Z}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 108
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part05/ch40-the-yang-mills-mass-gap.tex lines 41-51

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Physics.GapTheorem
• Name: ym_coupling_check

Dependencies

• Canonical: III.D39, III.D43

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.