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

Preprint · Yinjie Li

- Archive id: arxiv:2608.29750
- Published: 2026-08-30
- arXiv: https://arxiv.org/abs/2608.29750
- Source URL: https://arxiv.org/abs/2608.29750
- PDF: https://arxiv.org/pdf/2608.29750
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.