dft8Size
plain-language theorem explainer
The definition dft8Size assigns the value 8 to the size of the eight-point discrete Fourier transform, matching 2 raised to the spatial dimension D=3. Researchers studying computational complexity within Recognition Science cite it to confirm that DFT operations stay polynomial-time in D. The definition is introduced by direct assignment of the natural-number power 2^3.
Claim. The DFT-8 size is defined by $2^3 = 8$.
background
The module Computational Complexity from RS identifies five canonical classes (P, NP, coNP, PSPACE, EXP) with configDim D = 5. Recognition Science sets D = 3 spatial dimensions, yielding the eight-tick octave of period 2^3. The definition dft8Size supplies the concrete size 2^D = 8 so that DFT computation lies in P, polynomial-time in D. This rests on the observation that |ℤ/8ℤ| = 8 = 2^D.
proof idea
The definition is a direct assignment dft8Size := 2 ^ 3, which evaluates to 8 by the standard rules of natural-number exponentiation.
why it matters
This definition supplies the concrete value required by the ComputationalComplexityCert structure, which records five_classes : Fintype.card ComplexityClass = 5 together with dft_poly : dft8Size = 8. It implements the step that places DFT computation in P inside the RS conjecture that P ≠ NP because NP-complete problems possess an exponential number of J = 0 basins in the J-cost landscape. The value directly realizes the eight-tick octave forced by T7 and T8 of the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.