diff8
plain-language theorem explainer
Defines the discrete one-step difference on complex 8-tick signals: pointwise (Sv − v), with S the cyclic shift. Gap-weight and DFT-projection arguments cite it as the local shift-invariant operator whose squared energy produces the sin²(πk/8) spectral weights. The body is a one-line pointwise definition, not a proof.
Claim. For any complex-valued map $v$ on the eight-tick cycle $\mathrm{Fin}\,8$, the discrete difference is $(\mathrm{diff}\,v)(t) := (Sv)(t) - v(t)$, where $S$ is the cyclic shift by one tick (indices mod 8). Equivalently, $\mathrm{diff} = S - I$ as an operator on $\mathbb{C}^8$.
background
The module GapWeight.Projection makes two historically implicit choices explicit: the geometric weight factor $\sin^2(\pi k/8)$ and the normalization $64 = 8\times 8$. The first is the spectral weight of a discrete derivative (or Laplacian) on the eight-tick cyclic shift; the second is the cardinality of the fundamental RS interface cell (8 ticks times 8 vertices of the $Q_3$ cell).
The eight-tick cycle is the RS octave clock (forcing landmark T7). The cyclic shift $S$ advances the reading index by one tick: $(Sv)(t) = v(t+1 \bmod 8)$. It is the fundamental discrete time-evolution generator on Signal8-type data. This definition packages the first-order difference $S-I$ as a named operator so downstream energy and mode lemmas can quote it cleanly.
proof idea
Pure definition: no tactics or lemmas. The value at tick $t$ is cyclic_shift v t - v t, i.e. the pointwise action of $S-I$. Downstream energy sums and mode calculations unfold this equation and then use the DFT shift-eigenvector relation.
why it matters
This operator is the concrete discrete derivative whose total squared energy diffEnergy8 is the canonical local, shift-invariant quadratic form on the octave. The mode lemma diffEnergy8_mode then shows that on DFT mode $k$ the energy equals $|\omega_8^k - 1|^2$, which (up to a fixed factor 4) is proportional to $\sin^2(\pi k/8)$. That identity is the module's stated reason the geometric gap weights carry a $\sin^2(\pi k/8)$ factor: it is forced by shift-diagonalization of $S-I$, not chosen by hand.
In the broader RS chain this sits under the eight-tick octave (T7) and the claim-hygiene program that removes hidden measure/operator freedom from constant and gap-weight derivations. Parents in-module are the energy functional and its modal spectrum identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.