inverse_dft_expansion
plain-language theorem explainer
Any complex 8-vector equals the sum of its DFT coefficients times the DFT-8 matrix columns (inverse DFT reconstruction). Spectral and ledger workers cite it to pass between time-domain ticks and frequency modes on the eight-tick cycle. The proof expands the coefficients, swaps the double sum, and collapses via row orthonormality to a Kronecker delta.
Claim. For every $v:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$ and every time index $t$, $v(t)=\sum_{k=0}^{7} c_k(v)\,B_{t,k}$, where $B_{t,k}=\omega^{tk}/\sqrt{8}$ is the DFT-8 entry ($\omega=e^{-2\pi i/8}$) and $c_k(v)=\sum_s \overline{B_{s,k}}v(s)$ is the $k$-th DFT coefficient.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by $D=3$ (period $2^3$). The primitive root is $\omega=e^{-2\pi i/8}$; matrix entries are $B_{t,k}=\omega^{tk}/\sqrt{8}$. Columns are the DFT modes; the DC mode ($k=0$) is the constant vector, and modes $k=1..7$ are the oscillatory neutral directions.
Unitary DFT means $B^H B=I$, hence also $B B^H=I$. Coefficients are the inner products $c_k(v)=\langle\mathrm{mode}k,v\rangle$. Row orthonormality states $\sum_k \overline{B{s,k}}B_{t,k}=\delta_{s,t}$, which is the algebraic engine of inversion.
Local setting: DFT-8 is the unique (up to phase/permutation) unitary basis that diagonalizes cyclic shift, separates DC from mean-free modes, and supplies $\varphi$-lattice phases for the recognition octave.
proof idea
Fix $t$ and unfold the coefficient definition so the right-hand side is $\sum_k\bigl(\sum_s \overline{B_{s,k}}v(s)\bigr)B_{t,k}$. A short algebraic rearrangement (sum-mul, mul-sum, commute sums, ring) rewrites this as $\sum_s v(s)\bigl(\sum_k \overline{B_{s,k}}B_{t,k}\bigr)$. Apply dft8_row_orthonormal pointwise in $s$ to replace the inner sum by $\mathbf{1}_{s=t}$. The remaining sum collapses by the standard sum_ite_eq' identity to $v(t)$.
why it matters
This is the reconstruction half of DFT unitarity on the eight-tick backbone. Downstream, dft8_neutral_subspace quotes it directly: any mean-free $v$ has vanishing DC coefficient, so inverse DFT writes $v$ in the span of modes $1..7$. That span fact is listed among the module's main results and underwrites the separation of conserved (DC) content from neutral ledger fluctuations on the forced period-$8$ cycle (T7 eight-tick octave, $D=3$).
Without inverse expansion, one cannot certify that the seven non-DC modes exhaust the mean-zero subspace, nor pass cleanly between tick-indexed postings and spectral coordinates. It is pure linear algebra on $\mathbb{C}^8$, but it is the bridge the rest of the spectral layer uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.