发表机构
State Key Laboratory of Mathematical Sciences, Academy of Mathematics and Systems Science, Chinese Academy of Sciences; University of Chinese Academy of Sciences（中国科学院数学与系统科学研究院; 中国科学院大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明零迹矩阵存在维度无关的换位子表示，并构造酉族揭示对角限制下界，用Lean 4形式化验证。
AI 中文摘要
我们证明每个零迹矩阵$A\in M_n(\mathbb{C})$都允许表示$A=BC-CB$，其中$B,C\in M_n(\mathbb{C})$且$\lVert B\rVert\lVert C\rVert\le K\lVert A\rVert$，这里$K$是一个与$n$无关的绝对常数，$\lVert\cdot\rVert$表示算子范数。对于固定的$t>0$，证明根据是否对所有$\theta\in\mathbb{R}$成立$\lVert\operatorname{Re}(e^{\mathrm{i}\theta}A)\rVert_1\ge tn\lVert A\rVert$来分情况处理，其中$\lVert\cdot\rVert_1$表示迹范数。当此下界成立时，我们直接构造换位子表示。否则，Marcus、Spielman和Srivastava的向量选择定理产生较小的零迹压缩，其范数足够小使得归纳法得以闭合。我们还构造了一个显式的零对角Hermitian酉矩阵族，当任一因子被要求在对角基下为对角矩阵时，该族迫使$\lVert B\rVert\lVert C\rVert$具有$\sqrt{\log n}$量级的下界。同一族允许用少于$2\varepsilon^{-2}$个块进行$\varepsilon$-填充，并允许用两个正规因子表示，其最优范数乘积为$1/2$。这确立了无限制换位子界与在指定对角限制下的界之间的区别。主要结果及其关键输入使用Mathlib在Lean 4中形式化。该开发还包括从同一向量选择定理形式化推导Kadison-Singer状态扩展定理。
英文摘要
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.
Comments29 pages
