dft_coefficients_add
plain-language theorem explainer
The discrete Fourier coefficients of an 8-tick complex signal are additive in the signal: the k-th mode of f+g equals the sum of the k-th modes of f and g. Anyone building linear projectors or sector decompositions on the eight-tick ledger cites this. The proof unfolds the DFT sum and distributes multiplication and finite sums via the ring laws.
Claim. For any two 8-tick complex signals $f,g$ and any mode index $k\in\{0,\ldots,7\}$, the discrete Fourier coefficient satisfies $\widehat{f+g}(k)=\hat f(k)+\hat g(k)$.
background
In the Recognition Operator module the canonical state space is Signal8, an 8-sample complex signal on the forced eight-tick octave (T7: period $2^3$). The discrete Fourier transform on this cycle extracts mode amplitudes via a finite sum against the eighth roots of unity; those amplitudes are the dft_coefficients.
The local setting is the analytic 8-tick operator that replaced an older ledger-side API. Additivity of the coefficient map is the first half of $\mathbb{C}$-linearity needed before one can treat Fourier-mode projectors as genuine linear maps on the signal space.
Upstream arithmetic supplies the ring identities used in the sum: distributivity of multiplication over addition and the commutative-associative laws for addition, available both in the logic-native naturals and in the PRC integer layer.
proof idea
Term-style proof: unfold the definition of the DFT coefficient (a finite weighted sum), then simp with mul_add, Finset.sum_add_distrib, and the addition commutativity/associativity lemmas. The sum of products becomes a sum of sums, which rearranges to the sum of the two coefficient sums. No induction or case split is required.
why it matters
This lemma discharges the map_add' obligation inside sectorProject, the canonical linear projector that keeps only a chosen set of Fourier modes on Signal8. Without coefficient additivity the projector would not be a LinearMap and the structured-sector calculus on the eight-tick operator would not typecheck.
In the broader framework the eight-tick DFT is the spectral face of T7 (the forced octave). Linearity of the mode map is the elementary bridge from the raw recognition operator to sector decompositions used by later ledger and gravity bridges. The companion scalar-homogeneity fact (not this lemma) completes full $\mathbb{C}$-linearity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.