dft8_diagonalizes_shift
plain-language theorem explainer
The 8-point DFT unitarily diagonalizes the cyclic shift on 8-vectors: conjugating the shift by the DFT matrix yields diag(1, ω, …, ω⁷). Spectral and 8-tick analyses cite this as the time-translation eigenbasis. The proof is entrywise: associate the product, apply the precomputed Bᴴ(SB) formula, then finish by ring on the diagonal and off-diagonal cases.
Claim. Let $B$ be the $8\times 8$ DFT matrix with entries $\omega^{tk}/\sqrt{8}$ and $S$ the cyclic shift matrix on $\mathbb{C}^8$. Then $B^H S B = \mathrm{diag}(1,\omega,\omega^2,\ldots,\omega^7)$, where $\omega=e^{-2\pi i/8}$ is the primitive eighth root of unity and the $k$-th diagonal entry is the shift eigenvalue $\omega^k$.
background
The module builds the DFT-8 backbone for the forced eight-tick recognition cycle $\tau_0=2^D$ with $D=3$. The primitive root $\omega_8=e^{-2\pi i/8}$ supplies the phases; matrix entries are $\omega^{tk}/\sqrt{8}$, assembled into the unitary DFT matrix $B$. The cyclic shift $S$ is the time-translation operator on 8-vectors; its putative eigenvalues on DFT modes are $\omega^k$.
Physically, DFT-8 is the canonical unitary basis that diagonalizes time translation, splits the DC mode $k=0$ from the mean-free modes $k=1..7$, and quantizes the $\varphi$-lattice via complex exponentials. Upstream, the lemma on $B^H(SB)$ already evaluates the conjugated product entrywise as $\omega^j\delta_{ij}$, which is the algebraic content needed here.
proof idea
Work entrywise with ext i j. Reassociate the triple product so the middle factor is $S B$, then rewrite by the upstream lemma conjTranspose_shift_mul, which states $(B^H(SB)){ij}=\omega^j\delta{ij}$. Unfold the diagonal matrix and the shift-eigenvalue definition. On the diagonal branch ($i=j$) substitute and close by ring; off-diagonal, the zero factor likewise reduces by ring. No spectral theorem is invoked: the identity is pure finite matrix algebra over $\mathbb{C}$.
why it matters
This is a listed main result of the DFT-8 module and the concrete realization of time-translation diagonalization on the eight-tick octave (forcing landmark T7, period $2^3$). Together with unitarity of $B$ and the eigenvalue formula $\omega^k$, it licenses the split into the constant DC mode and the neutral (mean-free) subspace spanned by modes $k=1..7$, which the module records as the next structural claim.
In the Recognition framework the eight-tick cycle is not optional: $D=3$ forces period 8, so the unique (up to phase/permutation) unitary eigenbasis of the cyclic shift is the natural spectral language for ledger evolution, mode projections, and later $\varphi$-lattice quantization. No downstream dependents are wired yet in the graph; the theorem stands as infrastructure for neutral-subspace and mode-analysis developments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.