diffEnergy8_nonneg
plain-language theorem explainer
The discrete-difference energy of any complex 8-tick signal is nonnegative. Anyone building gap weights, DFT-8 spectral projections, or per-cell normalizations on the octave clock cites this positivity. The proof unfolds the sum definition and applies nonnegativity of complex squared norms termwise.
Claim. For every complex-valued signal $v$ on the eight-tick cycle $\mathrm{Fin}\,8$, the total squared energy of its discrete difference is nonnegative: $0 \le \sum_{t} |(\Delta v)_t|^2$.
background
The module GapWeight.Projection makes two historically implicit choices explicit: the geometric factor $\sin^2(\pi k/8)$ as the spectral weight of the discrete derivative (Laplacian) on the 8-tick cyclic shift, and the normalization $64 = 8\times 8$ as the cardinality of the fundamental RS interface cell (8 ticks times 8 vertices of the $Q_3$ cell). That converts a scale-invariant fraction into a per-cell integrated weight.
The object whose positivity is claimed is the total squared energy of the discrete difference: sum over the eight ticks of the squared complex modulus of the local difference operator applied to $v$. It is the canonical local, shift-invariant quadratic form on the octave clock (T7: period $2^3$). Upstream, squared-modulus nonnegativity for complex values (and the parallel finite-amplitude norm-square lemma) supply the termwise lower bound used here.
proof idea
One short term proof. Unfold the definition of the difference energy to a finite sum over $\mathrm{Fin},8$ of $\mathrm{Complex.normSq}$ of the discrete difference at each tick. Apply Finset.sum_nonneg with the standard fact that squared complex modulus is nonnegative at every summand. No spectral or DFT identity is needed; positivity is purely algebraic.
why it matters
Gap-weight constructions need a nonnegative quadratic form before they can be treated as energies, projected DFT weights, or normalized per-cell contributions. This lemma is the elementary positivity gate for that form on the eight-tick interface. It sits under the module's claim-hygiene program: operator and measure choices are explicit, so the $\sin^2(\pi k/8)$ spectral weights and the $64$-normalization have no hidden sign or scale freedom.
Framework landmarks: T7 eight-tick octave and the $Q_3$ eight-vertex cell that force the $8\times 8$ cell measure. Downstream use edges are not yet recorded for this lemma; sibling results (phiDFTEnergyTotal_nonneg, w8_projected_nonneg) play the same positivity role for total DFT energy and projected weights. No open scaffold is left here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.