← All papers
First page of A Walk From Free Probability to Matrix Discrepancy III: Higher Rank Kadison-Singer and Spectrally Thin Trees

A Walk From Free Probability to Matrix Discrepancy III: Higher Rank Kadison-Singer and Spectrally Thin Trees

Tarun Kathuria

cs.DS Sep 18, 2026 · v1
The existence proof of the higher-rank Kadison-Singer signing theorem, including the source estimates, was formalized in Lean.
Let $A_1,\ldots,A_N$ be positive semidefinite matrices of rank at most $r$, with $\sum_iA_i=I$ and $\|A_i\|\le\varepsilon$. We prove that the original matrices admit signs with discrepancy $O(\sqrt\varepsilon\log(2r))$, independently of their dimension and number which is a significantly stronger result than what was known existentially. We give a deterministic algorithm with polynomial real-arithmetic work, and a separate existence proof requiring no computational assumptions. This extends our companion paper on rank-one Kadison–Singer discrepancy. A concave matrix power interpolates between the trace source, which pays a factor $r$, and the sandwich source, whose density response is harder to control. We prove that source concavity controls this additional response in the same inverse-Sylvester metric as the optimized spectral potential. As an application, a single spanning tree can be chosen simultaneously $O(\varepsilon\log^2(2s))$-spectrally thin for $s$ positive edge weightings of a common graph, provided every edge has leverage at most $\varepsilon$ in every weighting. The reduction preserves one common selection decision per edge. For incidence matrices with at most $t$ ones in every row and column, the diagonal specialization gives a deterministic walk on fractional colorings with discrepancy $O(\sqrt t\log(2t))$. The local-walk mechanism gives both existence and an efficient construction without using the Lovász local lemma. A Lean formalization of our existence proof has been completed and will be released shortly.

Given positive semidefinite matrices of rank at most r summing to identity with bounded norm, one wants to assign signs to whole matrices (not decomposed pieces) so that the signed sum has small operator norm, generalizing the rank-one Kadison-Singer discrepancy result.

A concave matrix power source interpolates between a trace source and a sandwich source, controlling the density response in an inverse-Sylvester metric. A local-walk mechanism yields both an existence proof and a deterministic polynomial-work algorithm using semidefinite programming to evaluate the potential. The existence proof, including nonlinear source estimates and the endpoint-or-negative-curvature argument, was formalized in Lean under the matrix hypotheses.

Signs exist with discrepancy O(sqrt(epsilon) log(2r)), independent of dimension and count, improving prior existential bounds. Applications include simultaneously spectrally thin spanning trees and deterministic fractional colorings with discrepancy O(sqrt(t) log(2t)).