dft8_entry_sym
plain-language theorem explainer
DFT-8 matrix entries are symmetric under swap of time and frequency indices: B_{t k} = B_{k t}. Anyone proving row orthonormality from column orthonormality cites this. The proof unfolds the entry definition and applies natural-number multiplication commutativity on the exponent.
Claim. For all $t,k \in \{0,\ldots,7\}$, the DFT-8 matrix entry $B_{tk} = \omega^{t k}/\sqrt{8}$ equals $B_{kt}$, where $\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 eight-tick recognition cycle. The period $\tau_0 = 2^D$ with $D=3$ is forced by the Recognition axioms (T7 eight-tick octave, T8 spatial dimension three). The primitive root is $\omega = e^{-2\pi i/8}$, and each matrix entry is defined by
$$B_{tk} := \omega^{t\cdot k}/\sqrt{8},$$
with $t$ the time (row) index and $k$ the frequency (column) index on $\mathrm{Fin},8$.
Because the exponent is the product of the two integer representatives, the only algebraic content needed for index symmetry is commutativity of multiplication in $\mathbb{N}$. Upstream, that is ordinary Nat.mul_comm (and parallel commutativity lemmas in the integer/orbit layers). The module's larger goal is unitarity of the full $8\times 8$ matrix and diagonalization of the cyclic shift, which separate the DC mode from the seven neutral modes.
proof idea
Term-mode, two steps. Unfold the definition of the entry so both sides become $\omega^{t.val\cdot k.val}/\sqrt{8}$ and $\omega^{k.val\cdot t.val}/\sqrt{8}$. Then simp with Nat.mul_comm equates the exponents; the common normalizing factor $\sqrt{8}$ is unchanged. No complex analysis or root-of-unity identities are required.
why it matters
Row orthonormality (dft8_row_orthonormal) is proved from column orthonormality precisely by rewriting each summand via this symmetry: $\overline{B_{s k}}B_{t k} = \overline{B_{k s}}B_{k t}$. That step is the documented bridge in the downstream theorem.
In the framework, DFT-8 is the unique (up to permutation/phase) unitary basis that diagonalizes time-translation on the forced eight-tick cycle and splits DC from the mean-free subspace. Symmetry of entries is a small but necessary algebraic fact on the path to dft8_unitary and the shift-eigenvalue calculus. It does not itself invoke J-cost, $\varphi$, or the RCL; it sits entirely inside the spectral backbone for T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.