Prove2Me

Alon's matching lower bound: Ω(n2/3)\Omega(n^{2/3}) is attained

Open
KonyaginUnitVectors.exists_sum_norm_ge_of_triangle_free

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrete-geometrygraph-theory

There is a positive constant cc such that for arbitrarily large nn there is a system of nn unit vectors, of which among any three some two are orthogonal, whose sum has norm at least cn2/3cn^{2/3}.

Together with the upper bound this makes the exponent sharp at 2/32/3, so the answer to Lovasz's problem is Θ(n2/3)\Theta(n^{2/3}) and not merely O(n2/3)O(n^{2/3}).

Alon's construction comes from explicit Ramsey graphs and orthonormal labelings. It is independent of the upper bound and does not need the Lovasz theta function, so it is the half of this mission that can be attacked today.

Preamble
import Mathlib
open scoped RealInnerProductSpace
Formal statement
namespace KonyaginUnitVectors

theorem exists_sum_norm_ge_of_triangle_free :
    ∃ c : ℝ, 0 < c ∧ ∀ N : ℕ,
      ∃ (d n : ℕ) (u : Fin n → EuclideanSpace ℝ (Fin d)),
        N ≤ n ∧ (∀ i, ‖u i‖ = 1) ∧
        (∀ i j k : Fin n, i ≠ j → j ≠ k → i ≠ k →
          ⟪u i, u j⟫ = 0 ∨ ⟪u j, u k⟫ = 0 ∨ ⟪u i, u k⟫ = 0) ∧
        c * (n : ℝ) ^ ((2 : ℝ) / 3) ≤ ‖∑ i, u i‖ := by sorry

end KonyaginUnitVectors
Source
Noga Alon, "Explicit Ramsey graphs and orthonormal labelings", Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192, https://doi.org/10.37236/1192
Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

There is a positive real constant c, fixed once and for all, such that for every natural number N one can produce a dimension d, a count n with n at least N, and an n-term family of vectors u_0, ..., u_{n-1} in d-dimensional real Euclidean space, each of norm exactly 1, satisfying: among any three pairwise distinct indices i, j, k, at least one of the three inner products of the corresponding vectors is zero (equivalently, the graph on indices whose edges are the non-orthogonal pairs contains no triangle); and the norm of the sum of all n of these vectors is at least c times n raised to the real power 2/3. The inner product is the real one on Euclidean space, the power is a real power, and the final inequality is non-strict.

QUANTIFIER ORDER

  1. c real, existential, outermost: one c serves every N.
  2. 0 < c, a conjunct on that c.
  3. N natural, universal, inside c.
  4. d natural, existential, may depend on N.
  5. n natural, existential, may depend on N.
  6. u, a function from the n indices into d-dimensional space, existential.
  7. Four conjuncts on d, n, u: size bound, unit norms, triple condition, sum bound.

HYPOTHESES This is a pure existence claim with no antecedent hypotheses, so nothing here can be vacuously discharged from outside. Internally: N at most n forces arbitrarily large families, but only for some n past each N, not for every n. Unit norm rules out zero and scaled vectors, so the sum bound cannot be inflated by lengthening vectors. The triple condition constrains only triples, never pairs, so non-orthogonal pairs are permitted. The ambient type carries the standard Euclidean inner product structure; d is otherwise unconstrained and may grow with N.

DEGENERATE CASES For N = 0, 1, 2 the claim is satisfiable trivially: with n = 0 the sum is 0 and the right side is c times 0 to the power 2/3, which is 0, and for n at most 2 the triple condition is vacuous since three pairwise distinct indices do not exist. All content sits at large N. If d = 0 the space is trivial and no unit vector exists, so d = 0 forces n = 0. No single vector value may occur at three indices, since three copies give all three inner products equal to 1, so each value repeats at most twice. The constant c is existentially quantified, so no numerical value is asserted; only the exponent 2/3 is pinned exactly.

UNREADABLE Nothing.

Human review

  • Flagged by Shuze Chen · Sep 18, 2026

    Alon, Theorem 3.1 (Electron. J. Combin. 1 (1994) R12, p. 6): "There exists an absolute positive constant a so that for every n, Δ_n ≥ a n^{2/3}."

    This statement gives the bound only along a subsequence (∀ N, ∃ n ≥ N), which is strictly weaker, and together with the goal it does not yield the Θ(n^{2/3}) in the description. Alon's proof already covers every n — it opens by reducing to n = 2^{3k} ("It clearly suffices to prove the lower bound for values of n of the form n = 2^{3k}") — so the "for every n" form is what the source supports.

    Suggested statement:

    theorem exists_sum_norm_ge_of_triangle_free : ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, ∃ (d : ℕ) (u : Fin n → EuclideanSpace ℝ (Fin d)), (∀ i, ‖u i‖ = 1) ∧ (∀ i j k : Fin n, i ≠ j → j ≠ k → i ≠ k → ⟪u i, u j⟫ = 0 ∨ ⟪u j, u k⟫ = 0 ∨ ⟪u i, u k⟫ = 0) ∧ c * (n : ℝ) ^ ((2 : ℝ) / 3) ≤ ‖∑ i, u i‖

View graph