phiDFTEnergyTotal_nonneg
plain-language theorem explainer
The total DFT energy of the φ-pattern on the eight-tick basis is nonnegative. Anyone normalizing a projected gap weight by this Parseval denominator cites it to justify a well-defined nonnegative ratio. The proof is a one-line sum-nonneg argument from pointwise nonnegativity of the eight mode amplitudes.
Claim. The total DFT energy of the $\varphi$-pattern, defined as $\sum_{k=0}^{7} |\widehat{\varphi}(k)|^2$ over the eight-tick modes, satisfies $0 \le E_{\mathrm{DFT}}(\varphi)$.
background
GapWeight.Projection makes two historically implicit choices explicit: the $\sin^2(\pi k/8)$ spectral weight from the discrete Laplacian 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.
phiDFTEnergyTotal is the Parseval denominator for that projection: the sum of phiDFTAmplitude over Fin 8. Each amplitude is a complex norm-squared of a DFT coefficient of the $\varphi$-pattern, hence nonnegative by phiDFTAmplitude_nonneg. The eight-tick octave is the T7 landmark (period $2^3$); the spatial eight-vertex cell matches the discrete geometry used for per-cell integrated weights via projectionScale = N_cell.
proof idea
Unfold the definition of the total energy to a finite sum over Fin 8. Apply Finset.sum_nonneg, then for each mode index invoke phiDFTAmplitude_nonneg, which itself is Complex.normSq_nonneg. No further algebraic work: nonnegativity of the sum is inherited pointwise from the mode energies.
why it matters
Feeds w8_projected_nonneg, which shows the explicit projection weight
projectionScale * (rawWeightedNeutralEnergy / totalEnergy)
is nonnegative. That parent needs a nonnegative denominator (and a zero-energy edge case) so the ratio is a well-defined per-cell weight rather than an unsigned formal quotient.
In the Recognition framework this closes the “weights + normalization” ambiguity for the gap-weight constant on the eight-tick octave. It does not invent new physics; it certifies that the DFT energy used as Parseval measure cannot go negative, so downstream gap-weight inequalities and positivity claims remain on solid ground. Landmark contact is T7 (eight-tick period) and the discrete cell measure $8\times 8$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.