Improved mathematical bound for balancing vectors in matrix problems
A $(\log n)^{1/4}$ Bound for the Komlós Problem
Discrete MathematicsData Structures and Algorithms
Summary
The problem studied involves finding a way to assign signs (like plus or minus) to columns in a matrix so that the overall imbalance, called discrepancy, is kept small. The authors improve upon previous work by tightening a key mathematical bound that measures this discrepancy, making it grow more slowly as the matrix size increases. They use an advanced framework called affine spectral independence and careful mathematical tools to achieve a better estimate. Their result includes precise calculations and computer-verified parts to ensure correctness.
discrepancy theorymatrixEuclidean normaffine spectral independencepartial coloringlogarithmcovarianceroundingLean theorem prover
Authors
Eren Ercan
Abstract
Let $A\in\mathbb{R}^{m\times n}$ have columns of Euclidean norm at most one. We prove that $\operatorname{disc}(A)\le2395\left(1+\log_+\frac n9\right)^{1/4}+2\sqrt2$. Here $\log_+t=\max\{0,\log t\}$. Building on Bansal and Jiang's affine spectral independence framework, we remove the $(\log\log n)^{7/4}$ factor from their bound. The fourth root comes from balancing the logarithmic decrease in the alive dimension against the fourth power of the row thresholds. Historical exponential sums control the covariance budget across size classes with summable thresholds. An exact threshold-sum certificate gives the coefficient $2395$, and rounding at most eight remaining fractional coordinates costs $2\sqrt2$. The finite construction also gives partial colourings from any prescribed starting point and at any prescribed depth, preserving existing signs. We formalize the partial- and full-colouring theorems in Lean, including the finite trajectory, exact threshold sum and final rounding, with Bansal--Jiang Theorem A.4 as the sole external research theorem assumption.