dft8Size_8
plain-language theorem explainer
The equality dft8Size = 8 follows by direct evaluation of the upstream definition dft8Size := 2^3. Researchers working on Recognition Science complexity bounds cite it to confirm that the discrete Fourier transform over the eight-point group remains polynomial-time when D equals three. The proof is a single decide tactic that computes the power.
Claim. The size of the discrete Fourier transform on eight points equals eight: $dft8Size = 8$, where $dft8Size := 2^3$.
background
In the module ComputationalComplexityFromRS the five canonical classes P, NP, coNP, PSPACE, EXP are identified with configDim D = 5. The upstream definition states dft8Size : ℕ := 2 ^ 3, which encodes the DFT-8 size as 2^D. The module doc notes that |ℤ/8ℤ| = 8 = 2^D places DFT computation in P, consistent with the eight-tick octave arising from D = 3 in the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the numerical equality 2^3 = 8.
why it matters
This supplies the dft_poly field inside computationalComplexityCert, anchoring the claim that DFT remains polynomial-time. It directly supports the module statement that |ℤ/8ℤ| = 8 = 2^D places the transform in P and connects to the eight-tick octave (T7) and D = 3 (T8) landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.