dft_coefficients_smul
plain-language theorem explainer
Scalar homogeneity of the 8-mode DFT: the coefficient of mode k on a•f equals a times the coefficient on f. Anyone building linear maps from Fourier data on the eight-tick signal space cites this. The proof unfolds the sum definition and pulls the scalar through a finite sum by complex multiplication identities.
Claim. For every $a \in \mathbb{C}$, every 8-tick signal $f : \mathrm{Fin}\,8 \to \mathbb{C}$, and every mode index $k \in \mathrm{Fin}\,8$, the DFT coefficient satisfies $\widehat{(a\cdot f)}(k) = a\,\widehat{f}(k)$, where $\widehat{v}(k) = \sum_t \overline{\mathrm{mode}_k(t)}\,v(t)$.
background
The ambient object is Signal8, the space of complex-valued functions on an eight-tick discrete circle (the RS octave period $2^3$ from the forcing chain T7). The module treats the recognition operator analytically on this space rather than on the older ledger-state API.
Upstream, dft_coefficients is the unnormalized DFT map
$c_k = \sum_t \overline{\mathrm{dft8_entry}(t,k)},v(t)$.
It is the standard inner-product extraction of Fourier amplitudes against the eight discrete modes. The Kronecker delta on Fin n appears elsewhere in the spectral layer for mode orthonormality, but is not needed for this scalar identity.
The local setting is the foundation layer that equips the eight-tick operator with linear algebra so sector projectors and bond/channel structure can be stated as genuine $\mathbb{C}$-linear maps.
proof idea
Term-mode proof by unfolding dft_coefficients to its finite sum, then a single simp pass. The scalar action on the signal is pointwise (Pi.smul_apply), so each summand becomes $a$ times the original summand. Finset.mul_sum / Finset.sum_mul pull $a$ outside the sum; mul_assoc, mul_left_comm, and mul_comm rearrange the complex products into the form $a \cdot c_k$. No mode-table identities are required.
why it matters
This is the scalar half of DFT linearity on the eight-tick circle. Downstream, sectorProject builds the canonical $\mathbb{C}$-linear projector onto a structured sector by summing only the kept modes:
$t \mapsto \sum_{k \in S.\mathrm{keepModes}} \widehat{f}(k),\mathrm{mode}_k(t)$.
That definition needs $\widehat{a\cdot f}(k)=a\widehat{f}(k)$ (together with additivity) so the projector is a genuine linear map on Signal8.
In the Recognition framework this sits under the eight-tick octave (T7): Fourier sectors on the discrete period-8 ledger are the natural language for channel and bond structure. Without scalar homogeneity, sector projection would not be linear and the analytic recognition operator could not act as a linear operator on mode subspaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.