fftOps_24
plain-language theorem explainer
The equality between the fast Fourier transform operation count per tick and twenty-four certifies the computational cost of DFT-8 in Recognition Science numerical analysis. Researchers verifying the five canonical methods against the eight-tick structure would cite this result when assembling the overall certification. The proof is a direct decision on the arithmetic definition of the operation count as eight times three.
Claim. The fast Fourier transform requires exactly 24 operations per tick, where this count arises as eight modes times three operations per mode in the discrete Fourier transform implementation.
background
The module Numerical Analysis from RS presents five canonical numerical methods (Newton, Euler, Runge-Kutta, Gaussian elimination, FFT) as corresponding to configDim D = 5. DFT-8 supplies the canonical algorithm with 8 = 2^D modes, and the fast implementation yields O(N log N) cost specialized to 8 × 3 = 24 operations per tick. The upstream definition states that FFT operations per tick equal 8 times 3.
proof idea
This is a one-line wrapper that applies the decide tactic to the arithmetic definition of the fast Fourier transform operation count.
why it matters
This result supplies the fft_ops field inside the numericalAnalysisCert definition, completing the certification of five methods and eight modes. It directly instantiates the eight-tick octave with D = 3 spatial dimensions to produce the concrete operation count 24. No open questions remain at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.