{"id":"arxiv:2608.29750","kind":"preprint","title":"An independent proof of the even-dimensional S-matrix inequality","authors":["Yinjie Li"],"author_count":1,"year":2026,"published":"2026-08-30","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2608.29750","nct_id":null,"source_url":"https://arxiv.org/abs/2608.29750","archive_url":"https://space-kitty.com/papers/arxiv:2608.29750","updated":"2026-10-07","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2608.29750","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_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["math.CO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}