An independent proof of the even-dimensional S-matrix inequality
Yinjie Li
math.CO
Aug 30, 2026 · v2
TL;DR
The even-dimensional proof is formalized in Lean 4 with Mathlib, conditional on an external lemma, using native_decide for finite rational-arithmetic 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. 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.
Problem
Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative n×n matrix satisfies ||A^{-1}||_F ≥ 2n/(n+1)·||A||_max^{-1}, with equality exactly for positive multiples of S-matrices. Cheng settled odd n, so the strict inequality for even n remained open.
Approach
Starting from the structural identities of Frankel and Urschel (their Lemma 2.1), the authors derive a global defect budget and combine binary rounding, fixed intersections, and Gram projection. A ten-row obstruction handles even n ≥ 66, and an exact finite rational calculation handles 4 ≤ n ≤ 64 with n ≠ 6. A multi-column energy argument treats n = 6, and n = 2 is elementary. The proof is formalized in Lean 4.19.0 with mathlib, taking Frankel–Urschel Lemma 2.1 as an explicit hypothesis. The finite check has a kernel-checked soundness theorem, and the checker's success is discharged by native_decide.
Results
The strict even-dimensional inequality is proved. Combined with Cheng's odd-dimensional theorem, this recovers the full S-matrix theorem and its equality characterization. The formalization's trust boundary is the unformalized external lemma plus Lean's native evaluator.
