diffEnergy8_mode_eq_four_sin_sq
plain-language theorem explainer
The discrete difference energy of each DFT-8 eigenmode equals four times the squared half-angle sine: E_diff(mode k) = 4 sin²(kπ/8). Anyone tracing the gap-weight oscillation factor to the eight-tick difference operator cites this spectrum identity. The proof is a two-step rewrite: mode energy reduces to |ω₈ᵏ − 1|², then the trig closure evaluates that modulus.
Claim. For every mode index $k \in \{0,\ldots,7\}$, the discrete difference energy of the corresponding DFT-8 eigenmode equals $4\sin^2(k\pi/8)$.
background
In the Alpha Genesis M6 setting, the gap-weight mode weights carry an oscillation factor $\sin^2(k\pi/8)$. The module's claim is that this factor is not a modeling choice: it is one quarter of the spectrum of the one-step difference operator on the eight-tick cycle, read on the DFT-8 eigenbasis.
The difference energy $\mathrm{diffEnergy8}(v)$ is the total squared modulus of the discrete one-step difference of a length-8 complex vector. Upstream, the lemma on mode energies shows that on a DFT mode this collapses to $|\omega_8^k-1|^2$, because cyclic shift acts by the eigenvalue $\omega_8^k$. The companion trig closure then states $|\omega_8^k-1|^2=4\sin^2(k\pi/8)$.
Together those two facts turn the abstract difference spectrum into the explicit sine factor that appears inside the geometric mode weight.
proof idea
Two-step rewrite. First apply the mode-energy lemma, which replaces the difference energy of DFT mode $k$ by $\mathrm{Complex.normSq}(\omega_8^{k}-1)$. Then discharge the goal by the trig-closure theorem, which evaluates that squared modulus as $4\sin^2(k\pi/8)$. No further case splits or arithmetic are needed.
why it matters
This is link 3 in the M6 spectral-forcing chain: after DFT modes diagonalize the cyclic shift and mode energy equals $|\omega_8^k-1|^2$, the trig identity supplies the concrete $\sin^2$ spectrum. Downstream, the factorization theorem rewrites the geometric mode weight as $(\mathrm{diffEnergy8}(\mathrm{mode},k)/4)$ times the T9 forced lattice measure, citing this identity to replace the sine factor by difference energy over four. The spectral-forcing certificate bundles the same identity as one of its three conjuncts.
In framework terms it closes the oscillation joint of the gap weight on the eight-tick octave (T7): pattern, envelope, and dressing are forced elsewhere; here the $\sin^2$ factor is forced as derivative spectrum rather than inserted by hand. The only remaining inherited $w_8$ ingredient named in the module is Parseval/64-cell normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.