idft8
plain-language theorem explainer
Re-export of the inverse length-8 discrete Fourier transform on eight-tick signals. Maps a frequency-domain Signal8 back to the time domain by the unitary formula with factor 1/√8 and powers of the primitive eighth root ζ. Cited wherever OperatorCore needs the inverse DFT without importing the parent ComplexStructureForcing module directly. Pure abbreviation; no proof content.
Claim. The inverse DFT on eight-tick complex signals is the map $F^{-1}$ sending $g:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$ to $(F^{-1}g)(j)=(1/\sqrt{8})\sum_{k=0}^{7} g(k)\,\zeta^{kj}$, where $\zeta$ is a fixed primitive eighth root of unity.
background
Recognition Science forces an eight-tick discrete clock (forcing chain T7: period $2^3$). Complex structure on that clock is developed via the length-8 DFT backbone: signals are functions Signal8 = Fin 8 → ℂ, and the forward transform uses powers of a primitive eighth root ζ.
The inverse transform undoes that map. Upstream it is defined by the standard unitary formula $(F^{-1}g)(j)=(1/\sqrt{8})\sum_k g(k),\zeta^{kj}$. The factor $1/\sqrt{8}$ makes the pair unitary with respect to the eight-point inner product, so mode costs and J-cost comparisons stay norm-preserving.
This module (OperatorCore.ComplexStructureForcing) re-exports the parent definition under a short local name so operator-level lemmas can cite the inverse without a long qualified path.
proof idea
No proof. The declaration is a one-line abbrev that aliases IndisputableMonolith.Foundation.ComplexStructureForcing.idft8. All mathematical content lives in that upstream def.
why it matters
Gives OperatorCore a stable handle on the inverse eight-point DFT used when complex structure is forced on the eight-tick octave. Downstream and upstream coincide here: the same idft8 is the definition being re-exported, so this alias is plumbing for the DFT/IDFT pair that underpins unitary evolution, mode costs, and eigenvalue analysis of the shift on Fin 8.
In the broader framework it sits under T7 (eight-tick period) and the complex-structure forcing that turns the discrete clock into a setting where J-cost and total mode cost can be compared in the frequency domain. Without a named inverse, unitarity and Parseval-type identities for the eight-tick ladder cannot be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.