diffEnergy8_mode
plain-language theorem explainer
On the eight-tick cycle, the discrete difference energy of the k-th DFT mode equals the squared modulus of ω^k − 1, with ω a primitive eighth root of unity. Anyone deriving the sin²(πk/8) gap-weight factor from the Laplacian spectrum cites this identity. The proof is a short eigenvector calculation: the cyclic shift multiplies the mode by ω^k, the difference factors, and unit-norm DFT columns leave only |ω^k − 1|².
Claim. For each mode index $k \in \{0,\ldots,7\}$, the total squared energy of the one-step discrete difference of the $k$-th length-8 DFT mode equals $|\omega^k - 1|^2$, where $\omega = e^{2\pi i/8}$ is a primitive eighth root of unity.
background
The module makes two historically implicit choices explicit: the spectral origin of the $\sin^2(\pi k/8)$ geometric weight, and the normalization factor $64 = 8\times 8$ from the eight-tick octave times the eight vertices of the $Q_3$ cell. Both sit inside the Recognition eight-tick (T7) interface.
The discrete difference operator on the cycle is $(S-I)v$, pointwise $v_{t+1}-v_t$. Its total squared energy is the sum of complex squared moduli of those increments: a local, shift-invariant quadratic form. The length-8 DFT modes are the eigenvectors of the cyclic shift $S$, with eigenvalues $\omega^k$ for $\omega=e^{2\pi i/8}$.
Upstream, the DFT-8 columns are orthonormal, so each mode has unit $\ell^2$ norm: the sum of squared moduli over the eight ticks equals 1. That unit-norm fact is what lets the energy collapse to a pure eigenvalue expression.
proof idea
Unfold the energy and the difference. Invoke the shift-eigenvector law: $S$ applied to mode $k$ equals $\omega^k$ times the mode. Pointwise, the increment is therefore $(\omega^k-1)$ times the mode value. Squared modulus multiplies, so each term is $|\omega^k-1|^2$ times the mode's local squared modulus. Factor the constant out of the finite sum (via Finset.mul_sum), then apply unit-norm of the DFT mode to replace the remaining sum by 1. A final ring cleanup yields equality.
why it matters
This lemma is the operator-theoretic reason the gap weight carries a $\sin^2(\pi k/8)$ factor. Downstream, diffEnergy8_mode_eq_four_sin_sq rewrites $|\omega^k-1|^2$ as $4\sin^2(k\pi/8)$, so the oscillation factor in the gap weight is exactly one quarter of the difference-operator spectrum. That identity is the spectral forcing step in AlphaGenesis.
In the broader framework it closes claim hygiene on the eight-tick octave (T7): the weight is forced by shift-diagonalization of the discrete Laplacian, not chosen by hand. No free spectral parameter remains once the cyclic difference energy is fixed as the quadratic form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.