Rothvoß's Lemma 8: one round of the partial-coloring method

This is Rothvoß's Lemma 8, the one-round partial-coloring lemma at the heart of Spencer's entropy-method proof of the discrepancy theorem, generalized here from a single set to $n$ rows handled jointly.

Fix $n$ rows $a_1,\dots,a_n:\mathrm{Fin}\,m\to\{0,1\}$ on a common active column set of size $m\ge1$, and $\lambda\ge2$ satisfying the entropy budget

Then there exist two Boolean colorings $x,y:\mathrm{Fin}\,m\to\{\mathrm{true},\mathrm{false}\}$ that differ in more than $2\lfloor m/10\rfloor$ coordinates (a substantial fraction of $m$), such that the signed half-difference $\chi:=\tfrac12(\mathrm{RSign}(x)-\mathrm{RSign}(y))$ — a partial coloring valued in $\{-1,0,1\}$, nonzero exactly where $x$ and $y$ disagree — keeps every row's signed sum small:

The proof combines subadditivity of Shannon entropy across the $n$ rows with Rothvo\u00df's Lemma 9 (the per-row entropy bound shannonEntropy_shellFin_le) to bound the joint entropy of the quantized row sums, a pigeonhole argument to find a large bucket of colorings whose row sums are pairwise close, and Kleitman's diameter theorem (via a Pinsker-type bound on the relevant Hamming-ball volume) to extract two colorings in that bucket at large Hamming distance. Iterating this lemma on a shrinking active column set is what proves the full $O(\sqrt n)$ discrepancy bound.

Formalization Note. $\mathrm{RSign}$ is the platform definition of the same name (the $\{-1,+1\}$-valued Rademacher sign of a Boolean coloring).