A Dimension-Independent Commutator Bound
Hao Shen, Jiaqi Wang, Lihong Zhi
math.FA
Sep 9, 2026 · v1
TL;DR
Formalizes in Lean 4 with Mathlib the dimension-independent commutator bound, the Kadison–Singer theorem, and related separation estimates.
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 $\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.
Problem
Whether every trace-zero matrix admits a commutator representation A=[B,C] with the norm product ‖B‖‖C‖ bounded by an absolute constant times ‖A‖, independent of dimension n, and whether restricting a factor to be diagonal changes this.
Approach
For fixed t, the proof splits on whether ‖Re(e^{iθ}A)‖₁ ≥ tn‖A‖ holds for all θ; when it holds a commutator representation is built directly. Otherwise the Marcus–Spielman–Srivastava vector-selection theorem yields smaller trace-zero compressions closing an induction. An explicit family of zero-diagonal Hermitian unitaries from skew-Hadamard doubling gives the diagonal-restriction lower bound. The main results and their essential inputs are formalized in Lean 4 using Mathlib.
Results
An absolute constant K works in every dimension for unrestricted factors. The explicit family forces a √(log n)-order lower bound when a factor must be diagonal, while admitting ε-pavings with fewer than 2ε⁻² blocks and normal-factor representations with optimal norm product 1/2. Lean proofs pass the kernel using only propext, Classical.choice, and Quot.sound.
