A Dimension-Independent Commutator Bound

Abstract

We prove that every trace-zero matrix $A\in M_n(\mathbb{C})$ admits a representation $A=BC-CB$ with $B,C\in M_n(\mathbb{C})$ and $\Vert B\Vert \Vert C\Vert \le K\Vert A\Vert$, where $K$ is an absolute constant independent of $n$, and $\Vert \cdot \Vert$ denotes the operator norm. For a fixed $t>0$, the proof splits according to whether $\Vert \mathrm{Re}(e^{\mathrm{i}\theta }A){\Vert }_1\ge tn\Vert A\Vert$ holds for all $\theta \in \mathbb{R}$, where $\Vert \cdot {\Vert }_1$ denotes the trace norm. When this lower bound holds, we construct a commutator representation directly. Otherwise, the vector-selection theorem of Marcus, Spielman, and Srivastava yields smaller trace-zero compressions whose norms are small enough for the induction to close. We also construct an explicit family of zero-diagonal Hermitian unitaries that forces a lower bound of order $\sqrt{\log n}$ for $\Vert B\Vert \Vert C\Vert$ when either factor is required to be diagonal in the prescribed basis. The same family admits $\epsilon$-pavings with fewer than $2{\epsilon }^{-2}$ blocks and representations by two normal factors with optimal norm product $1/2$. This establishes a distinction between unrestricted commutator bounds and bounds under a prescribed diagonal restriction. The main results and their essential inputs are formalized in Lean 4 using Mathlib. The development also includes a formal derivation of the Kadison-Singer state-extension theorem from the same vector-selection theorem.

29 pages