An independent proof of the even-dimensional S-matrix inequality

Abstract

Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix $A\in {\mathbb{R}}^{n\times n}$ satisfies $\Vert A^{-1}{\Vert }_F\ge 2n(n+1{)}^{-1}\Vert A{\Vert }_{\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\ge 66$; a finite exact calculation handles $4\le n\le 64$, $n\ne 6$; 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.

arXiv comment24 pages. Revised title and positioning; added Zhang citation; clarified error estimates and boundary cases. Main theorem unchanged. Lean 4 formalization and exact-rational Python certificate included as ancillary files