dft8_mode_normSq_sum
plain-language theorem explainer
Each length-8 DFT mode has unit Euclidean norm: the sum of squared complex magnitudes over the eight tick indices equals 1. Anyone deriving discrete-difference energies or projected gap weights on the eight-tick clock cites this. The proof is a short cast-and-rewrite from column orthonormality of the DFT-8 matrix.
Claim. For every mode index $k \in \{0,\ldots,7\}$, if $v^{(k)}$ denotes the corresponding length-8 DFT mode (the $k$-th column of the unitary DFT-8 matrix), then $\sum_{t=0}^{7} |v^{(k)}_t|^2 = 1$.
background
The module GapWeight.Projection makes two historically implicit choices explicit: the $\sin^2(\pi k/8)$ spectral weight of the eight-tick discrete derivative, and the normalization factor $64 = 8 \times 8$ coming from eight ticks times eight vertices of the $Q_3$ cell. Both sit on the DFT-8 basis of the cyclic shift on the octave clock (T7: period $2^3$).
A DFT-8 mode is the $k$-th column of the standard length-8 discrete Fourier matrix; its entries are the normalized powers of the primitive eighth root of unity. Column orthonormality of that matrix is the structural fact used here. Upstream, the shift eigenvalue at mode $k$ is $\zeta^k$, so modes are simultaneous eigenvectors of the cyclic shift; unit norm is the remaining piece needed before difference energies can be read off as $|\omega^k - 1|^2$.
proof idea
Start from column orthonormality: the inner product of column $k$ with itself is $1$, written as $\sum_t \overline{U_{tk}} U_{tk} = 1$ in $\mathbb{C}$. Rewrite each summand via $\overline{z},z = |z|^2$ (as a real cast into $\mathbb{C}$). Pull the real-to-complex cast out of the finite sum, then apply injectivity of $\mathbb{R}\to\mathbb{C}$ to obtain the real identity $\sum_t |U_{tk}|^2 = 1$. Finish by unfolding the definition of the mode vector so the sum is over dft8_mode k t.
why it matters
Unit-norm modes are the missing normalization step before discrete difference energy can be identified with $|\omega^k-1|^2$. The sole downstream consumer is diffEnergy8_mode, whose doc-comment states that this is "the precise mathematical reason a $\sin^2(\pi k/8)$ factor appears: it is (up to a fixed factor 4) the spectrum of the 8-tick discrete derivative/Laplacian." That factor feeds the projected gap weight $w_8$ and the claim-hygiene goal of the module: no hidden operator or measure freedom in the geometric weights. Framework-wise it sits on the eight-tick octave (T7) and the DFT/Cl$_8$ bridge, converting abstract orthonormality into the concrete $L^2$ normalization used by per-cell integrated weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.