star_dft8_entry_mul
plain-language theorem explainer
For fixed time index t, the product of a conjugated DFT-8 entry with another entry equals the corresponding product of powers of the primitive 8th root of unity, divided by 8. Spectral theorists proving column orthonormality of the 8-point DFT cite this. The proof unfolds the entry definition and cancels the two √8 normalizers.
Claim. For all $t,k,k'\in\{0,\ldots,7\}$, $\overline{B_{tk}}\,B_{tk'}=\overline{\omega^{tk}}\,\omega^{tk'}/8$, where $B_{tk}=\omega^{tk}/\sqrt{8}$ is the DFT-8 matrix entry and $\omega=e^{-i\pi/4}$ is the primitive 8th root of unity used in this module.
background
The DFT8 module builds the 8-point Discrete Fourier Transform as the canonical unitary basis for the Recognition Science 8-tick cycle (period $2^3$, forced at T7). The primitive root is $\omega=e^{-i\pi/4}$, and each matrix entry is $B_{tk}=\omega^{tk}/\sqrt{8}$ with row $t$ the time index and column $k$ the frequency index.
Column orthonormality of $B$ is the algebraic heart of unitarity: the inner product of columns $k$ and $k'$ is $\sum_t \overline{B_{tk}}B_{tk'}$, which must equal $\delta_{kk'}$. Before summing, one needs a clean expression for each summand in pure powers of $\omega$. That is exactly what this lemma supplies.
Upstream, dft8_entry is the normalized entry and omega8 is the root; both are unfolded here. The conjugate acts only on the complex exponential factor once the real normalizer is peeled off.
proof idea
Tactic proof. Unfold dft8_entry, then apply star_div₀ together with Complex.star_def and Complex.conj_ofReal so the conjugate hits only the power of $\omega$ and the real $\sqrt{8}$ stays real. Establish the local identity $(\sqrt{8}:\mathbb{C})\cdot\sqrt{8}=8$ by pulling the product back to reals and using Real.mul_self_sqrt. field_simp clears denominators; ring_nf rearranges; rewrite the squared root via that identity to obtain the claimed /8.
why it matters
Direct fuel for dft8_column_orthonormal, which states $\sum_t \overline{B_{tk}}B_{tk'}=\delta_{kk'}$ and is the fundamental orthonormality property of DFT-8. That result is a stepping stone to full unitarity (dft8_unitary: $B^H B=I$) and to the spectral facts that DFT diagonalizes the cyclic shift and separates the DC mode from the neutral subspace.
In the Recognition framework this sits on the eight-tick octave forced at T7 ($\tau_0=2^D$ with $D=3$ from T8). DFT-8 is the unique (up to permutation/phase) unitary basis that diagonalizes time-translation on the cycle and supplies $\varphi$-lattice quantization via complex exponentials. Without the normalized product identity, the column-sum argument does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.