idft8
plain-language theorem explainer
Defines the inverse discrete Fourier transform on 8-tick complex signals: each output sample is the normalized sum of input samples against powers of a primitive 8th root of unity. Anyone working the complex-structure forcing argument (diagonalizing the cyclic shift) cites this as the reconstruction half of DFT-8. The body is a direct pointwise formula, not a derived theorem.
Claim. For a complex-valued signal $g$ on the eight-tick cycle ($g : \{0,\ldots,7\} \to \mathbb{C}$), the inverse DFT-8 is the signal $(F^{-1}g)(j) = \frac{1}{\sqrt{8}} \sum_{k=0}^{7} g(k)\,\zeta^{kj}$, where $\zeta$ is a fixed primitive eighth root of unity.
background
The module Complex Structure Forcing argues that the eight-tick shift (T7) cannot be diagonalized over the reals: its eigenvalues are the eighth roots of unity, and $\omega^2 = i$ has no real square root because $x^2+1>0$ for all real $x$. Complexification is therefore forced, and the DFT-8 is the canonical unitary that diagonalizes the cyclic shift.
A signal on the cycle is simply a map from $\mathrm{Fin},8$ to $\mathbb{C}$. The forward DFT uses the conjugate root; this definition supplies the inverse kernel with the same normalization $1/\sqrt{8}$, so that the pair is unitary (Parseval) once the usual orthogonality identities are in place.
Sibling material in the file builds the shift operator, its iterates of period 8, the DFT basis vectors, and the eigenvalue $i$ at mode 2. The inverse transform is the reconstruction map that closes that spectral picture.
proof idea
Pure definition: no proof obligations. For each output index $j$, evaluate the finite sum $\sum_{k:\mathrm{Fin},8} g(k),\zeta^{k\cdot j}$ and scale by the complex cast of $1/\sqrt{8}$. The root $\zeta$ and the type Signal8 are ambient in the module; the formula matches the classical unitary IDFT-8 kernel.
why it matters
Closes the reconstruction half of the DFT-8 pair used to force complex Hilbert structure from cost axioms and the eight-tick octave (T7). The module registry item is exactly the gap "complex Hilbert space from cost," depending on T5 (J-uniqueness), T7, and T8 ($D=3$). Downstream, OperatorCore re-exports this definition as an abbrev so spectral and unitarity lemmas can cite a single name.
Without an explicit inverse, one cannot state Parseval, phase invariance of J-cost on mode moduli, or the claim that admissibility-preserving maps are unitary. This def is scaffolding for those theorems rather than a theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.