Komlós 问题的 $(\nlog n)^{1/4}$ 界
A $(\log n)^{1/4}$ Bound for the Komlós Problem
浏览论文内容
中文总结 AI 辅助
针对 Komlós 问题，利用仿射谱独立性框架并平衡阈值，将色散上界改进为 $O((\log n)^{1/4})$，并在 Lean 中形式化证明。
中文摘要 AI 辅助
设 $A\in\mathbb{R}^{m\times n}$ 的列欧几里得范数至多为 1。我们证明 $\operatorname{disc}(A)\le2395\left(1+\log_+\frac n9\right)^{1/4}+2\sqrt2$，其中 $\log_+t=\max\{0,\log t\}$。基于 Bansal 和 Jiang 的仿射谱独立性框架，我们移除了他们界中的 $(\log\log n)^{7/4}$ 因子。四次根源于平衡活维度中的对数减少与行阈值的四次幂。历史指数和以可求和阈值控制各尺寸类别的协方差预算。精确的阈值和证书给出系数 2395，对至多八个剩余分数坐标的舍入花费 $2\sqrt2$。有限构造还从任意指定起点和任意指定深度给出部分着色，并保留已有符号。我们在 Lean 中形式化了部分和完全着色定理，包括有限轨迹、精确阈值和最终舍入，并以 Bansal–Jiang 定理 A.4 作为唯一的外部研究定理假设。
英文摘要
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.
