Kleitman's diameter theorem for the Hamming cube

Let $\iota$ be a finite index set of size $r = |\iota|$, and equip $\{0,1\}^\iota$ (equivalently, $\iota \to \mathrm{Bool}$) with the Hamming metric $d(x,y) = |\{j \in \iota : x_j \ne y_j\}|$. Let $s$ be a natural number with $2s < r$, and let $A \subseteq \{0,1\}^\iota$ satisfy

i.e. $A$ is strictly larger than a Hamming ball of radius $s$. Then $A$ contains two points at Hamming distance strictly greater than $2s$:

This is Kleitman's diameter theorem (1966): the diameter of a family exceeding the size of a radius-$s$ Hamming ball must exceed $2s$, twice the naive bound obtainable from a volume/pigeonhole argument alone (which only guarantees a point outside a ball of radius $s$ centred at a fixed element of $A$, hence diameter $> s$). The bound is sharp: a genuine Hamming ball of radius $s$ has diameter exactly $2s$ and size exactly $\sum_{i=0}^s \binom{r}{i}$, so no weaker size hypothesis suffices. The theorem is a key ingredient of J. Spencer's entropy method for discrepancy (Six standard deviations suffice, 1985): a large enough 'fiber' of colourings sharing the same discretised row-sum pattern must contain two colourings that are far apart in Hamming distance, and their difference yields a good partial colouring.

Formalization Note. Stated over a general finite index type $\iota$ rather than specifically $\mathrm{Fin}\,r$ so that it applies directly to an arbitrary finite coordinate set (e.g. a subset of columns) without an explicit re-indexing equivalence.