临界混合算术四点半平面HRT定理
The critical mixed-arithmetic four-point HRT theorem
浏览论文内容
中文总结 AI 辅助
本文解决了四个时频平移的临界混合算术HRT定理，证明在特定维度条件下四点函数线性无关，并用Lean 4完成了端到端形式化验证。
中文摘要 AI 辅助
尽管Heil--Ramanathan--Topiwala猜想在完全一般性下是假的，但其失败使得正几何与算术区域的分类更加紧迫。我们解决了四个时频平移的临界混合算术区域。对于\\(z=(x,ω)\\)和\\(w=(y,η)\\)，设\\(σ(z,w)=xη-yω\\)。令\\(u,v\in\R^2\\)满足\\(\lvertσ(u,v)\rvert=1\\)，记\\(ν=αu+βv\\)，并假设\\(0,u,v,ν\\)互不相同。若\\(\dim_{\Q}\operatorname{span}_{\Q}\{1,α,β\}=2\\)，则对于每个非零\\(f\in L^2(\R)\\)，向量\\(f,π(u)f,π(v)f,π(ν)f\\)线性无关。这包括了Chris Heil猜想9.2中的两种四点构型。证明首先将假定的线性相关转化为无理旋转上的标量上循环。在正测度的无零点纤维族上，绕数和连分数返回迫使周期和乐群为常数。然而返回乘子为Laurent多项式，因此其未规范化的和乐群是代数的；常数和乐群定律同时使其成为无理特征。这些结论不相容。主定理及其完整的正式依赖链已在Lean 4中端到端完全认证，包括物理全非零情形、完整的三点HRT定理、系数约简步骤以及最终的四点结论。随附的Lean 4认证档案包含可复现的源代码、固定构建说明和传递公理审计。
英文摘要
Although the Heil--Ramanathan--Topiwala conjecture is false in full generality, its failure makes the classification of positive geometric and arithmetic regimes more urgent. We settle the critical mixed-arithmetic regime for four time-frequency shifts. For \(z=(x,ω)\) and \(w=(y,η)\), set \(σ(z,w)=xη-yω\). Let \(u,v\in\R^2\) satisfy \(\lvertσ(u,v)\rvert=1\), write \(ν=αu+βv\), and assume that \(0,u,v,ν\) are distinct. If \(\dim_{\Q}\operatorname{span}_{\Q}\{1,α,β\}=2\) then, for every nonzero \(f\in L^2(\R)\), the vectors \(f,π(u)f,π(v)f,π(ν)f\) are linearly independent. This includes both four-point configurations in Chris Heil's Conjecture~9.2. The proof first converts a putative dependence into a scalar cocycle over an irrational rotation. On a positive-measure family of zero-free fibres, winding and continued-fraction returns force the periodic holonomy to be constant. The return multiplier is Laurent polynomial, however, so its ungauged holonomy is algebraic; the constant-holonomy law simultaneously makes it an irrational character. These conclusions are incompatible. The principal theorem and its complete formal dependency chain have been fully certified end-to-end in Lean~4, including the physical all-nonzero case, the complete three-point HRT theorem, the coefficient-reduction step, and the final four-point conclusion. The accompanying \href{https://www.dropbox.com/scl/fi/jd9xeqqera147wdc82r8k/3f260460-07d5-45f5-8d1c-ee1d2879c0af-aristotle-32-.tar.gz?rlkey=a24njadfds5ty9ez473lk03lv\&e=1\&dl=0} {Lean~4 certification archive} contains reproducible source, pinned build instructions, and transitive axiom audits.
发表机构
- Bridgewater State University（布里奇沃特州立大学）
机构由 AI 辅助整理，请以论文原文为准。
