mod8_mul_eq
plain-language theorem explainer
For the primitive eighth root of unity ω, the powers ω^(((t+1) mod 8)·k) and ω^((t+1)·k) agree for every tick index t in Fin 8 and every natural k. Anyone proving that DFT-8 modes are shift eigenvectors needs this congruence. The proof splits on whether t+1 wraps past 8 and uses ω^8 = 1.
Claim. Let $\omega = e^{2\pi i/8}$ be the primitive eighth root of unity. For every $t \in \{0,\ldots,7\}$ and every $k \in \mathbb{N}$, $$\omega^{((t+1)\bmod 8)\,k} = \omega^{(t+1)k}.$$
background
The module builds the eight-point DFT as the canonical unitary basis for the Recognition Science eight-tick cycle (period $2^3$, forced at T7). The primitive root is $\omega_8 = e^{2\pi i/8}$, with the standing identity $\omega_8^8 = 1$. DFT matrix entries are $\omega^{tk}/\sqrt{8}$; cyclic shift advances the reading index by one tick modulo 8.
When one evaluates a shifted DFT mode at tick $t$, the phase becomes $\omega^{((t+1)\bmod 8),k}$. The unshifted comparison is $\omega^{(t+1)k}$. Because exponents of $\omega$ live in $\mathbb{Z}/8\mathbb{Z}$, these two powers coincide; the present lemma records that equality in $\mathbb{C}$.
Upstream, omega8_pow_8 supplies $\omega^8=1$. The cyclic shift and eigenvalue definitions from ComplexStructureForcing/CycleOperator fix the same $\omega$ and the same mod-8 indexing used here.
proof idea
Invoke $\omega^8=1$. Case-split on $t.\mathrm{val}+1 < 8$ versus $\ge 8$.
- If strict inequality,
Nat.mod_eq_of_ltmakes the mod a no-op, so both sides are identical. - If $\ge 8$, then since $t.\mathrm{val}<8$ one has $t.\mathrm{val}+1=8$. The left exponent collapses via
Nat.mod_selfandzero_mul/pow_zeroto $\omega^0=1$. The right side is $\omega^{8k}=(\omega^8)^k=1^k=1$ bypow_mulandone_pow.
No external spectral lemmas are needed; the argument is pure root-of-unity arithmetic on Fin 8.
why it matters
This is the single algebraic step that lets dft8_shift_eigenvector conclude
$$\mathrm{cyclic_shift}(\mathrm{dft8_mode},k)=\omega^k\cdot\mathrm{dft8_mode},k.$$
That eigenvector identity is the heart of DFT diagonalizing the shift operator, listed among the module's main results (dft8_diagonalizes_shift, shift_eigenvalue).
In the Recognition framework the eight-tick octave (T7) is forced; DFT-8 is the unique (up to phase/permutation) unitary basis that diagonalizes discrete time translation and separates the DC mode from the neutral subspace. Without the mod-8 power identity, the phase bookkeeping on the left-hand side of the eigenvector equation does not match the right-hand side. The lemma is therefore scaffolding for the spectral backbone of the 8-tick cycle, not a physics claim on its own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.