The S-matrix conjecture
Yinjie Li
math.CO
Aug 30, 2026 · v1
TL;DR
The new even-dimensional proof of the S-matrix conjecture is formalized in Lean 4 with Mathlib, using native_decide for finite exact checks.
Abstract
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. Cheng proved the conjecture in odd dimensions, while Frankel and Urschel proved the even-dimensional case for $n\ge1000$. We complete the remaining even-dimensional cases. Starting from the structural identities in Frankel–Urschel Lemma 2.1, we derive an exact global defect budget and combine binary rounding with Gram projection. A refined ten-row obstruction handles every even $n\ge66$; a finite exact calculation handles $4\le n\le64$, $n\ne6$; and a separate multi-column energy argument treats $n=6$. The order-two case follows from a direct calculation. The new even-dimensional proof has been formalized in Lean 4, with Frankel–Urschel Lemma 2.1 as its sole external mathematical input. Together with Cheng's odd-dimensional theorem, this proves the S-matrix conjecture in every dimension.
Problem
Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix satisfies ‖A^{-1}‖_F ≥ 2n(n+1)^{-1}‖A‖_max^{-1}, with equality only for S-matrices. Odd dimensions and even n≥1000 were known; the remaining even cases were open.
Approach
Starting from the Frankel–Urschel structural Lemma 2.1, an exact global defect budget is derived and combined with binary rounding and Gram projection. A ten-row obstruction handles even n≥66, an exact rational finite calculation handles 4≤n≤64 (n≠6), and a multi-column energy argument treats n=6. The even-dimensional proof is formalized in Lean 4.19.0 with Mathlib 4.19.0, conditional only on Lemma 2.1, using rational/integer arithmetic and a native_decide checker with a kernel-checked soundness theorem.
Results
The S-matrix conjecture is proved in every dimension: strict inequality in even orders, equality precisely for positive multiples of S-matrices in odd orders. No floating-point estimate enters the proof; the finite calculation and its link to the matrix argument are verified in Lean.
