fourierOperationCount
plain-language theorem explainer
The theorem asserts that the inductive type enumerating five Fourier operations has cardinality exactly 5. Researchers deriving spectral properties inside Recognition Science cite this to confirm the operation count matches configDim at D=3. The proof is a one-line decision procedure that uses the Fintype instance generated by the inductive definition.
Claim. The cardinality of the set of Fourier operations is five: $Fintype.card(FourierOperation) = 5$, where FourierOperation consists of the discrete Fourier transform, fast Fourier transform, convolution, correlation, and power spectrum.
background
The module develops Fourier analysis from the Recognition Science framework. It begins with the eight-tick recognition period that produces eight Fourier modes equal to two to the power of the spatial dimension D=3. Five canonical operations are identified as matching the configuration dimension at this D value. The referenced definition introduces the inductive type FourierOperation with the five constructors DFT, FFT, convolution, correlation, and powerSpectrum. This type automatically derives DecidableEq, Repr, BEq, and Fintype, which enable direct cardinality statements. The upstream result is exactly this inductive definition, which supplies the structure required for the cardinality computation.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card FourierOperation = 5. The tactic succeeds at once because the inductive type with five distinct constructors derives a Fintype instance whose cardinality is statically five.
why it matters
This theorem supplies the five_ops field inside the fourierCert definition that assembles the Fourier certification for RS. It realizes the module claim that five operations equal configDim at D=3 and connects to the eight-tick octave together with the three-dimensional forcing step. No open questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.