A Dimension-Independent Commutator Bound
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 $\lVert B\rVert\lVert C\rVert\le K\lVert A\rVert$, where $K$ is an absolute constant independent of $n$, and $\lVert\cdot\rVert$ denotes the operator norm. For a fixed $t>0$, the proof splits according to whether $\lVert\operatorname{Re}(e^{\mathrm{i}θ}A)\rVert_1\ge tn\lVert A\rVert$ holds for all $θ\in\mathbb{R}$, where $\lVert\cdot\rVert_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 $\lVert B\rVert\lVert C\rVert$ when either factor is required to be diagonal in the prescribed basis. The same family admits $\varepsilon$-pavings with fewer than $2\varepsilon^{-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.