A $(\log n)^{1/4}$ Bound for the Komlós Problem
Eren Ercan
math.CO
Sep 8, 2026 · v1
cs.DM cs.DS
TL;DR
Formalizes the partial- and full-colouring discrepancy theorems in Lean, including the finite trajectory, exact threshold sum, and final rounding.
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.
Problem
The Komlós conjecture asks whether the combinatorial discrepancy of a matrix with unit-norm columns is bounded by an absolute constant. Prior bounds by Bansal and Jiang gave O((log n)^{1/4}(log log n)^{7/4}).
Approach
Building on Bansal and Jiang's affine spectral independence framework, the work constructs a finite trajectory of partial colourings with a class schedule of summable row thresholds and a covariance budget controlled via historical exponential sums. The fourth root arises from balancing the logarithmic decrease in alive dimension against the fourth power of row thresholds. An exact threshold-sum certificate yields the explicit constant, and rounding at most eight fractional coordinates costs 2√2. The partial- and full-colouring theorems are formalized in Lean, with Bansal–Jiang Theorem A.4 as the sole external assumption.
Results
The discrepancy is bounded by 2395(1+log_+(n/9))^{1/4}+2√2, removing the (log log n)^{7/4} factor from the previous bound. Prescribed-depth partial colourings and completions from arbitrary starting points are also obtained.
