dftBasis
plain-language theorem explainer
Defines the eight DFT modes on the tick cycle: the k-th basis signal is the pure tone j ↦ ζ^{kj}, with ζ an 8th root of unity. Anyone citing the forced complex diagonalization of the eight-tick shift uses this as the eigenvector family. The body is a one-line pointwise power of ζ.
Claim. For each mode index $k \in \{0,\ldots,7\}$, the $k$-th DFT basis signal is the map $e_k:\{0,\ldots,7\}\to\mathbb{C}$ given by $e_k(j)=\zeta^{kj}$, where $\zeta$ is a primitive eighth root of unity. Each $e_k$ is an eigenvector of the cyclic shift on eight-tick signals.
background
The module forces complex structure from the eight-tick ledger dynamics (T7). The cyclic shift $T$ on eight-tick states satisfies $T^8=I$, so its spectrum consists of the eighth roots of unity. Over $\mathbb{R}$ the root $\omega^2=i$ has no representative ($x^2+1>0$ for all real $x$), so $T$ is not diagonalizable over $\mathbb{R}$ and the base field must extend to $\mathbb{C}$.
A signal on the eight-tick cycle is a function $\mathrm{Fin},8\to\mathbb{C}$. The DFT-8 supplies the canonical unitary eigenbasis of the shift. The companion definition records the eigenvalue at mode $k$ as $\zeta^k$. This basis is the concrete family those eigenvalues act on.
proof idea
Pure definition: the value of the $k$-th basis signal at tick $j$ is the complex power $\zeta^{k\cdot j}$. No lemmas are applied; the term is the pointwise monomial that diagonalizes the cyclic shift once the eigenvalue $\zeta^k$ is fixed.
why it matters
This is the eigenvector family in the complex-structure forcing argument. The module closes the gap from cost axioms (T5 J-uniqueness) and the eight-tick octave (T7) to a complex Hilbert space with genuine unitarity, depending also on $D=3$ (T8). Downstream facts in the same file identify eigenvalues $\zeta^2=i$ and $\zeta^6=-i$, prove there is no real root of $x^2+1$, and connect to phase-invariant J-cost and Parseval preservation. Without an explicit DFT basis, the claim that complexification is algebraically forced rather than chosen stays schematic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.