shift_mul_dft8_entry
plain-language theorem explainer
The product of the cyclic shift matrix and the DFT-8 matrix has entries (SB)_{t,j} = ω^j B_{t,j}: each DFT column is a shift eigenvector with eigenvalue ω^j. Cited when building the eight-tick spectral diagonalization of time translation. Proof specializes the mode-wise eigenvector identity and collapses the matrix-product sum to the single nonzero shift entry.
Claim. For all indices $t,j\in\{0,\ldots,7\}$, if $S$ is the cyclic shift matrix on $\mathbb{C}^8$ and $B$ is the DFT-8 matrix with entries $B_{t,k}=\omega^{tk}/\sqrt{8}$ where $\omega=e^{-2\pi i/8}$, then $(SB)_{t,j}=\omega^j\,B_{t,j}$.
background
The DFT-8 module builds the canonical unitary basis for the Recognition Science eight-tick cycle. The period $\tau_0=2^D$ with $D=3$ is forced at T7 of the foundation chain; the spectral objects here take that discrete circle as given. The primitive root $\omega=e^{-2\pi i/8}$ defines matrix entries $B_{t,k}=\omega^{tk}/\sqrt{8}$, assembled into the full $8\times 8$ DFT matrix $B$.
The cyclic shift $S$ advances the tick index by one modulo 8 (a permutation matrix). DFT modes are the columns of $B$. The structural fact recorded here is that $S$ multiplies column $j$ by the scalar $\omega^j$, written entrywise as $(SB){t,j}=\omega^j B{t,j}$. This is the matrix form of the shift-eigenvalue relation used throughout the module's diagonalization results.
proof idea
Invoke the mode-wise eigenvector identity: the cyclic shift applied to DFT mode $j$ equals $\omega^j$ times that mode. Specialize at coordinate $t$. Expand $(SB)_{t,j}$ via the matrix product sum. The shift matrix has a single 1 in each row, at column $(t+1)\bmod 8$, so rewrite the sum with Finset.sum_eq_single on that index. The surviving term matches the specialized eigenvector identity (after unfolding DFT entry and mode definitions). Off-index summands vanish by the zero entries of the shift matrix. The empty-membership branch is absurd because the chosen index lies in Finset.univ.
why it matters
Immediate parent is the conjugate-transpose lemma showing $(B^H SB){i,j}=\omega^j\delta{i,j}$. That identity is the entrywise form of DFT diagonalizing the cyclic shift, listed among the module's main results alongside unitarity and the neutral-subspace split (modes $k=1..7$ mean-free). Without entrywise control of $SB$, the conjugated operator $B^H SB$ cannot be identified with $\mathrm{diag}(\omega^k)$.
In the Recognition framework this encodes time-translation symmetry of the eight-tick octave (T7) in the unique unitary basis that also separates DC from neutral modes and supplies $\varphi$-lattice phases via complex exponentials. It is scaffolding for any later spectral argument that treats tick-shift as a diagonal multiplier in the DFT frame.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.