fourierCert
plain-language theorem explainer
Recognition Science requires a certificate confirming exactly five Fourier operations, an 8-mode DFT-8 structure, and a positive fundamental frequency to match the 8-tick harmonic comb at D=3. The fourierCert definition supplies this bundled certificate for use in QFT derivations. It is assembled by direct record construction from the decide-based cardinality lemmas and the div_pos positivity proof.
Claim. The Fourier certificate asserts that the cardinality of FourierOperation equals 5, that the DFT-8 mode count equals 8, and that the fundamental frequency satisfies $0 < dft8Fundamental$.
background
The module establishes Fourier analysis in RS as the decomposition into frequency components where the DFT-8 equals the 8-tick harmonic comb. This yields exactly 8 = 2^D modes when D=3, with fundamental frequency 5φ/8 Hz and five canonical operations (DFT, FFT, convolution, correlation, power spectrum) matching configDim D=5. The FourierCert structure packages the three required properties: five_ops as Fintype.card FourierOperation = 5, dft8_modes as dft8ModeCount = 8, and fundamental_pos as 0 < dft8Fundamental.
proof idea
The definition constructs the FourierCert record by direct field assignment. five_ops is set to the theorem fourierOperationCount (which applies decide), dft8_modes to dft8_eq_8 (also decide), and fundamental_pos to dft8Fundamental_pos (which unfolds and applies div_pos with phi_pos and norm_num).
why it matters
This definition certifies the Fourier component of the Recognition Science framework, directly supporting the 8-tick octave (T7) and D=3 (T8) by confirming DFT-8 modes equal 2^3. It feeds the quantum error correction derivations that reuse dft8_eq_8. The module links RS-native constants to the five-operation count without open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.