The S-matrix conjecture

Harwit and Sloane conjectured that every nonsingular entrywise nonnegative matrix A of order n satisfies ||A⁻¹||_F >= (2n/(n+1)) ||A||_max^(-1), with equality precisely for positive multiples of S-matrices. Cheng proved the conjecture in odd dimensions, and Frankel and Urschel proved it for all n >= 1000. 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 >= 66; a finite exact calculation handles 4 <= n <= 64, n != 6; 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.