fftOps
plain-language theorem explainer
The definition fixes the number of fast Fourier transform operations per tick at 24 inside the Recognition Science numerical analysis module. Researchers certifying discrete transforms or counting operations in the five-method framework would reference this constant when verifying DFT-8 cost. It is supplied by a direct arithmetic assignment that matches the expected O(N log N) scaling for eight modes.
Claim. Let $N_{FFT}$ be the number of operations performed by the fast Fourier transform per tick. Then $N_{FFT} = 24$.
background
The module treats numerical analysis as five canonical methods whose cardinality equals the spatial dimension D = 5. DFT-8 supplies the canonical algorithm with exactly eight modes, while the fast Fourier transform implements it at O(N log N) cost. The supplied definition therefore records the concrete integer 8 × 3 = 24 that appears in the operation count per tick.
proof idea
The declaration is introduced by direct definition as the arithmetic product of eight and three.
why it matters
This constant supplies the missing numerical value needed to complete the NumericalAnalysisCert structure that bundles five methods, eight modes, and twenty-four FFT operations. It is invoked by the immediate theorem fftOps_24 that proves equality to 24. The choice 8 × 3 aligns with the eight-tick octave (T7) and D = 3 from the forcing chain, where 2^D modes produce the documented 3 × 8 operation count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.