Konyagin's theorem: a triangle-free unit vector system sums to
OpenKonyaginUnitVectors.sum_norm_le_of_triangle_freeThere is an absolute constant such that for any system of unit vectors in a Euclidean space, of which among any three some two are orthogonal, the norm of the sum is at most .
The hypothesis says exactly that the non-orthogonality graph, joining to when , is triangle-free. It is written here as a condition on triples so that the statement needs no definition item; in Mathlib's vocabulary it is SimpleGraph.CliqueFree 3.
The constant is quantified outside everything, so it depends neither on the dimension nor on .
The attribution is worth stating carefully, because it is commonly given wrong in both halves. Lovasz posed the problem; Konyagin proved the bound.
import Mathlib open scoped RealInnerProductSpace
namespace KonyaginUnitVectors
theorem sum_norm_le_of_triangle_free :
∃ C : ℝ, 0 < C ∧ ∀ (d n : ℕ) (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) →
‖∑ i, u i‖ ≤ C * (n : ℝ) ^ ((2 : ℝ) / 3) := by sorry
end KonyaginUnitVectors
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, with the following property. For every dimension d, every count n, and every indexed family u(0), ..., u(n-1) of vectors in d-dimensional real Euclidean space: if each u(i) has norm exactly 1, and if for every three pairwise distinct indices i, j, k at least one of the three real inner products of u i with u j, u j with u k, u i with u k equals 0, then the norm of the sum of all n vectors is at most C times n raised to the real power 2/3. The second hypothesis says exactly that the graph on the index set {0, ..., n-1} joining i to j when the inner product of u i and u j is nonzero has no triangle. The family is indexed, not a set, so repeats are allowed, but no value can occur three times, since three equal unit vectors give three inner products equal to 1. The exponent is 2/3 exactly and the constant is existential, not exhibited. The proof body is sorry, so nothing is established here.
QUANTIFIER ORDER C : real, outermost, so independent of d, n and u. d : natural, dimension of the ambient space, unbounded and unrelated to n. n : natural, number of vectors. u : a function from the n indices into d-dimensional Euclidean space over the reals. Then two hypotheses, then the conclusion.
HYPOTHESES 0 < C: rules out a nonpositive constant; any positive witness suffices, and the conjunct is inside the existential. Unit norms: each vector has norm exactly 1, ruling out the zero vector and any scaling freedom. Triangle-free condition: applies only to triples of pairwise distinct indices, so it says nothing about a pair, and nothing about i = j. Symmetry of the real inner product means the three disjuncts cover all three pairs of the triple. The space is EuclideanSpace R (Fin d), finite-dimensional real with the standard inner product, so no conjugation is involved.
DEGENERATE CASES n = 0: empty sum, norm 0, and 0 raised to 2/3 is 0 under the real power convention, so the claim reads 0 <= 0 and holds. n = 1 and n = 2: the triple hypothesis is vacuous, and the claim forces C times 2^(2/3) to be at least 2, so C is at least 2^(1/3). This is a constraint on the witness only. d = 0: the space is trivial, every vector has norm 0, so the unit-norm hypothesis is unsatisfiable for n greater than 0; those instances are vacuous. d = 1: unit vectors are plus or minus 1, all pairs non-orthogonal, so the triangle-free hypothesis is unsatisfiable for n at least 3. The statement as a whole is not vacuous: instances with d large and n large do satisfy both hypotheses.
UNREADABLE nothing.