dft8
plain-language theorem explainer
Re-export of the length-8 discrete Fourier transform on complex signals indexed by Fin 8. Maps an eight-tick waveform to its frequency modes with the unitary 1/√8 normalization and conjugate powers of the primitive 8th root of unity. Cited wherever Born-rule sector measures or the complex-structure certificate need the DFT on the forced octave. Pure abbreviation; no local proof.
Claim. Write $\mathrm{DFT}_8$ for the map sending an eight-component complex signal $f$ to the signal $F$ with $F(k) = \frac{1}{\sqrt{8}} \sum_{j=0}^{7} f(j)\,\overline{\zeta}^{kj}$, where $\zeta$ is a primitive eighth root of unity. This declaration is the local name for that transform.
background
In the Recognition foundation, the eight-tick octave (forcing chain T7) supplies a discrete time circle of length 8. A Signal8 is a map $\mathrm{Fin},8\to\mathbb{C}$: one complex amplitude per tick. The shift operator on that circle has period 8 and spectrum the eighth roots of unity; its eigenbasis is the DFT basis.
The upstream definition states the transform explicitly: $F(f)(k)=\frac{1}{\sqrt{8}}\sum_j f(j),\overline{\zeta}^{kj}$. The factor $1/\sqrt{8}$ makes the map unitary for the standard Hermitian inner product on $\mathbb{C}^8$, so Parseval holds and total $\ell^2$ mass (sector measure of the full set) is preserved.
This module (OperatorCore.ComplexStructureForcing) only re-exports that name so operator-core and Born-rule developments can cite a single short identifier without threading the longer foundation path.
proof idea
No proof body: the declaration is an abbrev equating the local name to IndisputableMonolith.Foundation.ComplexStructureForcing.dft8. All mathematical content lives in that upstream def (normalized sum against conjugate powers of $\zeta$). Downstream lemmas such as unitarity and matrix form are proved against the upstream object; the abbrev is transparent to the type checker.
why it matters
DFT-8 is the bridge from the forced 8-tick clock to frequency-domain Born statistics. The master ComplexStructureCertificate lists DFT unitarity (inner8 (dft8 f) (dft8 g) = inner8 f g) as one of the certificate fields tying cost axioms T5–T8 to a complex structure: the shift has $T^8=I$ and an imaginary eigenvalue, and the DFT diagonalizes that action.
Born-rule forcing uses it heavily: dft_sector_total_eq is the Parseval corollary that total sector measure is invariant; isNormalized_dft8 lifts normalization across the transform; dft8_sector_forcing_freq restates sector-probability axioms on DFT modes (phase rotation invariance of sector masses). Without this name, the octave would stay a pure time-domain object and the complex/Born layer could not quote a canonical frequency basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.