Kunisky: the Komlós constant is at least $1+\sqrt{2}$

Theorem komlos_lower_bound. For every real number $K$, if $K$ has the following property — call it the "Komlós bound property" — then $1 + \sqrt{2} \le K$.

The Komlós bound property of $K$ (the hypothesis, unfolded) asserts: for every pair of natural numbers $n$ and $m$ (including $n = 0$ and $m = 0$) and every family of vectors $v_1, \dots, v_n \in \mathbb{R}^m$, where $\mathbb{R}^m$ carries the Euclidean ($\ell^2$) norm, such that

there exists a function $\varepsilon$ assigning to each index $i \in \{1, \dots, n\}$ a real number $\varepsilon_i$ with $\varepsilon_i = 1$ or $\varepsilon_i = -1$, such that for every coordinate $j \in \{1, \dots, m\}$,

where $v_i(j)$ denotes the $j$-th coordinate of $v_i$. In other words, the signed sum $\sum_i \varepsilon_i v_i$ has $\ell^\infty$ norm at most $K$, and this must hold uniformly over all dimensions $m$ and all family sizes $n$.

The theorem's conclusion is the non-strict inequality $1 + \sqrt{2} \le K$ (approximately $2.414 \le K$).

Remarks on what the quantifiers silently include: the hypothesis quantifies over $n = 0$ (the empty family, for which the sum is $0$ and the coordinate bound forces $|0| \le K$ whenever $m \ge 1$, so any $K$ with the property is automatically $\ge 0$) and over $m = 0$ (where the coordinate condition is vacuous). The theorem is an implication, not an equivalence: it says nothing about whether any $K$ actually has the property, and if no real number had the property the statement would hold vacuously. The sign condition is stated for real-valued $\varepsilon_i$ constrained to the two values $\pm 1$; the vector norm in the hypothesis is the Euclidean $\ell^2$ norm, while the bound on the signed sum is coordinatewise ($\ell^\infty$).