dft8_eq_8
plain-language theorem explainer
The equality dft8ModeCount = 8 confirms that the DFT-8 harmonic comb contains exactly eight modes, matching the eight-tick recognition period to D = 3 spatial dimensions via 2^D. Researchers in Recognition Science Fourier analysis cite it to anchor the mode count before constructing certificates for spectral signatures or quantum error correction. The proof reduces the claim to a direct numerical decision on the definition 2^3.
Claim. The number of modes in the DFT-8 equals 8, where the mode count is defined as $2^3$.
background
The Fourier Analysis from RS module treats Fourier analysis as decomposition into frequency components, with the DFT-8 realizing the 8-tick harmonic comb required by the Recognition Science eight-tick octave. The 8-tick recognition period forces eight Fourier modes equal to 2^D at D = 3. The sibling definition dft8ModeCount : ℕ := 2 ^ 3 supplies the left-hand side; an upstream duplicate definition in QuantumErrorCorrectionFromJCost sets the same symbol directly to 8.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the concrete equality 2^3 = 8.
why it matters
This theorem supplies the dft8_modes field inside the fourierCert certificate and the dft8_count field inside qecCert. It realizes the T7 eight-tick octave (period 2^3) and T8 D = 3 spatial dimensions from the forcing chain, confirming that DFT has 8 = 2^D modes at D = 3 with zero sorry statements in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.