Brauer progression theorem (source code)

= Brauer progression theorem
{c}

For <positive integers> $k,s,\ell$, some $N$ ensures that every $k$-color <finite coloring> of $[N]$ contains a <monochromatic> set
$$
\{sd,a,a+d,\ldots,a+(\ell-1)d\},\qquad a,d>0.
$$
It follows from the <Van der Waerden theorem> by <mathematical induction> on the number of colors. If $M$ is a bound for $k-1$ colors, take a long one-color <arithmetic progression> of length $(\ell-1)M+1$ and step $d$. Either one of $sd,2sd,\ldots,Msd$ has its color, giving the result immediately, or these multiples use only $k-1$ colors. Pull back their <finite coloring> to $[M]$ and use <mathematical induction>, then multiply the resulting configuration by $sd$. Enlarge the ambient finite <integer interval> to include all these multiples. The cases $k=1$ and $\ell=1$ are immediate. The parameter $s$ makes this useful for positive <monochromatic> solutions of a <partition regular equation> with arbitrary <integer> coefficients.