Komlós conjecture

DefinitionSigns indexed by two elements#✓fully proved

For \(s \in \{0, 1\}\), the associated real sign is \(-1\) if \(s = 0\) and \(1\) if \(s = 1\).

def signValue (s : Fin 2) : ℝ := if s = 0 then -1 else 1

Used by 2

Used byDiscrepancy of a real matrix · The discrepancy is attained

DefinitionDiscrepancy of a real matrix#✓fully proved

For a real \(m \times n\) matrix \(A\), the discrepancy of \(A\) is the infimum, over all sign vectors \(x \in \{-1, 1\}^n\), of the maximum norm \(\|Ax\|_\infty = \max_i |(Ax)_i|\) (which is \(0\) when \(m = 0\)), taken in \([0, \infty]\).

def discrepancy (A : Matrix (Fin m) (Fin n) ℝ) : ENNReal :=
  ⨅ x : Fin n → Fin 2, ENNReal.ofReal ‖A.mulVec (fun j => signValue (x j))‖

Uses 1 · Used by 2

Statement usesSigns indexed by two elements

Used byKomlós constant in a fixed dimension · The discrepancy is attained

DefinitionMatrices with columns in the unit ball#✓fully proved

A real \(m \times n\) matrix \(A\) is column admissible when every column of \(A\) lies in the closed Euclidean unit ball, that is, \(\sum_{i=1}^{m} A_{ij}^2 \le 1\) for every column index \(j\).

def ColumnAdmissible (A : Matrix (Fin m) (Fin n) ℝ) : Prop :=
  ∀ j, ∑ i, (A i j) ^ 2 ≤ 1

Used by 3

Used byKomlós constant in a fixed dimension · Komlós conjecture for vector colorings (statement) · Statement of Nikolov's bound on vector discrepancy

DefinitionKomlós constant in a fixed dimension#✓fully proved

For a natural number \(n\), this is the supremum of the discrepancy of \(A\) over all real \(n \times n\) matrices \(A\) whose columns all have Euclidean norm at most \(1\), taken in \([0, \infty]\). The definition also applies to \(n = 0\).

def dimensionConstant (n : ℕ) : ENNReal :=
  ⨆ A : {A : Matrix (Fin n) (Fin n) ℝ // ColumnAdmissible A}, discrepancy A.1

Uses 2 · Used by 8

Statement usesMatrices with columns in the unit ball · Discrepancy of a real matrix

Used byStatement of the sublogarithmic Komlós bound · Statement of Banaszczyk's Komlós bound · Statement of the little-o square-root-log Komlós bound · Statement of the Bansal–Jiang Komlós bound · Statement of the Bansal–Dadush–Garg Komlós bound · Beck–Spencer–Gluskin logarithmic upper bound (statement) · Komlós constant · Infinitely many dimensions with Komlós constant at least \(1 + \sqrt{2}\) (statement)

DefinitionKomlós constant#✓fully proved

The Komlós constant is the supremum, over all integers \(n \ge 1\), of the Komlós constant in dimension \(n\), namely the supremum of the discrepancy of \(A\) over all real \(n \times n\) matrices \(A\) whose columns all have Euclidean norm at most \(1\). It is taken in \([0, \infty]\).

def komlosConstant : ENNReal :=
  ⨆ n : {n : ℕ // 1 ≤ n}, dimensionConstant n.1

Uses 1 · Used by 2

Statement usesKomlós constant in a fixed dimension

Used byEquivalence of the square and rectangular Komlós formulations (statement) · Kunisky's lower bound for the Komlós constant (statement)

TheoremThe discrepancy is attained#✓fully proved

For every real \(m \times n\) matrix \(A\), including the cases \(m = 0\) and \(n = 0\), there is a sign vector \(x \in \{-1, 1\}^n\) such that the discrepancy of \(A\) equals \(\|Ax\|_\infty\).

theorem discrepancy_attained (A : Matrix (Fin m) (Fin n) ℝ) :
    ∃ x : Fin n → Fin 2,
      discrepancy A = ENNReal.ofReal ‖A.mulVec (fun j => signValue (x j))‖

Uses 2

Statement usesDiscrepancy of a real matrix · Signs indexed by two elements

DefinitionUniform discrepancy bound for vectors in the unit ball#✓fully proved

The statement that there is a real constant \(C > 0\) such that for all natural numbers \(n\) and \(d\) and all vectors \(v_1, \dots, v_n \in \mathbb{R}^d\) of Euclidean norm at most \(1\), writing \(v_{ij}\) for the \(j\)-th coordinate of \(v_i\), there are signs \(\varepsilon_1, \dots, \varepsilon_n \in \{-1, 1\}\) with \(\left|\sum_{i=1}^{n} \varepsilon_i v_{ij}\right| \le C\) for every coordinate index \(j\).

def UniformRectangularBound : Prop :=
  ∃ C : ℝ, 0 < C ∧
    ∀ (n d : ℕ) (v : Fin n → Fin d → ℝ),
      (∀ i, ∑ j, (v i j) ^ 2 ≤ 1) →
        ∃ epsilon : Fin n → ℝ,
          (∀ i, epsilon i = 1 ∨ epsilon i = -1) ∧
          ∀ j, |∑ i, epsilon i * v i j| ≤ C

Used by 1

Used byEquivalence of the square and rectangular Komlós formulations (statement)

DefinitionEquivalence of the square and rectangular Komlós formulations (statement)#✓fully proved

The statement that the uniform discrepancy bound for vectors in the unit ball holds if and only if the Komlós constant is finite.

def constantFormulationEquivalence : Prop :=
  UniformRectangularBound ↔ komlosConstant < ⊤

Sources

• optimization catalogue C24a, line 26, and AIM Problem 1.05. The padding bridge is requested, not assumed or claimed definitional.

Uses 2 · Used by 1

Statement usesUniform discrepancy bound for vectors in the unit ball · Komlós constant

Used byThe square and rectangular Komlós formulations are equivalent

DefinitionBeck–Spencer–Gluskin logarithmic upper bound (statement)#✓fully proved

The statement that there are a real number \(c > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c \log n\), where \(\log\) is the natural logarithm.

def beckSpencerGluskinLogUpperBound : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
    dimensionConstant n ≤ ENNReal.ofReal (c * Real.log n)

Sources

• optimization catalogue C24a, line 35, Beck (1981), Spencer (1985), and Gluskin (1989); their full original theorem texts remain a primary-source gap.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used byBeck–Spencer–Gluskin logarithmic upper bound for the Komlós constant

DefinitionStatement of Banaszczyk's Komlós bound#✓fully proved

The proposition that there are a real constant \(c > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c \sqrt{\log n}\), where \(\log\) is the natural logarithm.

def banaszczyk1998SqrtLogUpperBound : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
    dimensionConstant n ≤ ENNReal.ofReal (c * Real.sqrt (Real.log n))

Sources

• optimization catalogue C24a, line 36, Banaszczyk (1998), also reported in retained BJ2025 introduction and BDG2019 Theorem komlos.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used byBanaszczyk's bound for the Komlós problem

DefinitionStatement of the sublogarithmic Komlós bound#✓fully proved

The proposition that for every real \(\varepsilon > 0\) there is a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(\varepsilon \log n\), where \(\log\) is the natural logarithm. In other words, the Komlós constant in dimension \(n\) is \(o(\log n)\).

def banaszczykSublogUpperBound : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
    dimensionConstant n ≤ ENNReal.ofReal (ε * Real.log n)

Sources

• optimization catalogue C24a, line 36, the o(log n) comment.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used bySublogarithmic bound for the Komlós problem

DefinitionStatement of the Bansal–Dadush–Garg Komlós bound#✓fully proved

The proposition that there are a real constant \(c > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c \sqrt{\log n}\), where \(\log\) is the natural logarithm.

Only this numerical bound is stated, not the polynomial-time algorithm of the source.

def bdg2019NumericalSqrtLogUpperBound : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
    dimensionConstant n ≤ ENNReal.ofReal (c * Real.sqrt (Real.log n))

Sources

• Bansal, Dadush, and Garg, arXiv1605.02882, retained introduction lines 52-60, Theorem komlos; efficient randomized/high-probability computation is an explicit separate gap.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used byBansal–Dadush–Garg bound for the Komlós problem, numerical form

DefinitionStatement of the Bansal–Jiang Komlós bound#✓fully proved

The proposition that there are a real constant \(c > 0\), a natural number \(p\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c (\log n)^{1/4} (\log \log n)^p\), where \(\log\) is the natural logarithm.

def bansalJiang2025QuarterLogUpperBound : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∃ p : ℕ, ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
    dimensionConstant n ≤ ENNReal.ofReal
      (c * (Real.log n) ^ (1 / 4 : ℝ) * (Real.log (Real.log n)) ^ p)

Sources

• Bansal and Haotian Jiang, arXiv2508.03961, retained abstract lines 1-9 and introduction Theorem thm:Komlos. The abstract explicitly defines tilde as poly(log log n); no degree is invented.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used byBansal–Jiang bound for the Komlós problem

DefinitionStatement of the little-o square-root-log Komlós bound#✓fully proved

The proposition that for every real \(\varepsilon > 0\) there is a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(\varepsilon \sqrt{\log n}\), where \(\log\) is the natural logarithm. In other words, the Komlós constant in dimension \(n\) is \(o(\sqrt{\log n})\).

def bansalJiang2025LittleSqrtLogUpperBound : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, 3 ≤ N ∧ ∀ n : ℕ, N ≤ n →
    dimensionConstant n ≤ ENNReal.ofReal (ε * Real.sqrt (Real.log n))

Sources

• optimization catalogue C24a, line 38, and BJ2025's retained abstract.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used byBansal–Jiang improvement on Banaszczyk's Komlós bound

DefinitionKunisky's lower bound for the Komlós constant (statement)#✓fully proved

The statement that the Komlós constant is at least \(1 + \sqrt{2}\).

The bound concerns the supremum over all dimensions; it does not assert that any single dimension attains \(1 + \sqrt{2}\).

def kunisky2023LowerBound : Prop :=
  ENNReal.ofReal (1 + Real.sqrt 2) ≤ komlosConstant

Sources

• optimization catalogue C24a, line 45, and retained Kunisky arXiv2111.02974v1, Theorem 1.1.

Uses 1 · Used by 1

Statement usesKomlós constant

Used byKunisky's lower bound for the Komlós constant

DefinitionInfinitely many dimensions with Komlós constant at least \(1 + \sqrt{2}\) (statement)#✓fully proved

The statement that there are infinitely many natural numbers \(n \ge 1\) such that the Komlós constant in dimension \(n\) is at least \(1 + \sqrt{2}\).

def kuniskyInfinitelyManyDimensionsLowerBound : Prop :=
  {n : ℕ | 1 ≤ n ∧ ENNReal.ofReal (1 + Real.sqrt 2) ≤ dimensionConstant n}.Infinite

Sources

• optimization catalogue C24a, line 53. Retained Kunisky v1 only gives a sequence approaching the endpoint from below; the journal2023 comparison is unresolved. This request does not certify exact finite attainment.

Uses 1 · Used by 1

Statement usesKomlós constant in a fixed dimension

Used byInfinitely many dimensions have Komlós constant at least \(1 + \sqrt{2}\)

DefinitionKomlós conjecture for vector colorings (statement)#✓fully proved

The statement that for all natural numbers \(m\) and \(n \ge 1\) and every real \(m \times n\) matrix \(A\) whose columns all lie in the closed Euclidean unit ball, there are unit vectors \(u_1, \dots, u_n\) in the Euclidean space \(\mathbb{R}^n\) such that \(\lVert \sum_{j=1}^{n} A_{ij} u_j \rVert \le 1\) for every row index \(i\), where \(\lVert \cdot \rVert\) is the Euclidean norm.

def nikolov2013VectorColoringBound : Prop :=
  ∀ (m n : ℕ), 1 ≤ n → ∀ A : Matrix (Fin m) (Fin n) ℝ, ColumnAdmissible A →
    ∃ u : Fin n → EuclideanSpace ℝ (Fin n), (∀ j, ‖u j‖ = 1) ∧
      ∀ i, ‖∑ j, A i j • u j‖ ≤ 1

Sources

• Nikolov, arXiv1301.4039, retained KomlosSDP.tex lines 115-139, Theorem thm:main. Positive column dimension is explicit.

Uses 1 · Used by 1

Statement usesMatrices with columns in the unit ball

Used byNikolov's theorem: the Komlós conjecture holds for vector colorings

DefinitionStatement of Nikolov's bound on vector discrepancy#✓fully proved

This is the proposition that for all natural numbers \(m\) and \(n\) with \(n \ge 1\) and every real \(m \times n\) matrix \(A\) whose columns all lie in the closed Euclidean unit ball, that is, \(\sum_{i} A_{ij}^2 \le 1\) for every column \(j\), the vector discrepancy of \(A\) is at most \(1\).

This bounds the unit-vector relaxation, not the discrepancy over sign vectors.

def nikolov2013VectorDiscrepancyUpperBound : Prop :=
  ∀ (m n : ℕ), 1 ≤ n → ∀ A : Matrix (Fin m) (Fin n) ℝ, ColumnAdmissible A →
    vectorDiscrepancy A ≤ 1

Sources

• Nikolov, arXiv1301.4039, retained KomlosSDP.tex, Theorem thm:main, and optimization catalogue C24a, line 55.

Uses 2 · Used by 1

Statement usesMatrices with columns in the unit ball · Vector discrepancy

Used byNikolov's bound on vector discrepancy

TheoremThe square and rectangular Komlós formulations are equivalent#●ready to prove

The following two conditions are equivalent. (a) There is a real constant \(C > 0\) such that for all natural numbers \(n\) and \(d\) and all vectors \(v_1, \dots, v_n \in \mathbb{R}^d\) of Euclidean norm at most \(1\), writing \(v_{ij}\) for the \(j\)-th coordinate of \(v_i\), there are signs \(\varepsilon_1, \dots, \varepsilon_n \in \{-1, 1\}\) with \(\left|\sum_{i=1}^{n} \varepsilon_i v_{ij}\right| \le C\) for every coordinate index \(j\). (b) The Komlós constant, the supremum over all \(n \ge 1\) of the discrepancy of real \(n \times n\) matrices whose columns all have Euclidean norm at most \(1\), is finite.

theorem_wanted constantFormulationEquivalence_holds : constantFormulationEquivalence

Sources

• optimization catalogue C24a, line 26, and AIM Problem 1.05.

Uses 1

Statement usesEquivalence of the square and rectangular Komlós formulations (statement)

TheoremBeck–Spencer–Gluskin logarithmic upper bound for the Komlós constant#●ready to prove

There are a real number \(c > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) (the supremum of the discrepancy of real \(n \times n\) matrices whose columns all have Euclidean norm at most \(1\), taken in \([0, \infty]\)) is at most \(c \log n\), where \(\log\) is the natural logarithm.

theorem_wanted beckSpencerGluskinLogUpperBound_holds : beckSpencerGluskinLogUpperBound

Sources

• optimization catalogue C24a, line 35, Beck, Spencer, and Gluskin.

Uses 1

Statement usesBeck–Spencer–Gluskin logarithmic upper bound (statement)

TheoremBanaszczyk's bound for the Komlós problem#●ready to prove

There are a real constant \(c > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c \sqrt{\log n}\), where \(\log\) is the natural logarithm.

theorem_wanted banaszczyk1998SqrtLogUpperBound_holds : banaszczyk1998SqrtLogUpperBound

Sources

• optimization catalogue C24a, line 36, Banaszczyk (1998).

Uses 1

Statement usesStatement of Banaszczyk's Komlós bound

TheoremSublogarithmic bound for the Komlós problem#●ready to prove

For every real \(\varepsilon > 0\) there is a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(\varepsilon \log n\), where \(\log\) is the natural logarithm. In other words, the Komlós constant in dimension \(n\) is \(o(\log n)\).

theorem_wanted banaszczykSublogUpperBound_holds : banaszczykSublogUpperBound

Sources

• optimization catalogue C24a, line 36, its sublogarithmic comment.

Uses 1

Statement usesStatement of the sublogarithmic Komlós bound

TheoremBansal–Dadush–Garg bound for the Komlós problem, numerical form#●ready to prove

There are a real constant \(c > 0\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c \sqrt{\log n}\), where \(\log\) is the natural logarithm.

theorem_wanted bdg2019NumericalSqrtLogUpperBound_holds : bdg2019NumericalSqrtLogUpperBound

Sources

• BDG2019, arXiv1605.02882, retained Theorem komlos.

Uses 1

Statement usesStatement of the Bansal–Dadush–Garg Komlós bound

TheoremBansal–Jiang bound for the Komlós problem#●ready to prove

There are a real constant \(c > 0\), a natural number \(p\) and a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(c (\log n)^{1/4} (\log \log n)^p\), where \(\log\) is the natural logarithm.

theorem_wanted bansalJiang2025QuarterLogUpperBound_holds : bansalJiang2025QuarterLogUpperBound

Sources

• BJ2025, arXiv2508.03961, abstract and Theorem thm:Komlos.

Uses 1

Statement usesStatement of the Bansal–Jiang Komlós bound

TheoremBansal–Jiang improvement on Banaszczyk's Komlós bound#●ready to prove

For every real \(\varepsilon > 0\) there is a natural number \(N \ge 3\) such that for every natural number \(n \ge N\), the Komlós constant in dimension \(n\) is at most \(\varepsilon \sqrt{\log n}\), where \(\log\) is the natural logarithm. In other words, the Komlós constant in dimension \(n\) is \(o(\sqrt{\log n})\).

theorem_wanted bansalJiang2025LittleSqrtLogUpperBound_holds :
  bansalJiang2025LittleSqrtLogUpperBound

Sources

• BJ2025, arXiv2508.03961, the improvement reported in its abstract.

Uses 1

Statement usesStatement of the little-o square-root-log Komlós bound

TheoremKunisky's lower bound for the Komlós constant#●ready to prove

The Komlós constant (the supremum over all \(n \ge 1\) of the discrepancy of real \(n \times n\) matrices whose columns all have Euclidean norm at most \(1\), taken in \([0, \infty]\)) is at least \(1 + \sqrt{2}\).

theorem_wanted kunisky2023LowerBound_holds : kunisky2023LowerBound

Sources

• Kunisky, arXiv2111.02974v1, Theorem 1.1; catalogue C24a, line 45.

Uses 1

Statement usesKunisky's lower bound for the Komlós constant (statement)

TheoremInfinitely many dimensions have Komlós constant at least \(1 + \sqrt{2}\)#●ready to prove

There are infinitely many natural numbers \(n \ge 1\) such that the Komlós constant in dimension \(n\) (the supremum of the discrepancy of real \(n \times n\) matrices whose columns all have Euclidean norm at most \(1\), taken in \([0, \infty]\)) is at least \(1 + \sqrt{2}\).

theorem_wanted kuniskyInfinitelyManyDimensionsLowerBound_holds :
  kuniskyInfinitelyManyDimensionsLowerBound

Sources

• catalogue C24a, line 53, unverified exact finite-endpoint assertion.

Uses 1

Statement usesInfinitely many dimensions with Komlós constant at least \(1 + \sqrt{2}\) (statement)

TheoremNikolov's theorem: the Komlós conjecture holds for vector colorings#●ready to prove

For all natural numbers \(m\) and \(n \ge 1\) and every real \(m \times n\) matrix \(A\) whose columns all have Euclidean norm at most \(1\), there are unit vectors \(u_1, \dots, u_n\) in the Euclidean space \(\mathbb{R}^n\) such that \(\lVert \sum_{j=1}^{n} A_{ij} u_j \rVert \le 1\) for every row index \(i\), where \(\lVert \cdot \rVert\) is the Euclidean norm.

theorem_wanted nikolov2013VectorColoringBound_holds : nikolov2013VectorColoringBound

Sources

• Nikolov, arXiv1301.4039, retained Theorem thm:main.

Uses 1

Statement usesKomlós conjecture for vector colorings (statement)

TheoremNikolov's bound on vector discrepancy#●ready to prove

For all natural numbers \(m\) and \(n\) with \(n \ge 1\) and every real \(m \times n\) matrix \(A\) whose columns all lie in the closed Euclidean unit ball, that is, \(\sum_{i} A_{ij}^2 \le 1\) for every column \(j\), the vector discrepancy of \(A\) is at most \(1\).

theorem_wanted nikolov2013VectorDiscrepancyUpperBound_holds :
  nikolov2013VectorDiscrepancyUpperBound

Sources

• Nikolov, arXiv1301.4039, retained Theorem thm:main; catalogue line 55.

Uses 1

Statement usesStatement of Nikolov's bound on vector discrepancy

18 fully proved11 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.