dft8_row_orthonormal
plain-language theorem explainer
Row orthonormality of the DFT-8 matrix: the sum over k of conjugate(B_sk) B_tk equals the Kronecker delta δ_{s,t}. Cited by anyone assembling unitarity of the eight-point DFT or the inverse mode expansion on the 8-tick cycle. The proof is a short reduction: entry symmetry swaps indices, then column orthonormality applies directly.
Claim. For all $s,t\in\{0,\ldots,7\}$, $\sum_{k=0}^{7}\overline{B_{sk}}\,B_{tk}=\delta_{s,t}$, where $B_{jk}=\omega^{jk}/\sqrt{8}$ are the DFT-8 matrix entries and $\omega=e^{-2\pi i/8}$ is the primitive eighth root of unity.
background
The module builds the eight-point Discrete Fourier Transform as the canonical unitary basis for the Recognition Science 8-tick cycle (period $2^3$, forced at T7 with $D=3$). The primitive root is $\omega=e^{-2\pi i/8}$; matrix entries are $B_{tk}=\omega^{tk}/\sqrt{8}$. Columns of this matrix are the DFT modes; the cyclic shift on 8-vectors is the discrete time-evolution generator, with eigenvalues $\omega^k$ on mode $k$.
Column orthonormality (already proved in-module) states $\sum_s\overline{B_{sk}}B_{st}=\delta_{k,t}$. Entry symmetry $B_{tk}=B_{kt}$ is available as a sibling lemma, so rows and columns are interchangeable for the Hermitian inner product. The physical point of the basis is that it diagonalizes cyclic shift, splits the DC mode from the seven neutral modes, and supplies the spectral frame for the eight-tick octave.
proof idea
Rewrite each summand via entry symmetry: $\overline{B_{sk}}B_{tk}=\overline{B_{ks}}B_{kt}$. After simp_rw on that identity, the sum is exactly the column-orthonormality sum with indices $(s,t)$. Finish by applying the already-proved column orthonormality lemma. No fresh geometric-sum argument is needed; the work is pure index swap.
why it matters
Row orthonormality is the missing half of $B^H B=I$ in the row picture. Downstream, inverse_dft_expansion uses it (together with the dual column form) to justify $v=B(B^H v)$, i.e. $v(t)=\sum_k\langle\mathrm{mode}k,v\rangle,B{tk}$. That expansion is the spectral reconstruction step on the 8-tick cycle.
In the framework this sits under the eight-tick octave (T7) and the DFT backbone that diagonalizes discrete time translation. Without both row and column orthonormality, unitarity of DFT-8 and the neutral-subspace claims remain incomplete. The result is fully proved; it closes no open scaffold, it simply finishes the unitary package used by shift diagonalization and mode expansions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.