conjTranspose_shift_mul
plain-language theorem explainer
Entrywise, the conjugated DFT-8 sandwich of the cyclic shift equals ω^j on the diagonal and zero off it. Anyone proving that DFT-8 diagonalizes the eight-tick shift cites this identity. The proof expands the triple product, factors ω^j via the shift-on-DFT entry rule, then invokes column orthonormality of the DFT matrix.
Claim. For all indices $i,j \in \{0,\ldots,7\}$, the $(i,j)$-entry of $B^H (S B)$ equals $\omega^j \delta_{ij}$, where $B$ is the unitary $8\times 8$ DFT matrix with entries $B_{tk}=\omega^{tk}/\sqrt{8}$, $S$ is the cyclic shift matrix, and $\omega=e^{-2\pi i/8}$ is the primitive eighth root of unity.
background
The DFT-8 module builds the canonical unitary basis for the forced eight-tick recognition cycle (period $2^3$, landmark T7). The primitive root $\omega=e^{-2\pi i/8}$ defines matrix entries $B_{t k}=\omega^{t k}/\sqrt{8}$. The cyclic shift $S$ advances the reading index by one tick mod 8; it is the discrete time-evolution generator on eight-component signals.
Unitary of $B$ means $B^H B=I$, so the columns are orthonormal: $\sum_t \overline{B_{t i}} B_{t j}=\delta_{ij}$. The present lemma is the entrywise form of the similarity that turns $S$ into a pure phase diagonal. Upstream, the shift-on-column identity supplies $(S B){t j}=\omega^j B{t j}$, which is the algebraic engine of the factorization below.
proof idea
Expand the $(i,j)$-entry of $B^H(SB)$ as $\sum_t \overline{B_{t i}},(SB){t j}$ via the matrix-multiply and conjugate-transpose definitions. For each summand apply the entry identity that $(SB){t j}=\omega^j B_{t j}$, then rearrange by ring to factor $\omega^j$ out of the sum. Pull the scalar through the finite sum. The remaining sum is exactly the column inner product $\sum_t \overline{B_{t i}} B_{t j}$, which equals $\delta_{ij}$ by DFT-8 column orthonormality. Multiplying by the Kronecker delta finishes the claim.
why it matters
This is the entrywise engine of dft8_diagonalizes_shift, which states $B^H S B=\mathrm{diag}(1,\omega,\ldots,\omega^7)$. That global diagonalization is listed among the module's main results: DFT-8 is the unique (up to permutation/phase) unitary basis that diagonalizes time-translation on the eight-tick cycle, separates the DC mode from the neutral subspace, and supplies $\varphi$-lattice quantization via complex exponentials.
In the Recognition forcing chain the eight-tick octave is T7, forced once $D=3$ spatial dimensions are fixed at T8. Without the entrywise phase-times-delta identity, the spectral decomposition of the recognition clock does not close in Lean. Downstream work on shift eigenvalues and the neutral (mean-free) subspace rides on this sandwich.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.