dft8
plain-language theorem explainer
The normalized length-8 discrete Fourier transform on complex signals over the eight-tick cycle. It is the canonical unitary that diagonalizes the cyclic shift forced by T7. Downstream unitarity, Parseval, Born-rule sector measures, and the complex-structure certificate all quote this map. The body is the standard DFT sum with conjugate roots of unity and factor 1/√8.
Claim. For a complex signal $f$ on the eight-tick cycle ($f : \{0,\ldots,7\} \to \mathbb{C}$), the DFT-8 is $$(Ff)(k) = \frac{1}{\sqrt{8}} \sum_{j=0}^{7} f(j)\,\overline{\zeta}^{kj},$$ where $\zeta$ is a primitive eighth root of unity.
background
The module Complex Structure Forcing argues that the eight-tick ledger shift $T$ (from T7) satisfies $T^8 = I$ and therefore has eigenvalues the eighth roots of unity. The mode $\omega^2 = i$ has no real square root ($x^2+1>0$ on $\mathbb{R}$), so $T$ cannot be diagonalized over the reals: complexification is forced, not optional.
A signal on the cycle is simply a map $\mathrm{Fin},8\to\mathbb{C}$. The DFT-8 is the standard unitary change of basis that diagonalizes the cyclic shift. The conjugate powers of $\zeta$ appear so that the transform matches the usual spectral convention and pairs cleanly with the inverse (which uses unconjugated powers).
The local goal is to close the gap from cost axioms plus the eight-tick period to a complex Hilbert-space structure with genuine unitarity (Parseval, phase invariance of $J$-cost, admissibility-preserving evolution).
proof idea
Pure definition: pointwise, scale the sum $\sum_j f(j),\overline{\zeta}^{k\cdot j}$ by the complex scalar $1/\sqrt{8}$. No lemmas are invoked; later theorems identify this map with matrix multiplication by the canonical DFT-8 matrix and prove Plancherel from root-of-unity orthogonality.
why it matters
This is the concrete diagonalizing unitary in the complex-structure chain. The master certificate ComplexStructureCertificate records DFT unitarity as one of its fields (inner products preserved). Sibling theorems prove the map equals the spectral DFT matrix, preserves the eight-tick inner product (Parseval/Plancherel), and preserves norms.
Born-rule forcing uses it heavily: total sector measure is DFT-invariant, normalization is preserved, and frequency-domain sector probabilities inherit phase invariance. That links the eight-tick ledger to Born weights on DFT modes.
Framework landmarks: T7 (eight-tick octave) supplies the cyclic period; T5/T6 supply the cost that is phase-blind; together they force complex Hilbert structure rather than a real one. Closes the registry gap "complex Hilbert space from cost."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.