Defect Functional Δ

Δ(f, n) measures the deviation of an ω-germ f from canonical form at primorial depth n. Δ ≥ 0; Δ = 0 iff stabilized. The defect is computable at each finite level.

Defect Functional Δ

Summary

Δ(f, n) measures the deviation of an ω-germ f from canonical form at primorial depth n. Δ ≥ 0; Δ = 0 iff stabilized. The defect is computable at each finite level.

Statement

\label{def:defect-functional}
Let $f$ be $\tau$-admissible fluid data and let $n \in \mathbb{N}$ be a primorial depth. The \emph{defect functional} is the non-negative quantity
\begin{equation}
\Delta(f, n) \;=\; \sum_{S \in \{A,B,C,D,\omega\}}
\bigl\| f_S\big|_{\operatorname{Prim}(n)} - f_S^{\mathrm{can}}\big|_{\operatorname{Prim}(n)} \bigr\|^2,
\label{eq:ch35-defect-functional}
\end{equation}
where $f_S^{\mathrm{can}}$ is the canonical (NF-stabilized) form of $f_S$ at primorial depth $n$, the restriction $\cdot\big|_{\operatorname{Prim}(n)}$ denotes evaluation on the lattice $\mathbb{Z}/\operatorname{Prim}(n)\mathbb{Z}$, and $\|\cdot\|$ is the $L^2$-norm on this finite lattice.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 92
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part05/ch35-fluid-sectors-and-the-defect-functional.tex lines 77-87

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Physics.FluidData
• Name: defect_monotone_check

Dependencies

• Canonical: III.D36, III.D38

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.