A quadratic lower bound for intervals in the Hales–Jewett theorem

A combinatorial line in $[m]^n$ is $q$-fold if its wildcard set, the set of coordinates that vary along the line, is a union of at most $q$ intervals of consecutive coordinates. Let $I(m,r)$ be the least $q$ such that, for $n$ large, every $r$-coloring of $[m]^n$ has a monochromatic $q$-fold line. We show that $I(m,2)>(m-3)^2/128$ for every $m\ge3$, so $I(m,r)\ge I(m,2)$ grows at least quadratically in $m$ for every $r\ge2$. This answers Question 3.1 of Conlon and Kamčev, who asked whether some $m\ge4$, $r\ge2$ and $c>1$ admit $r$-colorings of $[m]^n$ with no monochromatic line whose wildcard set is a union of at most $cr$ intervals: $m=18$, $r=2$ and any $1<c<3/2$ do, for every $n$. For $m=3$ the value is known, $r$ or $r-1$, by work of Conlon and Kamčev, Leader and Räty, and Kamčev and Spiegel; Kamčev and Spiegel noted that $r-1$ is the best explicit lower bound the known methods give, and Shelah's proof of the Hales–Jewett theorem gives the upper bound $\mathrm{HJ}(m-1,r)$. To rule out lines with at most $Q$ intervals, we color $x$ by the parity of $\lfloor S(x)/(32Q)\rfloor$, where $S(x)$ is the sum of the squared differences of consecutive letters of the word $0x$. Along such a line, $S$ is a quadratic in the free letter whose values rise through a whole interval of length $32Q$ in smaller steps, so the line meets both colors. This coloring theorem is proved in Lean from the definitions; the step to $I(m,r)$ is a short argument on paper. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.