dft8_unitary
plain-language theorem explainer
The 8×8 DFT matrix B with entries ω^{tk}/√8 is unitary: B^H B = I. Anyone working the eight-tick spectral backbone or the T7 canonical-carrier bridge cites this. The proof is a matrix-entry reduction that hands the sum off to column orthonormality of the DFT-8 modes.
Claim. Let $B$ be the $8\times 8$ DFT matrix with entries $B_{t,k}=\omega^{tk}/\sqrt{8}$, where $\omega=e^{-2\pi i/8}$. Then $B^{\dagger}B=I_8$.
background
The Spectral.DFT8 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; the DFT-8 basis is the unique (up to permutation and phase) unitary frame that diagonalizes cyclic time translation, splits the DC mode $k=0$ from the neutral modes $k=1..7$, and supplies $\varphi$-lattice quantization through complex exponentials.
Notation: $\omega_8$ is the primitive eighth root $e^{-2\pi i/8}$; dft8_entry is the normalized matrix entry $\omega^{tk}/\sqrt{8}$; dft8_matrix assembles those entries into the full $8\times 8$ operator $B$. Unitary means $B^H B=I$, equivalently that the columns form an orthonormal basis of $\mathbb{C}^8$.
The immediate upstream fact is column orthonormality: $\sum_t \overline{B_{t,i}}B_{t,j}=\delta_{ij}$. That identity is the concrete root-of-unity sum that makes the matrix product collapse to the identity.
proof idea
Tactic proof by matrix extensionality on indices $i,j$. Expand $(B^H B)_{i,j}$ via Matrix.mul_apply and conjTranspose_apply, and expand the identity via one_apply. The resulting sum $\sum_t \overline{\mathrm{dft8_entry},t,i}\cdot\mathrm{dft8_entry},t,j$ is definitionally the left-hand side of column orthonormality. A single convert dft8_column_orthonormal i j finishes the goal. No separate root-of-unity algebra is redone here; it lives in the column-orthonormality lemma.
why it matters
Unitary DFT-8 is the spectral backbone of the eight-tick octave (T7). Downstream, dft8_preserves_inner quotes it as Plancherel: $\langle F(f),F(g)\rangle=\langle f,g\rangle$, so the transform is an isometry on Signal8. The T7-to-canonical-carrier bridge in UnifiedForcingChain names DFT-8 unitarity among the certificate fields that lock the carrier Fin 8 → ℂ, the period-8 cyclic shift, and the algebraic need for $\mathbb{C}$ over $\mathbb{R}$.
In the forcing chain this sits under T7 (eight-tick octave) and feeds the complex-structure forcing layer that produces $I$ in the shift spectrum and the Hamiltonian small-deviation expansion $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$. Without $B^H B=I$, the canonical carrier certificate and Parseval identity do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.