结果族 130：Exact Fourier transforms below
@@M@@n\log n@@· 学科：Theoretical computer science · 验证状态：主结果已 Lean 形式化
把一台”乘法机器” @@M@@A@@ 用到一条 @@M@@q^b@@ 个坐标的大流水线上，教科书做法是沿 @@M@@b@@ 个方向各扫一遍，共 @@M@@b\cdot q^{b-1}@@ 次调用。本文证明：存在聪明的接线路径，配合”免费换线”，让调用次数严格少于这个数；并靠这一点，在完全不限制系数的电路模型里，把”算傅里叶变换必须花 @@M@@\Omega(n\log n)@@“的老猜想推翻了。
关键词卡片
@@M@@A\otimes A\otimes\cdots\otimes A@@，同一个小变换叠 @@M@@b@@ 层的大变换。@@M@@A@@ 的 @@M@@b@@ 层张量幂存在省调用的算法。看个具体例子
把盈余层层放大再”搬运”到傅里叶矩阵上：对任意常数 @@M@@c>0@@（比如 @@M@@c=1/100@@），都存在无穷增大的长度 @@M@@n@@（取互异素数之积），使精确傅里叶电路的规模不足 @@M@@c\cdot n\log_2 n@@ 个门——即比值 @@M@@L(n)/(n\log_2 n)@@ 的下极限为 0。
为什么值得关心
四十多年来 @@M@@\Omega(n\log n)@@ 下界在带系数限制的模型里屡试不爽，本文说明在最一般的非均匀复线性电路模型里它就是错的。
已 Lean 形式化
第一级台阶
导读里的”乘法机器与流水线”可说成：对象是一台固定的小机器 @@M@@A@@ 和一条 @@M@@q^b@@ 个坐标的长流水线，操作是把机器接到流水线的某些坐标上执行一次（记一次”调用”），调用之间允许任意”换线”——重排坐标并各自缩放，不另收费。教科书方案是沿 @@M@@b@@ 个方向各扫一遍，共 @@M@@b\cdot q^{b-1}@@ 次调用；论文的全部主张是：存在更聪明的接线路径，调用次数严格更少。
第二级台阶
本科术语化：线性电路由加、减、乘预选标量三种门组成，每个门记一次操作；非均匀指每个长度配一个专用电路，系数任意预置且生成不计费。单项矩阵指置换矩阵乘可逆对角阵，即”换线加缩放”。张量幂 @@M@@A^{\otimes b}@@ 是同一个小变换叠 @@M@@b@@ 层；逐轴标准算法恰需 @@M@@bq^{b-1}@@ 次 @@M@@A@@ 调用，严格改进即”有限盈余”。
第三级台阶
定理的语境：设 @@M@@L(n)@@ 为精确计算 @@M@@n@@ 点傅里叶矩阵 @@M@@F_n=(\zeta_n^{jk})@@ 的最小组数电路规模，则 @@M@@\liminf_{n\to\infty}L(n)/(n\log_2 n)=0@@。”系数不受限、生成不计费”的非均匀假设挡住了 Morgenstern 与 Ailon 下界的适用范围；结论只沿互异素数之积的无界长度序列成立，不承诺全部长度或均匀算法。论证两半拼合：一个有限盈余经张量放大与”恰好 @@M@@r@@ 个坐标”的局部编译传给傅里叶阵；反设无盈余则构造价格函数，被反射对合的上下界夹出矛盾。
本文在系数任意、非均匀的复线性电路（linear circuit）模型中，沿一列趋于无穷的长度构造出规模 @@M@@o(n\log n)@@ 的精确傅里叶电路，推翻了该模型下的 @@M@@\Omega(n\log n)@@ 下界猜想；核心是一个”有限张量盈余”的存在性证明。
精确计算 @@M@@n@@ 点傅里叶矩阵 @@M@@F_n=(\zeta_n^{jk})@@ 是否必须耗费 @@M@@\Omega(n\log n)@@ 次运算，是算术复杂度理论的老问题。已知下界均带附加条件：Morgenstern 1973 年的行列式论证要求系数有界；Ailon 的两个结果分别要求恰好 @@M@@n@@ 个寄存器配酉两坐标门、或对中间变换条件数的控制。在系数无界、允许任意预选常数的非均匀模型里，问题长期开放；上界方面 Alman–Rao 只改进了 2 的幂长度的常数因子。本文证明：在最一般的非均匀意义下，@@M@@\Omega(n\log n)@@ 下界不成立。
主定理：在该模型中 @@M@@\liminf_{n\to\infty}L(n)/(n\log_2 n)=0@@。等价地说，对任意 @@M@@c>0@@ 与任意阈值，都存在长度 @@M@@n@@（取互异素数之积、构成无界序列）以及规模不足 @@M@@c\,n\log_2 n@@ 个门的精确电路。模型计费严格：每个加、减、乘预选标量的门各记一次；系数的模、代数次数与描述长度不受限，其生成不计费；深度、存储与消去均无约束。支撑结论的是有限张量盈余（finite win）定理：存在可逆非单项（nonmonomial）矩阵 @@M@@A\in\GL_q(\mathbb C)@@、整数 @@M@@b\ge2@@ 与 @@M@@q^b@@ 个坐标上的词，用少于 @@M@@bq^{b-1}@@ 次 @@M@@A@@ 调用实现 @@M@@A^{\otimes b}@@，调用之间可自由插入可逆单项（monomial）映射。@@M@@bq^{b-1}@@ 正是逐轴标准算法的调用量。
全文分两半：有限盈余如何放大并传输给傅里叶矩阵，以及它为何必然存在。
前半从正生成引理开始：若 @@M@@A@@ 非单项，则 @@M@@A@@ 对角子空间的共轭撑满全矩阵空间，配合 Jacobi 行列式非零、Zariski 开集像与”两份模式相乘”，得到固定模式 @@M@@H=M_0AM_1\cdots AM_h@@，仅靠调节单项因子便能实现一切 @@M@@H\in\GL_q(\mathbb C)@@。张量放大引理把赢词自乘 @@M@@j=\lfloor k/b\rfloor@@ 层，调用槽的 @@M@@j@@ 重张量幂分解为直和 @@M@@\bigoplus_r(A^{\otimes r})^{\oplus\binom jr(Q-q)^{j-r}}@@，归一成本满足 @@M@@f(k)\le C_0+g\,\mathbb E f(K)@@，其中 @@M@@K@@ 服从二项分布；由严格盈余 @@M@@g\rho<1@@（@@M@@\rho=q/(Qb)@@）与凹性归纳，得 @@M@@A^{\otimes k}@@ 只需 @@M@@O(q^k(k+1)^\alpha)@@、@@M@@\alpha<1@@。传输阶段：Newton/Kuznetsov 型分解 @@M@@F_r=ND_N^{-1}N^{\mathsf T}@@ 把傅里叶阵化为三角 Toeplitz 阵，经位移秩（displacement rank）方法（残差秩至多 3）拆成卷积，再用 Bennett 式”计算—读取—逆算”重放在恰好 @@M@@r@@ 个坐标上借用脏坐标并复原，得 @@M@@O(\log^4 r)@@ 层的两坐标层；取 @@M@@n_m@@ 为前 @@M@@m@@ 个大于 @@M@@2q@@ 的素数之积（素数个数由初等组合估计保证），中国剩余定理给出 @@M@@F_{n_m}=\bigotimes_iF_{r_i}@@（至差一个置换）；把各轴的两坐标映射一律改写为 @@M@@A@@ 的固定正词并按时隙同步，每个 @@M@@A@@ 调用槽按活跃坐标分解为扇区直和，扇区宽度之和恰为 @@M@@n_m@@，总规模 @@M@@O(n_m(1+\log^4 m)(m+1)^\alpha)=o(n_m\log n_m)@@。
后半反设不存在任何有限盈余，由此构造价格函数 @@M@@p@@ 推出矛盾：比较打包与紧性论证给出在非单项矩阵上取正值、满足精确张量律与直和律的 @@M@@p@@；反馈构造（对新鲜数据反复调用、保留状态）使初始状态的修正费可忽略，证明可逆角块不贵于其宿主矩阵；标量枢轴律允许在两组基仍为基时交换一个输入与一个输出基向量而价格不变。最后的矛盾由反射制造：用 @@M@@C,Z,X@@ 型符号矩阵构造对合 @@M@@\Gamma@@，其价格精确等于 @@M@@dN/2@@；在 @@M@@w=N^2@@ 维取 @@M@@M=\Gamma\otimes\Gamma@@，其 @@M@@+1@@ 特征空间 @@M@@E@@ 既是对称稀疏阵 @@M@@A=SL@@ 的核（非对角支持对至多 @@M@@(d/2+1)w@@ 个），又是某个可逆矩阵的图像。上界：对每个支持对的多项式微扰至多 @@M@@3/2@@，经反馈单元与两次代数特化传给 @@M@@E@@ 上的正交反射 @@M@@R@@，得 @@M@@p(R)\le(\frac{3d}{4}+\frac72)w@@；下界：由图像表示做枢轴与和差对角化，能以 @@M@@O(w)@@ 的附加费从 @@M@@R@@ 复原 @@M@@M@@ 的价格 @@M@@dw@@，即 @@M@@dw\le p(R)+4w@@。取 @@M@@d>30@@ 时两式不相容，矛盾；故有限盈余存在，接上前半段即得主定理。
按任务信息，本文主结果已 Lean 形式化（结果族 130 附有 Lean 文档）。姊妹篇《An explicit power saving for the exact discrete Fourier transform》在同一证书接口上给出对所有长度的量化算法，两文互补：本文证有限盈余必然存在，该文给出显式网络与全长度实现。需注意本结论是非均匀存在性：系数逐电路预选且生成不计费，对数值稳定性与比特复杂度不作承诺；姊妹篇尚未形式化，按 OpenAI 官方声明，未经形式化的结果可能有问题，请以社区核验为准。
问 1：证明中最关键、最脆弱的一步是什么？
答：反设”不存在有限盈余”后的反射矛盾：对偶 @@M@@\Gamma@@ 的价格精确为 @@M@@dw@@，而其 @@M@@+1@@ 特征空间既是稀疏对称阵的核又是可逆阵的图像，上下夹逼得 @@M@@dw-O(w)\le p(R)\le\frac{3d}{4}w+O(w)@@，@@M@@d@@ 大时不相容。上界依赖”每个稠密对至多 @@M@@3/2@@“的计费与反馈修正可忽略；下界依赖”可逆角块不贵于宿主矩阵”。任一环节失手，矛盾消失，盈余存在性悬空。
问 2：为什么要求 @@M@@A@@ 非单项、单项映射又要免费？去掉会怎样？
答：单项 @@M@@A@@ 的张量幂仍是单项的，本就可用换线免费实现，谈不上盈余。免费单项映射只是矩阵词层面的中间记账约定：落成电路后每次标量乘法照计费，靠正生成引理的固定模式把单项因子吸收进调用槽。若在词层面就禁止单项映射，盈余可能根本不出现。
问 3：与已有工作相比真正的新意是什么？
答：Morgenstern、Ailon 的 @@M@@\Omega(n\log n)@@ 都带系数有界或酉门限制；Alman–Rao 只改 2 的幂长度的常数；Alman–Li 研究的是深度二秩一分解的另一度量。本文首次在最一般的非均匀复线性电路里推翻该下界。
问 4：非均匀、系数生成不计费——这不是在”作弊”吗？
答：这是明码标价的模型选择：定理正是关于这个最宽松模型的存在性陈述，结论不涉及数值稳定性、比特复杂度或有界系数电路（定理 1.1 后说明）。姊妹篇则在计费更苛刻的均匀模型里补上全长度算法。
问 5：AI 生成证明最可能出错的模式？
答：价格函数由紧性与分离论证抽象而来，链条极长（打包、反馈、特化、枢轴、反射五级），最危险的是隐性循环论证或”特化把精确电路换成极限”的越界——论文专门声明从未如此。主结果已 Lean 形式化，风险主要残留在散文表述与模型解读。
问 6：谁会用到它？
答：算术复杂度方向直接受益：任何未来的傅里叶下界必须先限制模型；张量放大与”恰好 @@M@@r@@ 坐标”编译器也是可复用的部件，姊妹篇的证书接口即由本文的存在性保证兜底。
总评
它把”傅里叶变换天然要 @@M@@n\log n@@“的信念在最一般模型中干净利落地否定掉，且经形式化，概念分量极重；最大风险在于结论的适用面常被误读——非均匀、存在性、系数不计费，三点缺一不可。