S矩阵猜想
An independent proof of the even-dimensional S-matrix inequality
浏览论文内容
中文总结 AI 辅助
该研究完成了S矩阵猜想所有偶数维情形的证明，结合已有奇数维结果，在所有维度证明了该猜想，且偶数维证明已在Lean 4中形式化。
中文摘要 AI 辅助
Harwit和Sloane猜想，每个非奇异元素非负矩阵$A\in\mathbb R^{n\times n}$满足$\\|A^{-1}\\|_F\ge 2n(n+1)^{-1}\\|A\\|_{\max}^{-1}$，等式仅在S矩阵的正倍数时成立。Cheng证明了奇数维的该猜想，Frankel和Urschel证明了$n\ge1000$时的偶数维情形，我们完成了剩余偶数维情形的证明。我们从Frankel-Urschel引理2.1中的结构恒等式出发，推导得到精确的全局缺陷预算，结合二进制舍入与Gram投影，用改进的十行障碍处理所有偶数$n\ge66$，用有限精确计算处理$4\le n\le64$且$n\neq6$，用单独的多列能量论证处理$n=6$，二阶情形由直接计算得出。该新偶数维证明已在Lean 4中形式化，仅以Frankel-Urschel引理2.1作为外部数学输入。结合Cheng的奇数维定理，该猜想在所有维度均得证。
英文摘要
Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix $A\in\mathbb R^{n\times n}$ satisfies $\|A^{-1}\|_F\ge 2n(n+1)^{-1}\|A\|_{\max}^{-1}$, with equality precisely for positive multiples of $S$-matrices. Zhang has given a complete proof of this conjecture by a centered pseudoinverse and spectral variance method. We present an independently obtained, structurally different proof of the strict even-dimensional inequality. Starting from the structural identities of Frankel and Urschel, we derive an exact global defect budget and combine binary rounding, fixed intersections, and Gram projection. A ten-row obstruction handles every even $n\ge66$; a finite exact calculation handles $4\le n\le64$, $n\ne6$; and a multi-column energy argument treats $n=6$. The order-two case is elementary. The even-dimensional argument is formalized in Lean 4, conditional on Frankel--Urschel Lemma 2.1 as an explicit external mathematical input. The finite evaluations use Lean's native evaluator; their trust boundary and exact certificates are documented. Together with Cheng's odd-dimensional theorem, the argument recovers the full S-matrix theorem and its equality characterization.
