NF Discreteness Lemma

The normal-form tower ℤ/Prim(k)ℤ is inherently discrete. No continuum limit within τ: each primorial level has finitely many states. Discreteness earned from K3 divisibility, not imposed.

NF Discreteness Lemma

Summary

The normal-form tower ℤ/Prim(k)ℤ is inherently discrete. No continuum limit within τ: each primorial level has finitely many states. Discreteness earned from K3 divisibility, not imposed.

Statement

\label{prop:nf-discreteness-lemma}
Let $k \in \mathbb{N}$ and let $\operatorname{Strong}_{E_1}^{(k)}$ denote the strong sector restricted to primorial depth~$k$. The number of distinct NF configurations in $\operatorname{Strong}_{E_1}^{(k)}$ is bounded by
\begin{equation}
\bigl|\operatorname{NF}\bigl(\operatorname{Strong}_{E_1}^{(k)}\bigr)\bigr|
\;\le\;
\operatorname{Prim}(k).
\label{eq:ch38-nf-discreteness-bound}
\end{equation}
Moreover, the bound is sharp: for each $k$, there exist exactly $\operatorname{Prim}(k)$ distinct C-sector normal forms at depth~$k$.

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 103
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part05/ch38-the-strong-sector-and-nf-discreteness.tex lines 81-92

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Physics.StrongSector
• Name: nf_discreteness_check

Dependencies

• Canonical: III.D23, III.T09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.