Sum of Squares and Non Sum of Squares Regimes for the Toeplitz Bottcher Wenzel Form
Wenqi Zhu, Ping Nie
math.NA
Oct 6, 2026 · v1
math.OC
TL;DR
Lean 4 formally verifies sum-of-squares certificates for the Toeplitz Böttcher–Wenzel form for orders 2–20, plus the large-order non-SoS theorem at the explicit threshold.
Abstract
Toeplitz matrices are among the simplest structured models of translation invariance, arising naturally in convolution, stationary covariance models, and discretizations of translation-invariant operators. For a pair of real matrices, the Böttcher–Wenzel form (BW form) is a nonnegative quartic measuring the gap in the corresponding commutator inequality. László conjectured that, when both matrices are Toeplitz, this quartic is a sum of squares for every matrix order. We show that the conjecture is false. More precisely, we identify an explicit family of corner-supported Toeplitz pairs, retaining only the outermost diagonals on the two sides, for which the associated BW form is not a sum of squares at all sufficiently large orders. The proof reduces the complete family of Gram representations to a finite complex test: its Gram-invariant part develops a strictly negative limiting direction, while the remaining Gram-dependent contribution vanishes. We also give an explicit sufficient threshold for the matrix order. The negative result is complemented by two positive regimes. If either Toeplitz factor is symmetric or skew-symmetric, then the corresponding BW form is SoS for every order, with the other factor allowed to be an arbitrary real Toeplitz matrix. For unrestricted Toeplitz pairs, we further prove SoS representability for every $2\le N\le50$, with formal Lean 4 verification through order 20.
Problem
László conjectured that the Böttcher–Wenzel quartic form for pairs of real Toeplitz matrices is a sum of squares (SoS) at every matrix order. The work tests whether Toeplitz structure alone guarantees SoS representability.
Approach
The form is written in wedge coordinates and restricted to corner-supported Toeplitz pairs. The full Gram family is reduced to a normal form using symmetries, and a finite complex test rules out positive semidefiniteness at large orders. Positive regimes come from an orthogonal symmetric/skew-symmetric splitting. Small orders are handled by an exact rational induction with SoS increments, and the certificates and the negative theorem at the explicit threshold are formalized in Lean 4.
Results
The conjecture is false: the form is not SoS for all sufficiently large N, with explicit threshold N0 = 2^9961475. It is SoS at every order when one factor is symmetric or skew-symmetric. Unrestricted pairs are SoS for 2 ≤ N ≤ 50, with Lean 4 verification for N ≤ 20.
| orders | verification |
|---|
| 2 ≤ N ≤ 20 | exact rational verification and Lean 4 |
| 21 ≤ N ≤ 50 | exact rational verification |
Verification coverage for SoS certificates
