A Numerical Refinement of an Exact Discrete Fourier Transform Bound
Zhihao Yao, Sichao Liu
cs.CC
Oct 31, 2026 · v1
cs.DS
TL;DR
The DFT work-bound theorem and convolution corollary are proved in Lean 4 and checked against a reference specification using Comparator. The Lean development is released as an artifact.
Abstract
We refine the numerical bounds in Kartal's instantiation of Sussman's exact discrete Fourier transform construction. For every integer n >= 1, the resulting algorithm computes the length-n transform with work O(n (log n)^(1 - delta)), where delta = 0.0030201659. The bound holds in an exact complex-arithmetic RAM model with a supplied canonical root of unity. This final exponent saving exceeds the earlier certified parameter C_0 = 0.00302016 by 5.9 x 10^(-9). We retain the underlying circuit, tighten rational bounds for sums of powers of its block and target ranks, and increase the fixed tensor power from 7760 to 11640. These bounds establish the inequalities for Sussman's recursion at the intermediate certificate parameter C = 0.00302016595. The gap C - delta absorbs the overhead of recursion and Fourier reduction. The resulting transform theorem is proved in Lean and checked against the reference problem statement.
Problem
Kartal's instantiation of Sussman's exact DFT construction certifies an exponent saving of C_0 = 0.00302016 in the O(n (log n)^(1-delta)) work bound. The task is to tighten the numerical certificate so the saving exceeds C_0.
Approach
The underlying circuit and its multisets of block and target ranks are kept unchanged. Tighter rational bounds are derived for power moments of these ranks, using truncated exponential series and certified logarithm bounds. The fixed tensor power is raised from 7760 to 11640 so the completion-and-splitting inequalities hold at C = 0.00302016595. The resulting theorem is verified in Lean 4.34.1, checked against the reference exact-DFT specification with Comparator, and cross-checked by an independent exact rational interval calculation.
Results
The length-n DFT is computed with work O(n (log n)^(1-delta)) for delta = 0.0030201659, which exceeds C_0 by 5.9e-9. The interval calculation also places the raw balance point between 0.00302016597701562048 and 0.00302016597701562050.
