dft8Mode
plain-language theorem explainer
DFT-8 mode amplitudes on the eight-tick vertex space: the (k,j) entry is ω^{kj}/√8 with ω = e^{2πi/8}. Anyone analyzing the cycle-operator spectrum, Born-rule forcing, or generation mixing on ℂ⁸ cites this basis. The body is a one-line definitional formula, not a proved claim.
Claim. For mode index $k \in \{0,\ldots,7\}$ and vertex index $j \in \{0,\ldots,7\}$, the DFT-8 amplitude is $\omega^{kj}/\sqrt{8}$, where $\omega = e^{2\pi i/8}$ is the primitive eighth root of unity. These are the components of the mode vectors $|\psi_k\rangle = (1/\sqrt{8})\sum_j \omega^{kj}|j\rangle$.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary permutation matrix induced by the 8-tick Gray-code walk on the cube $Q_3$. Vertices of $Q_3$ are the computational basis; one tick flips exactly one bit along the Gray path, so a full period is an 8-cycle.
The primitive root omega8 is $\omega = e^{2\pi i/8} = e^{i\pi/4}$. Because the cycle has period 8, its eigenvalues are the eighth roots of unity $\omega^k$, and the corresponding eigenvectors are the standard DFT-8 modes. The module doc states that these eigenstates are the same modes used for Born-rule forcing, and that the per-tick phase of each mode encodes generation structure.
This definition supplies the individual complex amplitudes of those modes. The eight-tick period itself is forced in the unified chain (T7): at spatial dimension $D=3$ the canonical period is uniquely 8.
proof idea
Definitional, not a proof. The body is the closed-form DFT matrix entry: raise omega8 to the integer power $k\cdot j$ (values of the Fin 8 indices) and divide by $\sqrt{8}$. No lemmas are applied; noncomputability comes from complex exponential and real square root.
why it matters
Places the DFT-8 basis inside the Recognition cycle-operator story. The module presents these modes as eigenstates of $U_{\mathrm{cycle}}$ with eigenvalues $\omega^k$, and as the algebraic seed from which CKM-type mixing and generation structure are read off via per-tick phases. That sits on the eight-tick octave (T7) forced with $D=3$ (T8).
Downstream wiring is not yet recorded for this symbol (no used_by edges). The next section of the file turns to generation-axis correspondence: the three axes of $Q_3$ as three generations, with an asymmetric 4:2:2 flip schedule giving unequal coupling. The mode basis is the natural language for that spectral analysis and for linking to Born-rule forcing on the same eight-dimensional space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.