FourierOperation
plain-language theorem explainer
The inductive enumeration defines five canonical Fourier operations as discrete Fourier transform, fast Fourier transform, convolution, correlation, and power spectrum. Researchers modeling frequency decompositions in Recognition Science tied to the eight-tick harmonic comb would cite this to match configDim D=5. The definition proceeds by direct inductive construction deriving Fintype for immediate cardinality access.
Claim. Let $F$ be the set of Fourier operations. Then $F$ consists exactly of the five elements discrete Fourier transform, fast Fourier transform, convolution, correlation, and power spectrum.
background
The module sets Fourier analysis in the Recognition Science setting where the DFT-8 mode structure equals the 8-tick harmonic comb. The 8-tick recognition period supplies 8 = 2^D Fourier modes while the five operations realize configDim D=5. Key relation: DFT has 8 = 2^3 modes at D=3. Upstream, powerSpectrum supplies the power spectrum of primordial perturbations with P(k) ∝ (H²/φ̇)² ∝ V³/(V')².
proof idea
The declaration is an inductive definition that lists the five constructors and derives DecidableEq, Repr, BEq, and Fintype in one step.
why it matters
This supplies the enumeration required by the FourierCert structure (five_ops : Fintype.card = 5, dft8_modes = 8) and the theorem fourierOperationCount. It realizes the framework point that five operations equal configDim D=5 and connects to the eight-tick octave (T7) together with D=3 (T8) from the forcing chain. The definition closes the mathematics module scaffolding for Fourier analysis from RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.