---

Claim. The consequence that Conlon and Fox draw from their Theorem 1.2 (printed p. 219 of the published paper): for each $n\ge1$ there is a red-blue coloring of $\mathbb R^n$ with no red unit-distance pair and no blue copy of $\ell_m$, the $m$-term progression with unit step, for any $m\ge10^{5n}$. For $n=2$ this gives a coloring of the plane avoiding a red unit pair and every blue unit progression of $10^{10}$ terms, so the least avoiding length $K_*$ of Problem 188 satisfies $K_*\le10^{10}$.

Covers. The upper bound $K_*\le10^{10}$ only. The least avoiding length itself stays open, and the bound is weaker than the Currier–Mody–Xie–Zhang bound $K_*\le6330$, which is not refereed.

Proof. Theorem 1.2 states that a $1$-separated set $K\subset\mathbb R^n$ of diameter at most $R-1$, $R>2$, with $|K|>10^{4n}\log_2R$ has a red-blue coloring of $\mathbb R^n$ with no red unit pair and no blue congruent copy of $K$; its proof colors red a randomly pruned periodic net and bounds the blue copies through a finite count of sign patterns. The corollary applies it to $\ell_M$ with $M=10^{5n}$ and $R=M$. The library's line corollary page writes out the deduction, with the one-dimensional case that the numerical specialization needs.

Postings. The arXiv preprint 1705.02166 was posted on 5 May 2017 (v4 on 20 March 2018), and the paper appeared in Discrete & Computational Geometry 61 (2019), 218–225, published online on 23 March 2018.

Acceptance. Refereed: Discrete & Computational Geometry 61 (2019), 218–225 (received 5 May 2017, accepted 25 February 2018). No formalization of the corollary is recorded.

Depends on. Conlon and Fox, line corollary and Theorem 1.2.