dft8Modes_8
plain-language theorem explainer
The equality dft8Modes = 8 fixes the discrete Fourier transform at exactly eight modes, matching 2^D with D = 3 in the Recognition Science setting. Numerical analysts certifying FFT implementations under RS-native units cite this to anchor the canonical eight-mode count. The proof is a one-line decision procedure that evaluates the definition 2 ^ 3 directly.
Claim. The number of modes in the discrete Fourier transform equals eight: $2^3 = 8$.
background
The Numerical Analysis from RS module states that five canonical numerical methods equal configDim D = 5. DFT-8 is the canonical algorithm with 8 = 2^D modes, while the fast Fourier transform realizes O(N log N) = O(8 × 3) operations per tick. The upstream definition sets dft8Modes : ℕ := 2 ^ 3. The tick is the fundamental RS time quantum τ₀ = 1, and one octave consists of eight ticks.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the definition dft8Modes := 2 ^ 3 and confirm equality with 8.
why it matters
This theorem supplies the eight_modes field inside numericalAnalysisCert, which certifies the five numerical methods together with the FFT operations count. It directly realizes the eight-tick octave (T7) and D = 3 spatial dimensions (T8) from the unified forcing chain. The result closes the numerical certification loop with zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.