← 研踪 PaperTrailarXiv:2611.01257 · v1
A Numerical Refinement of an Exact Discrete Fourier Transform Bound
首次提交 2026-11-01 04:49
版本更新 2026-11-01 04:49
雷达观测 2026-11-04 23:43
摘要
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.
观测到的版本
相邻记录可能跳过中间版本;首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-01 04:49 · 最新观测版本
A Numerical Refinement of an Exact Discrete Fourier Transform Bound
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.
查看此版本解读 →查看此版本原文 ↗