phiDFTEnergyTotal
plain-language theorem explainer
Defines the total DFT energy of the φ-pattern as the sum of squared mode amplitudes over the eight-tick basis. It is the Parseval denominator used when normalizing geometric gap weights. Anyone citing the projected eight-tick weight or its nonnegativity will pull this constant. The body is a direct Finset sum of the per-mode squared amplitudes.
Claim. The total DFT energy of the $\varphi$-pattern is $E_{\mathrm{tot}} := \sum_{k \in \mathbb{F}_8} |\hat{\varphi}(k)|^2$, i.e. the sum of squared DFT amplitudes over the eight cyclic modes. This quantity is the Parseval denominator for subsequent weight normalizations.
background
The GapWeight.Projection module makes two historically implicit choices explicit: the $\sin^2(\pi k/8)$ spectral weight from the discrete derivative on the 8-tick cyclic shift, and the normalization factor $64 = 8 \times 8$ from the fundamental RS interface cell (eight ticks times eight $Q_3$ vertices). The goal is claim hygiene: no hidden operator or measure freedom.
Upstream, each mode amplitude is the squared complex norm of the DFT coefficient of the $\varphi$-pattern on $\mathrm{Fin},8$. Summing those amplitudes yields the total energy that appears in Parseval-style normalizations. The eight-tick octave is the T7 landmark of the forcing chain; the DFT here is the shift-diagonalization of that cyclic clock.
proof idea
Pure definition, not a proved statement. The value is the universe sum over $k : \mathrm{Fin},8$ of the per-mode squared amplitude. No tactics or lemmas are applied; the body is the Finset sum of those amplitudes.
why it matters
This constant is the denominator in the projected eight-tick weight: that weight is the projection scale times (raw weighted neutral energy divided by this total energy). Nonnegativity of the total energy is proved immediately downstream by summing the nonnegative mode amplitudes, and that fact feeds the nonnegativity proof of the projected weight.
In the Recognition framework it closes the normalization half of the weights-plus-normalization ambiguity for gap weights on the eight-tick octave. Without an explicit Parseval denominator, the conversion from a scale-invariant fraction to a per-cell integrated weight would retain a free scale. It sits in the Constants domain and supports the geometric weight story tied to T7 (eight-tick period).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.