w8_dft_candidate
plain-language theorem explainer
Defines a real scalar equal to the sum, over the seven nonzero modes of the eight-tick circle, of each mode's φ-pattern DFT power times a geometric weight (sin² frequency times φ-decay). Gap-weight and α-pipeline authors cite it as the raw DFT candidate before projection/normalization. The body is a direct Finset sum of two already-defined nonnegative summands.
Claim. Let $w_8^{\mathrm{DFT}}$ be the real number $\sum_{k \in \{1,\ldots,7\}} A_\phi(k)\, G(k)$, where $A_\phi(k)$ is the squared complex DFT amplitude of the canonical $\varphi$-pattern at mode $k\in\mathbb{F}_8$, and $G(k)$ is the geometric weight $\sin^2(k\pi/8)\,\varphi^{-k}$ (with $G(0)=0$).
background
The module fixes the canonical φ-pattern on the eight-tick (period $2^3$) discrete circle and studies its discrete Fourier transform. Recognition Science forces that eight-tick octave at T7 of the unified forcing chain; gap weights built from it feed the fine-structure constant band.
phiDFTAmplitude k is the squared modulus of the DFT coefficient of that φ-pattern at bin $k\in\mathrm{Fin},8$. geometricWeight k multiplies a squared sine of the mode frequency $k\pi/8$ by a pure φ-power decay $\varphi^{-k}$, and vanishes at the zero mode. Both factors are nonnegative by sibling lemmas in the same file.
The certified constant used by the α pipeline is Constants.w8_from_eight_tick. The present sum is only a DFT-side candidate; equality with that certified value is not claimed here.
proof idea
Pure definition, not a proved equality. Expand as the Finset sum of phiDFTAmplitude k * geometricWeight k over Finset.univ filtered to drop the zero mode. No tactics or lemmas are applied at the definition site; positivity and projection identities are proved downstream by unfolding this sum and using nonnegativity of each factor.
why it matters
Supplies the raw numerator for the projection weight w8_projected := projectionScale * (w8_dft_candidate / phiDFTEnergyTotal), which makes normalization and measure choice explicit on the eight-tick basis. Downstream positivity (w8_dft_candidate_pos) and nonnegativity of the projected weight both unfold this sum. GapWeight documentation records a closed projection-equality path that reduces per-mode geometric weights via explicit sine identities; this candidate is the scaffold object those equalities compare against. In the broader RS picture it sits on the T7 eight-tick octave and the constants/α pipeline, but the doc-comment stresses it is not yet identified with the certified w8_from_eight_tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.