Sra's Six-Matrix Trace Inequality — Lean-Checked Counterexample

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.

Priority: An independently constructed counterexample. Sra refuted the underlying conjecture (arXiv:2608.29595, Theorem 8.4). His paper lists this six-matrix trace form as undecided, but its failure follows from Theorem 8.4 by a short congruence argument, given below. No novelty or priority is claimed.

Original problem
Six-matrix trace consequence of Sra's quantum coupon collector conjecture (Δ₆ > 0)
Also known as
quantum coupon collector conjecture, trace form; alternating sum of inverses of sums of positive definite matrices
Identifiers
MathOverflow 263833 (S. Sra, 2017) · arXiv:2608.29595, Problem 8.1 and Appendix E
Source
Suvrit Sra, MathOverflow question 263833 (2017), reproduced as Problem 8.1 of S. Sra, GPT, the Counterexample Machine, arXiv:2608.29595 (2026). The trace quantity Δn and the remark that its sign is undecided for 6 ≤ n ≤ 9 are in Appendix E of that paper.
Result
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.
Repository
https://github.com/cozuya/sra-six-matrix-trace

The claim

For real symmetric positive definite d×d matrices X1, …, Xn, write XS = Σi∈S Xi and

Qn = Σk=1n (−1)k+1 Σ|S|=k XS−1,    Δn = tr Qn = Σ∅≠S⊆[n] (−1)|S|−1 tr XS−1.

Sra's question (MathOverflow 263833; Problem 8.1 of arXiv:2608.29595) asks whether Qn ≻ 0. Positive definiteness implies Δn > 0. The paper proves Δn > 0 for n ≤ 5, gives a counterexample at n = 10, and lists the trace form as undecided for 6 ≤ n ≤ 9. The claim refuted here is the n = 6 trace form: Δ6 > 0 for every dimension d ≥ 1 and all six real symmetric positive definite Xi.

Counterexample

Let E = diag(1/100, 1, 1) and, for t ∈ {−3, −2, −1, 1, 2, 3}, vt = (t², 200, 200t)T and Xt = E + vtvtT. These are six rational 3×3 symmetric positive definite matrices, and

−99.97093178 < Δ6(X−3, …, X3) < −99.97093177.

The exact value is a rational number with a 376-digit numerator and a 374-digit denominator, stated in the Lean source.

Why this falsifies the claim

Each Xt is the sum of a positive definite diagonal matrix and a positive semidefinite rank-one matrix, so it is positive definite, and every subset sum XS is invertible. Evaluating all 63 nonempty-subset terms exactly gives Δ6 < 0, contradicting Δ6 > 0 (and also Δ6 ≥ 0). Since a positive semidefinite matrix has nonnegative trace, the same tuple also shows Q6 is not positive semidefinite; that Loewner-order failure was already established by Sra's Theorem 8.4.

Verification

Formalized in Lean 4.35.0 with Mathlib v4.35.0 using Mathlib's own Matrix, Matrix.PosDef, Matrix.trace, and matrix inverse. The main theorem is SraSixMatrix.six_matrix_trace_positivity_false : ¬ SixMatrixTracePositivity; trace_Q proves Δn = tr Qn for all n and d, and Verification.lean restates the claim using Mathlib definitions only. The exact value is computed by a proved trace-of-inverse formula for 3×3 matrices and norm_num.

Trust model: Lean's kernel and the standard axioms propext, Classical.choice, and Quot.sound, for all 18 audited declarations. The sources contain no sorry, admit, custom axiom, decide, or native_decide. The exported proof is re-checked from an empty environment by Lean's kernel checker and by nanoda, an independent type checker. A separate Python verifier using only exact rational arithmetic recomputes Δ6 by two inversion methods.

Prior art and earlier refutations

  • Sra's Theorem 8.4 (arXiv:2608.29595) gives six rational 3×3 matrices with −96 < vTQ6v < −95, refuting the six-matrix Loewner-order statement. Appendix E gives ten matrices with Δ10 < 0.
  • The six-matrix trace failure follows from Theorem 8.4 by an elementary common-congruence argument: if vTQ6(X)v < 0, then Yi = CXiCT for a suitable invertible C gives tr Q6(Y) < 0. Concretely, tr Q6(Y) = tr(Q6(X)W) with W = C−1C−T, and W = vvT + εI makes it negative. The paper does not state this deduction, and its Appendix E lists 6 ≤ n ≤ 9 as undecided for the trace form; the deduction was made in a prior-art audit for this work on October 16, 2026.
  • The witness here differs from both published tuples. Its only advantages are a compact parameterization and a machine-checked exact value; no minimality is claimed.

Provenance

Chris Ozols, with AI-assisted development and formalization. The counterexample was found during an AI-assisted investigation in October 2026 and first checked by exact rational arithmetic. A prior-art audit on October 16, 2026 concluded that the six-matrix trace failure is a routine consequence of Sra's Theorem 8.4. The Lean formalization, the independent Python verifier, and the repository were produced with Anthropic's Claude on October 27, 2026.