Sra's six-matrix trace inequality (Δ₆ > 0)
MathOverflow 263833 (S. Sra, 2017) · arXiv:2608.29595, Problem 8.1 and Appendix E
Six explicit rational 3×3 positive definite matrices give Δ₆ ≈ −99.97 < 0, so the six-matrix trace consequence of Sra's quantum coupon collector conjecture fails. The underlying conjecture was already refuted by Sra, and this failure follows from his Theorem 8.4 by a short argument.
Verification: Lean, kernel-checked; standard axioms only. Lean 4.35.0 with Mathlib v4.35.0; all 18 audited declarations depend only on propext, Classical.choice, and Quot.sound, and the proof is replayed by Lean's kernel checker and the independent nanoda checker.
Prior work: Earlier refutations are known; see the entry.