phiDFTAmplitude
plain-language theorem explainer
Defines the squared modulus of the k-th DFT coefficient of the canonical eight-tick φ-pattern, as a real number on Fin 8. Gap-weight and α-pipeline authors cite it as the mode energy entering DFT-based weight candidates and the Parseval total. The body is a one-line wrapper: Complex.normSq of the already-defined coefficient.
Claim. For each mode index $k \in \{0,\ldots,7\}$, the φ-pattern DFT amplitude is $|c_k|^2 \in \mathbb{R}$, where $c_k$ is the discrete Fourier coefficient of the canonical complex φ-pattern on the eight-tick register.
background
The module fixes the canonical φ-pattern on the eight-tick (period $2^3$) register and studies its discrete Fourier transform. The coefficient $c_k$ is the inner sum of the conjugated DFT8 kernel against the complexified φ-pattern at tick $t$. Squared modulus is the standard Born/energy weight of that complex mode.
Upstream, phiDFTCoeff builds $c_k$ as $\sum_t \overline{\mathrm{dft8}(t,k)},\phi_{\mathbb{C}}(t)$. Related finite-amplitude and Hilbert-display normSq definitions in the primitive recognition calculus play the same role for general amplitude vectors; here the ambient space is simply $\mathbb{C}$ per mode. The eight-tick octave is the T7 landmark of the forcing chain.
proof idea
Pure definition, not a proof. The value at mode $k$ is exactly Complex.normSq applied to the DFT coefficient of the φ-pattern at that mode. No tactics, no lemmas beyond the Mathlib squared-norm on $\mathbb{C}$.
why it matters
Supplies the per-mode energy that feeds the DFT-based gap-weight scaffold. Downstream, non-negativity is immediate from Complex.normSq_nonneg; the candidate weight $w_8$ sums amplitude times geometric weight over nonzero modes; positivity of that candidate uses a strictly positive summand; and phiDFTEnergyTotal sums amplitudes over all eight modes as the Parseval denominator in the projection module.
In the Recognition framework this sits in the Constants/GapWeight layer that aims to connect the eight-tick φ-pattern to the certified $w_8$ used by the α pipeline. The candidate is explicitly not yet identified with Constants.w8_from_eight_tick, so this definition is infrastructure for that comparison rather than a closed derivation of α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.