Letter-merging proof of the Hales-Jewett theorem (source code)

= Letter-merging proof of the Hales-Jewett theorem

Induct on the alphabet size $k$. For an $r$-colouring, choose an $(k-1,k)$-insensitive <combinatorial subspace> whose dimension forces a <monochromatic> <combinatorial line> over the first $k-1$ letters. The inductive <Hales-Jewett theorem> supplies that line. Changing all of its active parameters from $k-1$ to $k$, one at a time, preserves the colour by the <alphabet insensitivity lemma>. Thus the line extends to all $k$ letters. The one-letter alphabet is the base case.