An independent proof of the even-dimensional S-matrix inequality
Abstract
Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix A∈ℝn× n satisfies |A−1|F≥ 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≥66; a finite exact calculation handles 4≤ n≤64, n≠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.
Related
- Royen's proof of the Gaussian correlation inequality as a supersymmetric dimensional reduction
- The Ding-Song-Sun inequality for a class of even ferromagnets
- Finite Matrix Rings of Even Size Are Determined by Their Commuting Graphs
- A proof of the Baruah--Gogoi conjecture on sums of odd and even overlined parts
- A Short Proof and Generalization of the Rainbow Cycle Theorem and Improved Bounds for Binary Even-Query LCCs
BibTeX
@misc{li2026independent,
title = {{An independent proof of the even-dimensional S-matrix inequality}},
author = {Yinjie Li},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2608.29750},
eprint = {2608.29750},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.29750},
}
RIS
TY - UNPB
TI - An independent proof of the even-dimensional S-matrix inequality
AU - Yinjie Li
PY - 2026
DA - 2026/10/07
PB - arXiv
DO - 10.48550/arxiv.2608.29750
UR - https://arxiv.org/abs/2608.29750
AB - Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix A∈ℝ^n× n satisfies |A^−1|_F≥ 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≥66; a finite exact calculation handles 4≤ n≤64, n≠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.
ER -