Read-back: Komlos.komlos_implies_beck_fiala

The theorem is universally quantified over a real number $K$, together with a hypothesis (unfolded below) that $K$ witnesses the "Komlós property", and over natural numbers $t$, $n$, $m$ (each of which may be $0$) and a function $A : \{0,\dots,m-1\} \times \{0,\dots,n-1\} \to \mathbb{R}$, viewed as a real $m \times n$ matrix with rows indexed by $i \in \{0,\dots,m-1\}$ and columns indexed by $j \in \{0,\dots,n-1\}$.

Hypothesis 1 (the Komlós property at constant $K$, unfolded from the custom definition KomlosBound K). For every pair of natural numbers $n', m'$ (independent of the $n, m, t$ of the theorem) and every family of vectors $v_0, \dots, v_{n'-1} \in \mathbb{R}^{m'}$ satisfying $\lVert v_i \rVert \le 1$ for all $i$ (Euclidean/$\ell^2$ norm), there exists a function $\varepsilon : \{0,\dots,n'-1\} \to \mathbb{R}$ with $\varepsilon_i = 1$ or $\varepsilon_i = -1$ for every $i$ (this is the custom definition IsSignVector, unfolded), such that for every coordinate $j \in \{0,\dots,m'-1\}$,

i.e. the signed sum has $\ell^\infty$ norm at most $K$. Note this includes the case $n' = 0$ (empty sum, so it forces $0 \le K$); hence this hypothesis is unsatisfiable for $K < 0$, and the theorem is vacuous for such $K$.

Hypothesis 2. Every entry of $A$ equals $0$ or $1$: for all $i, j$, $A_{ij} = 0 \lor A_{ij} = 1$.

Hypothesis 3 (column sparsity). For every column $j \in \{0,\dots,n-1\}$, the number of rows $i$ with $A_{ij} = 1$ is at most $t$:

Conclusion. There exists a function $\varepsilon : \{0,\dots,n-1\} \to \mathbb{R}$ such that:

• $\varepsilon$ is a sign vector: for every $j$, $\varepsilon_j = 1$ or $\varepsilon_j = -1$; and
• for every row $i \in \{0,\dots,m-1\}$,

where $\sqrt{t}$ is the real square root of the natural number $t$.

Note that the signs in the conclusion are attached to the columns of $A$ and the bound is required for every row $i$, while the sparsity hypothesis bounds the number of $1$-entries in each column. Degenerate instances included by the quantifiers: if $n = 0$ the sum is empty and the conclusion asserts $0 \le K\sqrt{t}$ (with the empty function as sign vector); if $m = 0$ the row condition is vacuous; if $t = 0$ the bound is $K \cdot 0 = 0$ (and Hypothesis 3 then forces every column to have no $1$-entries). The proof body is sorry (the statement is asserted without proof).