FourierCert
plain-language theorem explainer
FourierCert bundles three facts for recognition-derived Fourier analysis: the inductive type of Fourier operations has five elements, the DFT-8 transform has eight modes, and the fundamental frequency 5 phi over 8 is positive. A mathematician reconstructing harmonic analysis or QFT from the eight-tick recognition period would cite this certificate to confirm the dimension match. The declaration is a plain structure definition that directly states these three properties.
Claim. A certificate asserting that the set of five Fourier operations (DFT, FFT, convolution, correlation, power spectrum) has cardinality 5, that the DFT-8 mode count equals 8, and that the fundamental frequency satisfies $0 < 5 phi / 8$.
background
The module derives Fourier analysis from the recognition science framework, where the DFT-8 mode structure equals the 8-tick harmonic comb. The eight-tick recognition period produces 8 = 2^D Fourier modes at spatial dimension D = 3, while five canonical operations match configDim at D = 3. The fundamental frequency is given as 5 phi / 8 Hz.
proof idea
This is a structure definition with an empty proof body. It directly packages three facts: Fintype.card of the inductive FourierOperation type equals 5, dft8ModeCount equals 8 from its definition as 2^3, and the strict inequality 0 < dft8Fundamental where dft8Fundamental is defined as 5 * phi / 8.
why it matters
The structure feeds the downstream fourierCert definition that instantiates it via fourierOperationCount, dft8_eq_8 and dft8Fundamental_pos. It confirms the mode count matches the eight-tick octave (T7) and the operation count matches configDim at D = 3 (T8), closing a small bundling step before use in quantum error correction derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.