dft8Modes
plain-language theorem explainer
The definition sets the number of modes in the eight-point discrete Fourier transform to two raised to the third power. Researchers certifying numerical methods in Recognition Science reference this constant when counting operations in the fast Fourier transform implementation. It is introduced by direct assignment of the arithmetic expression 2^3.
Claim. The number of modes for the eight-point discrete Fourier transform is defined by $2^3$.
background
The module derives five canonical numerical methods from Recognition Science, with their count equal to the configuration dimension D set to five. DFT-8 supplies the canonical algorithm whose mode count equals 2^D, and D equals three from the spatial dimension in the forcing chain. This produces eight modes, with the fast Fourier transform reducing complexity to eight times three operations per tick.
proof idea
The declaration is a direct definition that assigns the natural number 2^3 to the constant. No lemmas or tactics are invoked; the value is obtained by evaluating the power expression.
why it matters
This constant is required by the NumericalAnalysisCert structure to record eight modes alongside five methods and twenty-four FFT operations. It realizes the eight-tick octave (period 2^3) and the spatial dimension D=3 from the T0-T8 forcing chain. The definition supplies the base value used in the downstream equality proof dft8Modes_8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.