diffEnergy8
plain-language theorem explainer
Defines the total squared energy of the one-step cyclic difference of an 8-tick complex signal: sum of | (Sv − v)(t) |² over the octave. Anyone deriving the gap-weight sin² spectrum or the spectral-forcing factorization cites this quadratic form. The body is a direct sum of complex squared norms of the discrete difference.
Claim. For $v : \mathbb{F}_8 \to \mathbb{C}$, the difference energy is $\sum_{t \in \mathbb{F}_8} |(\mathrm{S}v - v)(t)|^2$, where $\mathrm{S}$ is the one-step cyclic shift on the eight-tick cycle.
background
The GapWeight.Projection module makes two historically implicit choices explicit: the $\sin^2(\pi k/8)$ factor in geometric weights, and the normalization by $64 = 8 \times 8$ (eight ticks times eight $Q_3$ vertices). Both arise from operator and measure choices on the fundamental RS interface cell, not free parameters.
The discrete difference diff8 is the local operator $(S - I)v$ on the 8-tick cycle: at each tick, the value after one cyclic shift minus the present value. Squared modulus is the standard complex energy density. Summing it yields a shift-invariant, local quadratic form on signals $v : \mathrm{Fin},8 \to \mathbb{C}$.
This sits in the eight-tick octave forced by T7 (period $2^3$). DFT-8 diagonalizes the cyclic shift, so the energy of each mode is fixed by the eigenvalue $\omega_8^k - 1$.
proof idea
Pure definition: unfold to the finite sum over $t : \mathrm{Fin},8$ of Complex.normSq applied pointwise to the discrete difference (cyclic_shift v t - v t). No lemmas or tactics; the noncomputable marker is inherited from complex norm-squared.
why it matters
This is the quadratic form whose spectrum forces the oscillation factor in the gap weights. Downstream, diffEnergy8_mode equates the energy of DFT mode $k$ to $|\omega_8^k - 1|^2$, and diffEnergy8_mode_eq_four_sin_sq closes the trig identity to $4\sin^2(k\pi/8)$. That identity is the precise reason a $\sin^2$ factor appears: it is (up to the fixed factor 4) the spectrum of the 8-tick discrete derivative.
geometricWeight_eq_spectrum_mul_measure then factors every nonzero mode weight as (difference-operator spectrum / 4) times the T9-forced lattice measure. Both factors are theorems. The bundle SpectralForcingCert packages this M6 closure. Nonnegativity (diffEnergy8_nonneg) is immediate from the sum of norm-squares.
Framework landmarks: T7 eight-tick octave; the claim-hygiene goal of removing hidden degrees of freedom from the geometric-weight construction that feeds $\alpha$ and the constants ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.