SpectralForcingCert
plain-language theorem explainer
Certificate bundling the three M6 spectral-forcing identities: the trig closure |ω₈ᵏ−1|² = 4 sin²(kπ/8), the matching difference-energy spectrum on every DFT-8 mode, and the factorization of each nonzero mode weight into (spectrum/4) times the forced lattice measure. Cited by anyone closing the gap-weight oscillation factor. Verification is a one-line conjunction of three prior theorems.
Claim. A certificate whose verification asserts: (i) for all $k\in\mathbb{N}$, $|\omega_8^k-1|^2=4\sin^2(k\pi/8)$; (ii) for every DFT-8 mode $k$, the difference energy of that mode equals $4\sin^2(k\pi/8)$; (iii) for every nonzero mode $k$, the geometric weight equals $(\mathrm{diffEnergy}(\mathrm{mode}\,k)/4)$ times the T9 lattice measure. Every such certificate is verified.
background
Alpha Genesis M6 treats the $\sin^2(k\pi/8)$ factor inside the gap-weight mode weights as forced, not chosen. On the eight-tick cycle the primitive root $\omega_8$ is the shift eigenvalue; DFT-8 modes diagonalize the cyclic shift. The difference energy $\mathrm{diffEnergy}_8(v)$ is the total squared modulus of the one-step discrete difference of a length-8 complex vector, a canonical local shift-invariant quadratic form.
Upstream, the trig closure states $|\omega_8^k-1|^2=4\sin^2(k\pi/8)$. The spectrum identity then rewrites the difference energy of mode $k$ as that same quantity. Separately, geometric weight is the mode weight built from $\sin^2$ times a $\phi$-decay envelope (zero on the DC mode). Lattice weight is the T9-forced measure on the cycle.
The module chain is: DFT eigenbasis $\to$ difference energy equals $|\omega_8^k-1|^2$ $\to$ trig closure $\to$ factorization into spectrum times measure. Together with M2 (pattern) and M5 (calibration), this is the last interior joint of the gap weight.
proof idea
The structure is an empty inhabited certificate. Its verified predicate is the conjunction of the three universal statements above. The companion theorem that every certificate is verified is a one-line refine assembling three already-proved lemmas: normSq_omega8_pow_sub_one (trig closure for all natural powers), diffEnergy8_mode_eq_four_sin_sq (spectrum identity on Fin 8, itself a rewrite of the mode energy lemma plus the trig closure), and geometricWeight_eq_spectrum_mul_measure (factorization for nonzero modes, rewriting the sin-form weight via the spectrum identity).
why it matters
Closes M6 of Alpha Genesis: the oscillation factor in the gap weight is one quarter of the difference-operator spectrum on the eight-tick cycle, evaluated on the DFT eigenbasis. Both spectrum and measure factors are theorem-backed; neither is an input. This sits on the T7 eight-tick octave and the T9 measure-forcing line, and finishes the interior forcing of pattern, envelope, oscillation, and dressing form for the mode weights.
The only remaining $w_8$ ingredient left as a named premise is the Parseval / 64-cell normalization. No CODATA enters the file. Downstream use is presently empty in the graph; the certificate is the package point for the three spectral identities rather than a stepping stone into a further named theorem yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.