phiDFTCoeff
plain-language theorem explainer
Defines the eight DFT coefficients of the canonical φ-pattern on the 8-tick register: each mode k is the inner product of the complexified pattern against the conjugate DFT-8 column. Gap-weight and geometric-weight constructions cite it as the spectral input. The body is the standard unitary DFT sum, not a derived identity.
Claim. For each frequency index $k \in \{0,\ldots,7\}$, the DFT coefficient of the canonical $\varphi$-pattern is $c_k = \sum_{t=0}^{7} \overline{U_{t k}}\, p_t$, where $U_{t k} = \omega^{t k}/\sqrt{8}$ is the unitary DFT-8 matrix entry and $p_t$ is the complexification of the real $\varphi$-pattern at tick $t$.
background
The module fixes the canonical φ-pattern on the eight-tick register (the discrete octave forced at T7 of the forcing chain). That real-valued length-8 sequence is lifted to complexes by phiPatternComplex so standard spectral tools apply.
The DFT-8 matrix is the unitary Fourier transform on $\mathbb{C}^8$: entry $(t,k)$ is $\omega^{tk}/\sqrt{8}$ with $\omega = e^{2\pi i/8}$. The coefficient defined here is exactly the $k$-th Fourier mode of the pattern under that unitary basis (conjugate on the matrix entry, sum over ticks).
Downstream objects read these coefficients as spectral amplitudes that seed geometric gap weights on the φ-ladder.
proof idea
Pure definition: expand the length-8 sum $\sum_t \overline{\mathrm{dft8_entry}(t,k)}\cdot p_t^{\mathbb{C}}$. No lemmas are applied; noncomputable only because the complex field and square-root normalization are noncomputable in Lean.
why it matters
Supplies the spectral coordinates of the canonical φ-pattern that the gap-weight formula needs. Immediately used by the squared-amplitude map (norm-squared of each coefficient) and by the positivity proof for the DFT-based candidate weight $w_8$, which sums positive contributions over nonzero modes. Ties the eight-tick octave (T7) to concrete geometric weights on the φ-ladder rather than leaving the pattern as a bare time-domain sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.