\documentclass[11pt]{amsart} \usepackage{amsmath,amssymb,amsthm} \usepackage{booktabs} \usepackage{microtype} \usepackage{tikz} \usepackage[margin=1.1in]{geometry} \usepackage[hidelinks]{hyperref} \newtheorem{theorem}{Theorem} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\E}{\mathbb{E}} \newcommand{\Z}{\mathbb{Z}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\C}{\mathbb{C}} \newcommand{\R}{\mathbb{R}} \newcommand{\arrows}{\rightarrow} \newcommand{\narrows}{\not\rightarrow} % ===================================================================================================== % CHOICE OF THE COLOURING -- the only line to change. 60 = cfg_k60.json (90 cells, 204 NEAR pairs; default), % 62 = cfg_t61.json (54 cells, one NEAR pair), % 63 = cfg_h62.json (53 cells, all FAR), 64 = cfg_h63.json (52 cells, all FAR; double-verified 2026-10-02). \newcommand{\UB}{60} % ===================================================================================================== % Placeholders that must be filled (or removed) before release; they print in red. \newcommand{\VERIFYNOTE}[1]{\textcolor{red}{\textbf{[TO FILL: #1]}}} \newcommand{\TODO}[1]{\textcolor{red}{\textbf{[TODO: #1]}}} \newcommand{\DOI}{\href{https://doi.org/10.5281/zenodo.23151058}{doi:10.5281/zenodo.23151058}} % Data of the four candidate colourings. Sources: data/n1001/MIX/cfg_*.json; Claim A numbers from % claimA_nf.py (paper_188/v4/logs/claimA_nf_all.txt; for 60: logs/claimA_k60.txt, logs/indep_nearfar_k60.txt); % Method 2 numbers from data/n1001/V2MIX/*.out; % Method 1 numbers from data/n1001/V1MIX (DIFF_NOTES.txt, verifier1/chain_v1.log, verifier1/chain2.log). \ifnum\UB=60 \newcommand{\MM}{59} % = \UB - 1: every progression meets red among its first \UB points \newcommand{\CFG}{cfg\_k60.json} \newcommand{\CFGSHA}{b15251de\ldots 7b2e} \newcommand{\NCELLS}{90} \newcommand{\NAPO}{48} \newcommand{\APOTEXT}{$39$ of the cells have apothem $h=619/1250=0.4952$, and the others have apothems between $0.0302$ and $0.466$} \newcommand{\NEARTEXT}{There are $204$ unordered near pairs among the $90$ listed cells $c_i+C(h_i)$ of Appendix~\ref{app:centres}, and none of them involves a nonzero lattice translate (all have $g=0$). They involve $44$ of the $90$ cells and fall into $8$ groups. In $7$ of them any two cells are near, so any two points of such a group are at distance less than $1$; the largest of these groups has $19$ cells, the others $3$ to $5$. The eighth group consists of the cells $43,56,58,61$, in which every pair except $\{58,61\}$ is near. Every other pair of cells is far.} \newcommand{\NEARMARGIN}{The smallest near margin is $(1-R^+_{6}-R^+_{80})^2-d^2>4.27\cdot10^{-3}$, for the cells $6$ and $80$ (apothems $0.4952$ and $0.0793$, $d=0.41542\ldots$).} \newcommand{\TRIPLES}{477{,}810} \newcommand{\FARPAIR}{$(i,j)=(58,61)$ and $g=0$, with $|c_i-c_j|^2=626837873549/500000000000$, so $|c_i-c_j|>1.119676$, against $1+R^+_{58}+R^+_{61}<1.114581$} \newcommand{\VtwoBoxes}{all but $73$ of the $40{,}000$ boxes passed at once, and those $73$ passed after at most five bisections ($40{,}198$ certified boxes)} \newcommand{\VtwoLeaves}{147{,}421{,}290} \newcommand{\VtwoMargin}{1.85\cdot10^{-9}} \newcommand{\VtwoTime}{$1049$ s} % Method 1 status (referee 2026-10-04: Method 2 is THE proof; Method 1 is a second check, stated per % colouring only when complete). k60: COMPLETE, PASS, final M 59 (data/n1001/V1MIX/verifier1/ % combine_k60.py -> combine_k60.out; fastk60.log; records runs_k60_N20000_W0.04/{chunk_*, refined59.json.box*, % refined59b.json.box*, l3w.*}; statistics recomputed from the records 2026-10-04). \newcommand{\VoneDone}{1} \newcommand{\INDEPNEAR}{the same $204$ near pairs} \newcommand{\VoneResult}{For the coloring of this note the refinement went one level further. The main pass ($N=20000$, $W=0.04$, $j_{\mathrm{cap}}=130$) had no failures and maximum $86$; $448$ boxes gave a value above $59$. After the first refinement ($4N$ boxes, $W=0.005$), $24$ of these main-pass boxes still had sub-boxes with a value above $59$. Each of these $24$ main-pass boxes was replaced by its $64$ sub-boxes in the tiling with $64N=1{,}280{,}000$ boxes, again with $W=0.005$; this left $210$ sub-boxes with the value $60$, which were recomputed with the narrower strip width $W=0.002$ and then all gave at most $47$. These $210$ sub-boxes lie in the thin range of directions from $21.24^\circ$ to $21.36^\circ$ (boxes $2360$--$2373$ of the main pass), the same region in which Method~2 needed its deepest bisections (five levels, near $21.35^\circ$). A separate script (\texttt{combine\_k60.py}, in place of \texttt{final\_m.py}) reads every record of all levels, checks in each the SHA-256 of the configuration file, the parameters $N$ and $W$ and the position in the nested tilings, and gives the certified value $M=59$; so Method~1 confirms Proposition~\ref{prop:claimB}.} \else\ifnum\UB=62 \newcommand{\MM}{61} % = \UB - 1: every progression meets red among its first \UB points \newcommand{\CFG}{cfg\_t61.json} \newcommand{\CFGSHA}{04212e3b\ldots e0ac} \newcommand{\NCELLS}{54} \newcommand{\NAPO}{14} \newcommand{\APOTEXT}{$40$ of the cells have apothem $h=619/1250=0.4952$, and the others have apothems between $0.1047$ and $0.4904$} \newcommand{\NEARTEXT}{Exactly one pair of cells in each period is near: the cells $47$ and $54$ of Appendix~\ref{app:centres}, whose center distance $d=0.40642\ldots$ satisfies $d+R_{47}+R_{54}<0.9890$; the cell $54$ (apothem $0.2959$) is a \emph{satellite} of the cell $47$. Every other pair of cells is far.} \newcommand{\NEARMARGIN}{The near pair has $(1-R^+_{47}-R^+_{54})^2-d^2>9.14\cdot10^{-3}$.} \newcommand{\TRIPLES}{171{,}990} \newcommand{\FARPAIR}{$(i,j)=(29,48)$ and $g=0$, with $|c_i-c_j|^2=163573702261/62500000000$, so $|c_i-c_j|>1.617769$, against $1+R^+_{29}+R^+_{48}<1.612743$} \newcommand{\VtwoBoxes}{$40{,}000$ boxes passed without bisection} \newcommand{\VtwoLeaves}{145{,}474{,}926} \newcommand{\VtwoMargin}{1.77\cdot10^{-9}} \newcommand{\VtwoTime}{$408$ s} \newcommand{\VoneDone}{0} % Method 1 on cfg_t61 not run (2026-10-04) \newcommand{\INDEPNEAR}{the same near pair} \newcommand{\VoneResult}{For this coloring Method~1 had not been run when this version was written, so Theorem~\ref{thm:upper} rests on Method~2 (Section~\ref{sec:method2}) alone.} \else\ifnum\UB=63 \newcommand{\MM}{62} \newcommand{\CFG}{cfg\_h62.json} \newcommand{\CFGSHA}{42ad67b0\ldots 6376} \newcommand{\NCELLS}{53} \newcommand{\NAPO}{13} \newcommand{\APOTEXT}{$40$ of the cells have apothem $h=619/1250=0.4952$, and the others have apothems between $0.1047$ and $0.4904$} \newcommand{\NEARTEXT}{In this coloring every pair of distinct cells is far.} \newcommand{\NEARMARGIN}{There are no near pairs.} \newcommand{\TRIPLES}{165{,}678} \newcommand{\FARPAIR}{$(i,j)=(29,48)$ and $g=0$, with $|c_i-c_j|^2=163573702261/62500000000$, so $|c_i-c_j|>1.617769$, against $1+R^+_{29}+R^+_{48}<1.612743$} \newcommand{\VtwoBoxes}{$40{,}000$ boxes passed without bisection} \newcommand{\VtwoLeaves}{145{,}103{,}589} \newcommand{\VtwoMargin}{1.77\cdot10^{-9}} \newcommand{\VtwoTime}{$459$ s} \newcommand{\VoneDone}{1} % chain2.log + final_m.py 2026-10-04: certified M 62 \newcommand{\INDEPNEAR}{no near pair} \newcommand{\VoneResult}{The main pass ($N=20000$, $W=0.04$, $j_{\mathrm{cap}}=130$) had no failures and maximum $83$; $182$ boxes gave a value above $62$. After the first refinement ($2289$ s) all of their sub-boxes gave at most $62$. The certified value is $M=62$ (\texttt{final\_m.py}), attained by unrefined boxes of the main pass, so Method~1 confirms Proposition~\ref{prop:claimB}.} \else \newcommand{\MM}{63} \newcommand{\CFG}{cfg\_h63.json} \newcommand{\CFGSHA}{1aab4cbf\ldots 9511} \newcommand{\NCELLS}{52} \newcommand{\NAPO}{12} \newcommand{\APOTEXT}{$40$ of the cells have apothem $h=619/1250=0.4952$, and the others have apothems between $0.1047$ and $0.4904$} \newcommand{\NEARTEXT}{In this coloring every pair of distinct cells is far.} \newcommand{\NEARMARGIN}{There are no near pairs.} \newcommand{\TRIPLES}{159{,}484} \newcommand{\FARPAIR}{$(i,j)=(45,48)$ and $g=0$, with $|c_i-c_j|^2=437060357617/200000000000$, so $|c_i-c_j|>1.478276$, against $1+R^+_{45}+R^+_{48}<1.473249$} \newcommand{\VtwoBoxes}{all but $5$ of the $40{,}000$ boxes passed at once and those $5$ passed after at most two bisections ($40{,}008$ certified boxes)} \newcommand{\VtwoLeaves}{144{,}786{,}936} \newcommand{\VtwoMargin}{2.73\cdot10^{-9}} \newcommand{\VtwoTime}{$94$ min, with the machine shared with other jobs,} \newcommand{\VoneDone}{1} \newcommand{\INDEPNEAR}{no near pair} \newcommand{\VoneResult}{The main pass ($N=20000$, $W=0.04$, $j_{\mathrm{cap}}=130$; $879$ s) had no failures and maximum $83$; $170$ boxes gave a value above $63$. After the first refinement ($657$ s) two boxes, $8078$ and $8079$ (near $72.7^\circ$), still had sub-boxes with value $70$; at the second level ($N=320000$, $W=0.002$) all of these gave at most $63$. The certified value is $M=63$, attained by unrefined boxes of the main pass, so Method~1 confirms Proposition~\ref{prop:claimB}.} \fi\fi\fi \title[Erd\H{o}s Problem \#188: $7\le k\le \UB$]{Bounds for Erd\H{o}s Problem \#188: $7\le k\le \UB$} \author{Carson Crocker} \address{Independent researcher} \email{carson.crocker1999@gmail.com} \date{\today} \begin{document} \begin{abstract} Let $\ell_k$ denote $k$ collinear points with consecutive distances $1$. Erd\H{o}s Problem~\#188 asks for the least $k$ such that the plane can be colored red and blue with no two red points at distance $1$ and no blue copy of $\ell_k$; the bounds $6\le k\le 6330$ were known. We prove $7\le k\le \UB$. For the lower bound we show that every red/blue coloring of the plane contains two red points at distance $1$ or a blue $\ell_6$, following the skeleton of Arman and Tsaturian's proof in three dimensions; four distance lemmas are reduced to explicit unsatisfiable propositional formulas, certified by DRAT proofs. For the upper bound we give an explicit periodic coloring whose red set consists of $\NCELLS$ closed regular $24$-gons of $\NAPO$ different sizes, all of diameter less than $0.999$, in each period, with rational centers and sizes. \ifnum\UB<63 Any two cells are either far apart (all distances between their points exceed $1$) or close together (all distances are less than $1$), \else Any two cells are far apart (all distances between their points exceed $1$), \fi which is checked in exact arithmetic and rules out red unit pairs. That every $\ell_{\UB}$ contains a red point is proved by a computer program that shows that $\UB$ translates of the red set cover the torus, with every inclusion checked in ball arithmetic. \ifnum\VoneDone=1 A second, separately written program, based on a reduction to one-dimensional covering problems solved in outward-rounded interval arithmetic, confirms this. \fi The computations, the verification code and drafts of the text were produced with AI tools under the author's direction; all proof certificates and verification programs are public. \end{abstract} \maketitle \ifnum\UB=60 \noindent\emph{Changes in this version (2026-10-15).} Corrections to the text only; no theorem, bound, certificate or program changes. Section~\ref{sec:exact} now states that the value of the coloring is exactly $60$, with the blue $\ell_{59}$ that the package already contained (the previous version said the exact value was not known), and Section~\ref{sec:search} refers to it. The definition of the search score in Section~\ref{sec:search} was off by one (it counted translates instead of one less than that count); the definition is corrected and called a numerical proxy, and the numbers in that section are unchanged. Section~\ref{sec:method1} now says that the $24$ boxes refined twice are main-pass boxes. The package DOI cited is now the all-versions DOI. \fi \section{Introduction} For finite configurations $K,K'\subset\E^n$, write $\E^n\arrows(K,K')$ if every red/blue coloring of $\E^n$ contains a red congruent copy of $K$ or a blue congruent copy of $K'$, and $\E^n\narrows(K,K')$ otherwise. Here $\ell_k$ is the configuration of $k$ collinear points with distance $1$ between consecutive points; a copy of $\ell_2$ is a pair of points at distance $1$. Erd\H{o}s Problem~\#188~\cite{EP188} asks for the smallest $k$ such that the plane can be colored red and blue with no two red points at distance $1$ and no blue $\ell_k$; that is, the smallest $k$ with $\E^2\narrows(\ell_2,\ell_k)$. Before this note the known bounds were $6\le k\le 6330$: Tsaturian~\cite{Tsa17} proved $\E^2\arrows(\ell_2,\ell_5)$, and Currier, Mody, Xie and Zhang proved $\E^2\narrows(\ell_2,\ell_{6330})$~\cite[Theorem~1.2]{CMXZ26}. Their planar coloring is built from the Voronoi cells of a hexagonal lattice, scaled to have diameter slightly less than $1$, with red cells chosen at random subject to a local rule that rules out red unit pairs. Section~\ref{sec:background} places the problem among the known results on relations $\E^n\arrows(\ell_s,\ell_t)$ and their negations. We prove the following. \begin{theorem}\label{thm:lower} Every red/blue coloring of $\E^2$ contains two red points at distance $1$ or a blue $\ell_6$. That is, $\E^2\arrows(\ell_2,\ell_6)$. \end{theorem} \begin{theorem}\label{thm:upper} There is a red/blue coloring of $\E^2$, periodic with respect to a lattice, in which no two red points are at distance $1$ and every copy of $\ell_{\UB}$ contains a red point. That is, $\E^2\narrows(\ell_2,\ell_{\UB})$. \end{theorem} \begin{corollary} The answer $k$ to Erd\H{o}s Problem~\#188 satisfies $7\le k\le \UB$. \end{corollary} For Theorem~\ref{thm:lower} we follow Arman and Tsaturian~\cite{AT17}: first exclude red pairs at a few distances, then find a monochromatic circle. Their distance lemmas use three-dimensional circles. In the plane we obtain the distance lemmas instead from the unsatisfiability of four propositional formulas on explicit finite point sets built from rotated patches of the triangular lattice (Sections~\ref{sec:proof} and~\ref{sec:sets}). Remark~\ref{rem:k8} records what we know about the next case, $\E^2\arrows(\ell_2,\ell_7)$. For Theorem~\ref{thm:upper} the red set is a periodic union of convex cells of diameter less than $1$, as in~\cite{CMXZ26}, where the cell framework and the hexagonal cells come from. Our cells are nearly round (regular $24$-gons), they have $\NAPO$ different sizes, and their centers are not on a lattice: $\NCELLS$ cells at explicit rational centers in each period of a lattice $\Gamma$ (Section~\ref{sec:colouring}). That no two red points are at distance $1$ follows from a simple rule, checked in exact arithmetic: every two cells are either far apart or close together (Lemma~\ref{lem:nearfar}). That there is no blue $\ell_{\UB}$ is proved by computer (Section~\ref{sec:claimB}): the space of all copies of $\ell_{\UB}$ modulo the period is compact, and a program checks, with every inclusion certified in ball arithmetic, that finitely many translates of the red set cover the torus (Method~2). A second, separately written program with a different reduction (Method~1) \ifnum\VoneDone=1 confirms the result\else is a further check, whose run for this coloring had not been completed when this version was written\fi. \emph{History.} An earlier draft of this note proved $k\le 166$ with a coloring of the kind used in~\cite{CMXZ26}: $36$ red closed regular hexagons of diameter $19/20$ among the Voronoi cells of a hexagonal lattice, in a $19\times19$ period. Cells that are nearly disks of diameter just below $1$, centers that are free rational points instead of lattice points, and the insertion of cells into the largest holes then gave $k\le 107$ and $k\le 85$ ($42$ equal cells per period). Red cells of different sizes, with smaller cells in the gaps between the large ones, gave $k\le 69$ and then $k\le 64$\ifnum\UB<64, and further search in the same setting gave $k\le 63$\fi.\ifnum\UB<63{} The step from $63$ to $62$ comes from relaxing the rule that all cells are far apart: a small cell (a \emph{satellite}) may sit close to another cell, so close that all distances between the two are less than $1$ (Lemma~\ref{lem:nearfar}).\fi\ifnum\UB<62{} The targeted insertion of one further cell gave $k\le 61$\ifnum\UB<61, and a search in which satellites are inserted, moved and resized gave $k\le 60$\fi.\fi{} The searches are described in Section~\ref{sec:search}; they play no role in the proofs. \subsection{Background}\label{sec:background} Relations of the form $\E^n\arrows(K,K')$ were introduced by Erd\H{o}s, Graham, Montgomery, Rothschild, Spencer and Straus in the series~\cite{EGMRSS73,EGMRSS75,EGMRSS75b}; the case of $\ell_2$ against a set $K$ is their question of which $K$ must appear in blue when the red points span no unit distance. (With more colors and $\ell_2$ in every color one obtains the Hadwiger--Nelson problem; at least five colors are needed for the plane~\cite{deG18}.) A coloring of $\E^n$ restricts to every plane, or subspace, of $\E^n$, so a relation $\E^d\arrows(K,K')$ implies $\E^n\arrows(K,K')$ for all $n\ge d$, and $\E^n\narrows(K,K')$ implies $\E^d\narrows(K,K')$ for $d\le n$. Table~\ref{tab:known} lists the results we know of; most are collected in the introduction of~\cite{CMXZ26}, to which we refer for further discussion. \emph{$\ell_2$ against $\ell_k$ in fixed dimension.} In the plane, Erd\H{o}s et al.~\cite{EGMRSS75} proved $\E^2\arrows(\ell_2,K)$ for every $3$-point set $K$ and $\E^2\arrows(\ell_2,\ell_4)$; Juh\'asz~\cite{Juh79} extended the first result to every $4$-point set, and Tsaturian~\cite{Tsa17} proved $\E^2\arrows(\ell_2,\ell_5)$. For general sets there are small exceptions: Juh\'asz~\cite{Juh79} gave a $12$-point set $K$ with $\E^2\narrows(\ell_2,K)$, and Csizmadia and T\'oth~\cite{CT94} an $8$-point one, a regular heptagon with its center. In three dimensions Iv\'an~\cite{Iva79} proved, as reported in~\cite{AT17}, $\E^3\arrows(\ell_2,K)$ for every $5$-point set $K$, and Arman and Tsaturian proved $\E^3\arrows(\ell_2,\ell_6)$~\cite{AT17} and $\E^n\arrows(\ell_2,\ell_{n+3})$ for $n\ge4$~\cite{AT17b}. \emph{Growth with the dimension.} Szlam~\cite{Szl01} (see~\cite{CF19}) showed, using the Frankl--Wilson theorem~\cite{FW81}, that every red/blue coloring of $\E^n$ contains a red $\ell_2$ or a blue translate of any given set of at most $2^{cn}$ points; with Raigorodskii's bound~\cite{Rai00} this gives $\E^n\arrows(\ell_2,K)$ for $|K|\le(1.239\ldots+o(1))^n$~\cite[Section~1]{CMXZ26}; here and below $o(1)$ is as $n\to\infty$. Conversely, Conlon and Fox~\cite{CF19} proved $\E^n\narrows(\ell_2,K)$ for every $1$-separated set $K$ of diameter at most $R-1$ with $|K|>10^{4n}\log_2 R$ ($R>2$), in particular $\E^n\narrows(\ell_2,\ell_m)$ for $m\ge10^{5n}$; this answered a question of Erd\H{o}s et al.~\cite{EGMRSS75}. Currier, Mody, Xie and Zhang improved this to $m>(5+o(1))^n$ (\cite[Theorem~1.1]{CMXZ26} and the remark following it). In the plane, Erd\H{o}s and Graham~\cite{EG80} remarked without proof that some $m$ ``at most 10000000'' has $\E^2\narrows(\ell_2,\ell_m)$ (we quote this from~\cite[Section~1]{CMXZ26}; see also~\cite{EP188}); the argument of~\cite{CF19} gives $m$ of order $10^{10}$, and \cite[Theorem~1.2]{CMXZ26} gives $m=6330$. \emph{Longer red progressions.} Currier, Moore and Yip~\cite{CMY24} proved that every red/blue coloring of the plane contains a monochromatic $\ell_3$, that is, $\E^2\arrows(\ell_3,\ell_3)$. Conlon and Fox, and independently Arman and Tsaturian, asked whether there is an $m$ with $\E^n\narrows(\ell_3,\ell_m)$ for every $n$; Conlon and Wu~\cite{CW23} showed that there is, with $m=10^{50}$ (as stated in~\cite{FT25}), F\"uhrer and T\'oth~\cite{FT25} lowered $m$ to $1177$, and Currier, Moore and Yip~\cite{CMY26} to $20$. The latter also proved $\E^n\narrows(\ell_4,\ell_{14})$ and $\E^n\narrows(\ell_5,\ell_8)$ for all $n$, while $\E^n\narrows(\ell_6,\ell_6)$ goes back to~\cite[Theorem~12]{EGMRSS73}. \emph{Colorings.} The negative results use geometric coloring constructions, sometimes with probabilistic choices. Those of~\cite{EGMRSS73} color a point $x$ by the residue of an integer part of a multiple of $|x|^2$. In~\cite{CF19,CMXZ26} space is partitioned into cells of diameter less than $1$, cells are colored red at random subject to a rule that prevents red unit pairs, and a probabilistic argument shows that some such coloring has no blue copy of the forbidden configuration. The coloring of the present note is explicit: its red set is a periodic union of cells of several sizes (regular $24$-gons, which do not partition the plane), any two of which are far apart or close together, and that every copy of $\ell_{\UB}$ meets a red cell is checked by computer;~\cite{CMY26} gives a general framework for avoiding short progressions. Erd\H{o}s Problem~\#188 is the planar case of the $(\ell_2,\ell_k)$ question: before this note $6\le k\le 6330$ was known, and Theorems~\ref{thm:lower} and~\ref{thm:upper} give $7\le k\le \UB$. \begin{table}[t] \caption{Known results on $\E^n\arrows(\ell_s,K)$ and $\E^n\narrows(\ell_s,K)$ (red $\ell_s$, blue $K$). Positive results in $\E^d$ hold in all $\E^n$, $n\ge d$. Rows with $o(1)$ are asymptotic statements, $o(1)\to0$ as $n\to\infty$.}\label{tab:known} \centering\small \begin{tabular}{@{}lll@{}} \toprule Relation & Dimension & Reference\\ \midrule $\arrows(\ell_2,K)$, every $K$ with $|K|=3$; $\arrows(\ell_2,\ell_4)$ & $n=2$ & \cite{EGMRSS75}\\ $\arrows(\ell_2,K)$, every $K$ with $|K|=4$ & $n=2$ & \cite{Juh79}\\ $\arrows(\ell_2,\ell_5)$ & $n=2$ & \cite{Tsa17}\\ $\arrows(\ell_2,\ell_6)$ & $n=2$ & Theorem~\ref{thm:lower}\\ $\narrows(\ell_2,K)$ for some $K$ with $|K|=12$; $|K|=8$ & $n=2$ & \cite{Juh79}; \cite{CT94}\\ $\narrows(\ell_2,\ell_{6330})$ & $n=2$ & \cite[Thm.~1.2]{CMXZ26}\\ $\narrows(\ell_2,\ell_{\UB})$ & $n=2$ & Theorem~\ref{thm:upper}\\ \midrule $\arrows(\ell_2,K)$, every $K$ with $|K|=5$ & $n=3$ & \cite{Iva79} (see~\cite{AT17})\\ $\arrows(\ell_2,\ell_6)$ & $n=3$ & \cite{AT17}\\ $\arrows(\ell_2,\ell_{n+3})$ & $n\ge4$ & \cite{AT17b}\\ $\arrows(\ell_2,K)$, every $K$ with $|K|\le(1.239\ldots+o(1))^n$ & $n\to\infty$ & \cite{Szl01,Rai00,CMXZ26}\\ $\narrows(\ell_2,\ell_m)$, $m\ge10^{5n}$ & all $n$ & \cite{CF19}\\ $\narrows(\ell_2,\ell_m)$, $m>(5+o(1))^n$ & $n\to\infty$ & \cite[Thm.~1.1]{CMXZ26}\\ \midrule $\arrows(\ell_3,\ell_3)$ & $n=2$ & \cite{CMY24}\\ $\narrows(\ell_3,\ell_{10^{50}})$; $\narrows(\ell_3,\ell_{1177})$; $\narrows(\ell_3,\ell_{20})$ & all $n$ & \cite{CW23}; \cite{FT25}; \cite{CMY26}\\ $\narrows(\ell_4,\ell_{14})$; $\narrows(\ell_5,\ell_8)$ & all $n$ & \cite{CMY26}\\ $\narrows(\ell_6,\ell_6)$ & all $n$ & \cite[Thm.~12]{EGMRSS73}\\ \bottomrule \end{tabular} \end{table} \section{Proof of the lower bound}\label{sec:proof} Call a red/blue coloring of the plane \emph{good} if it contains no two red points at distance $1$ and no blue $\ell_6$. We show that no good coloring exists. \begin{lemma}\label{lem:ladder} In a good coloring, no two red points are at distance $d$, for each $d\in\{4,3,2,6\}$. \end{lemma} The four cases are proved in the order $d=4,3,2,6$, and the case $d$ uses only the cases before it. \begin{proof} Identify the plane with $\C$. For each $d\in\{4,3,2,6\}$ let $D'(d)$ be the set of earlier distances: $D'(4)=\emptyset$, $D'(3)=\{4\}$, $D'(2)=\{4,3\}$, $D'(6)=\{4,3,2\}$. In Section~\ref{sec:sets} we give a finite set $S_d\subset\C$ containing $0$ and $d$ together with a propositional formula $F_d$ in one variable $r_x$ (``$x$ is red'') for each $x\in S_d$. The formula $F_d$ is a conjunction of clauses of the following four kinds: \begin{enumerate} \item[(i)] the unit clauses $r_0$ and $r_d$; \item[(ii)] $\neg r_x\vee\neg r_y$ for certain pairs $x,y\in S_d$ with $|x-y|=1$; \item[(iii)] $r_{x}\vee r_{x+u}\vee\dots\vee r_{x+5u}$ for certain $x\in S_d$ and $|u|=1$ with all six points in $S_d$; \item[(iv)] $\neg r_x\vee\neg r_y$ for certain pairs $x,y\in S_d$ with $|x-y|\in D'(d)$. \end{enumerate} Each $F_d$ is unsatisfiable (Section~\ref{sec:sets}). Suppose the case $d$ fails, so a good coloring has red points $p,q$ with $|p-q|=d$, and assume the earlier cases hold. The map $\phi(z)=p+(q-p)z/d$ is an orientation-preserving isometry of $\C$ with $\phi(0)=p$ and $\phi(d)=q$. Set $r_x$ true if and only if $\phi(x)$ is red. Clauses (i) hold because $p,q$ are red. Clauses (ii) hold because the coloring has no red pair at distance $1$. Clauses (iii) hold because $\phi$ maps $\{x,x+u,\dots,x+5u\}$ onto a copy of $\ell_6$, which is not all blue. Clauses (iv) hold by the earlier cases. So $F_d$ is satisfiable, a contradiction. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:lower}] Suppose a good coloring exists. Not every point is blue, since the plane contains an $\ell_6$; let $A$ be red. Let $u$ be any unit vector. The points $A+u,A+2u,\dots,A+6u$ form an $\ell_6$, so one of them is red. Its distance from $A$ is $j\in\{1,\dots,6\}$. The case $j=1$ is excluded because the coloring has no red pair at distance $1$, and $j\in\{2,3,4,6\}$ is excluded by Lemma~\ref{lem:ladder}. Hence $A+5u$ is red for every unit vector $u$, so the whole circle of radius $5$ about $A$ is red. This circle contains two points at distance $1$, a contradiction. \end{proof} \section{The point sets and the certificates for the lower bound}\label{sec:sets} Let $\omega=e^{i\pi/3}$, so $\omega^2=\omega-1$, and let \[ H_R=\{a+b\omega:\ a,b\in\Z,\ \max(|a|,|b|,|a+b|)\le R\}, \] a hexagonal patch of the triangular lattice with $3R^2+3R+1$ points. We use two rotations by unit complex numbers, \[ \rho_M=\frac{5+\sqrt{-11}}{6}\quad(\cos=5/6),\qquad \rho_7=\frac{5+3\omega}{7}\quad(\cos=13/14). \] The first is the Moser-spindle angle, the rotation about the origin that moves a lattice point at distance $\sqrt3$ by exactly $1$. The second moves a lattice point at distance $\sqrt7$ by exactly $1$. With $\bar\rho$ denoting complex conjugation, define the Minkowski unions \begin{align*} S &= H_6\ \cup\ (H_6+\rho_M H_3)\ \cup\ (H_6+\bar\rho_M H_3),\\ S' &= S\ \cup\ (H_6+\rho_7 H_3)\ \cup\ (H_6+\bar\rho_7 H_3). \end{align*} We take $S_4=S_3=S$ ($8{,}899$ points) and $S_2=S_6=S'$ ($11{,}797$ points). All points lie in the field $K=\Q(\omega,\sqrt{-11})$ of degree $4$ over $\Q$; each point is stored exactly as an integer $4$-tuple $(a,b,c,e)$ representing $\bigl((a+b\omega)+(c+e\omega)\sqrt{-11}\bigr)/42$. Since $\{1,\omega,\sqrt{-11},\omega\sqrt{-11}\}$ is a $\Q$-basis of $K$, equal tuples are equal points, and with the embedding $\sqrt{-11}\mapsto i\sqrt{11}$, \[ 4\cdot 42^2\,|z|^2=(2a+b)^2+3b^2+11(2c+e)^2+33e^2+4(bc-ae)\sqrt{33}, \] so every distance condition in the formulas can be checked in integer arithmetic. The clauses use a finite set $U$ of unit vectors (up to sign): all unit differences between points of the set within distance $2.2$ of the origin, each verified to have norm exactly $1$ in $K$. This gives $|U|=15$ for $S$ and $|U|=21$ for $S'$. The clauses of type (ii) are the pairs $\{x,x+u\}$, type (iii) the progressions $x,x+u,\dots,x+5u$, and type (iv) the pairs $\{x,x+d'u\}$ for $d'\in D'(d)$, over all $u\in U$ and all $x$ such that the points lie in the set. Using only some of the valid constraints is harmless: any clause set in which every clause is of type (i)--(iv) suffices for the proof of Lemma~\ref{lem:ladder}. \begin{table}[h] \centering \small \begin{tabular}{@{}lrrrrrrr@{}} \toprule Lemma & Points & $|U|$ & Clauses (ii) & (iii) & (iv) & Total & DRAT proof\\ \midrule $d=4$ & 8{,}899 & 15 & 62{,}004 & 16{,}380 & --- & 78{,}386 & 57.6 MB\\ $d=3$ & 8{,}899 & 15 & 62{,}004 & 16{,}380 & 22{,}863 & 101{,}249 & 3.3 MB\\ $d=2$ & 11{,}797 & 21 & 79{,}368 & 27{,}672 & 89{,}181 & 196{,}223 & 3.8 kB\\ $d=6$ & 11{,}797 & 21 & 79{,}368 & 27{,}672 & 150{,}624 & 257{,}666 & 1.9 kB\\ \bottomrule \end{tabular} \medskip \begin{tabular}{@{}lrrrr@{}} \toprule Lemma & Earlier distances & Solve time & Check time & Clauses in core\\ \midrule $d=4$ & --- & 1854 s & 464 s & 46{,}695\\ $d=3$ & 4 & 106 s & 107 s & 18{,}776\\ $d=2$ & 4, 3 & 3.4 s & 68 s & 117\\ $d=6$ & 4, 3, 2 & 5.4 s & 85 s & 108\\ \bottomrule \end{tabular} \caption{The four formulas. Totals include the two unit clauses (i). The type (iv) counts split as $35{,}559+53{,}622$ (distances $4,3$) for $d=2$ and $35{,}559+53{,}622+61{,}443$ (distances $4,3,2$) for $d=6$. Proofs are binary DRAT produced by CaDiCaL~1.5.3~\cite{BFFH20} through PySAT~\cite{IMM18}; checks are by \texttt{drat-trim}~\cite{WHH14}. Times are wall-clock on a shared laptop and are only indicative; with local copies of the files, \texttt{drat-trim} checks $d=4$ in about $260$ s and each of the others in under $5$ s.} \label{tab:sets} \end{table} \begin{remark} The two smallest proofs have unsatisfiable cores of $117$ and $108$ clauses, small enough in principle to be written out as a case analysis by hand. The case $d=4$ is the hard one: its core has $46{,}695$ clauses, and it is the only lemma that uses no earlier distance. \end{remark} The certificates were checked by the construction pipeline; by a separate verifier written from the data files alone, with its own field arithmetic and its own solvers (Glucose and Lingeling), which also produced and checked its own DRAT proofs for $d=2,3,6$; by a separate AI-assisted review, which re-ran \texttt{drat-trim} on all four proofs; and by an independent re-check with a different AI system, which regenerated the two point sets, checked every clause in exact arithmetic and re-solved all four formulas as unsatisfiable with its own SAT solver. None found an error. We also converted the four DRAT proofs to LRAT with \texttt{drat-trim -L} and checked them with \texttt{lrat-check}; the LRAT files are in the public package, so they can also be checked by a formally verified LRAT checker~\cite{CHHKS17}, which we have not done. \begin{remark}[Towards $k\ge 8$]\label{rem:k8} For $t>0$ let $L_t$ be the statement: a red/blue coloring of the plane with no red pair at distance $1$ and no blue $\ell_7$ has no two red points at distance $t$. With $\ell_7$ in place of $\ell_6$ in the clauses (iii), the method of Lemma~\ref{lem:ladder} gives the following conditional statements; for each, the clauses were checked in exact arithmetic by a separate script and a DRAT (or DRUP) proof was verified by \texttt{drat-trim}. On the set $S'$, $L_3$ implies each of $L_2$, $L_4$, $L_6$, $L_7$, and $L_7$ implies $L_3$; and a formula on $43$ points (a red point $0$ and the points $ju$, $1\le j\le 7$, for six exact unit vectors $u$) shows that a coloring with no red pair at distance $1,2,3,4$ or $6$ has a blue $\ell_7$. Hence $k\ge 8$ would follow from the single lemma $L_3$. In the larger $\Z$-module $M=\Z[\omega]+\sum_\rho(\rho\,\Z[\omega]+\bar\rho\,\Z[\omega])$, $\rho\in\{\rho_M,\rho_7,\rho_{10}\}$ with $\rho_{10}=(1+3\sqrt{-11})/10$ (cosine $1/10$), which lies in $K$ and contains $63$ unit vectors up to sign, the same method proves $L_{\sqrt{21}}\Rightarrow L_3$, $L_3\Rightarrow L_{\sqrt{21}}$ and $L_{\sqrt{19}}\wedge L_{\sqrt{21}}\Rightarrow L_3$ (on sets of $20{,}941$, $20{,}941$ and $11{,}503$ points built like $S'$). So $L_{\sqrt{21}}$ would also suffice. We have proved neither $L_3$ nor $L_{\sqrt{21}}$. The $\Z$-module $M'$ generated by $S'$ has a homomorphism $\phi\colon M'\to\Z/5$ that is nonzero on every unit vector of $M'$ (given explicitly, with a checker, in the package~\cite{Zen188}), and coloring $x\in M'$ red if and only if $\phi(x)=0$ gives no red unit pair and no blue $\ell_7$ inside $M'$, since five consecutive points of a unit progression in $M'$ meet every residue class. So no finite subset of $M'$ can yield a contradiction from the constraints ``no red unit pair'' and ``no blue $\ell_7$'' together with one prescribed red point; in particular $\E^2\arrows(\ell_2,\ell_7)$ cannot be proved in this way inside $M'$. In $M$ this particular obstruction disappears: $\rho_{10}+\bar\rho_{10}=1/5$ lies in $M$, so every homomorphism $M\to\Z/5$ vanishes on the unit vector $1$. This does not show that some finite subset of $M$ gives an unsatisfiable formula. \end{remark} \section{The coloring for the upper bound}\label{sec:colouring} Let \[ P_1=\Bigl(\frac{15620641}{10^6},\,0\Bigr),\qquad P_2=\Bigl(\frac{7980039}{10^6},\,\frac{13537743}{10^6}\Bigr), \qquad \Gamma=\Z P_1+\Z P_2 , \] and write $L=15.620641$, $H=13.537743$ and $P_2=(P_{2x},H)$ with $P_{2x}=7.980039$; so $P_2$ points in the direction $59.48\ldots^\circ$. The fundamental parallelogram $F=\{\alpha P_1+\beta P_2:\ \alpha,\beta\in[0,1)\}$ spanned by $P_1$ and $P_2$ is a fundamental domain of $\Gamma$, of area $LH=211.468\ldots$. For $0\le k\le 11$ let $n_k=(\cos\psi_k,\sin\psi_k)$ with $\psi_k=(2k+1)\pi/24$, and for $h>0$ let \[ C(h)=\bigl\{q\in\R^2:\ |n_k\cdot q|\le h\ \text{ for } k=0,\dots,11\bigr\}, \] the closed regular $24$-gon with center $0$, inradius (apothem) $h$ and circumradius $R(h)=h/\cos(\pi/24)$, whose vertices point in the directions $15m^\circ$. Thus $D(0,h)\subseteq C(h)\subseteq D(0,R(h))$, where $D(z,r)$ is the closed disk of radius $r$ about $z$. Let $c_1,\dots,c_{\NCELLS}$ be the rational points and $h_1,\dots,h_{\NCELLS}$ the rational apothems listed in Appendix~\ref{app:centres}, put $R_i=R(h_i)$, and define \[ \mathrm{RED}=\bigcup_{g\in\Gamma}\ \bigcup_{i=1}^{\NCELLS}\,\bigl(c_i+g+C(h_i)\bigr),\qquad \mathrm{BLUE}=\R^2\setminus\mathrm{RED}. \] We call the sets $c_i+g+C(h_i)$ the \emph{red cells} and $c_i+g$ their \emph{centers}. The coloring is invariant under translation by $\Gamma$. There are $\NAPO$ different apothems: \APOTEXT. Every $h_i$ is at most $0.4952$, so $R_i<0.4994731$ and every cell has diameter $2R_i<0.998947$. Figure~\ref{fig:period} shows one period. The same data are in the file \texttt{\CFG} of the package~\cite{Zen188} (SHA-256 \texttt{\CFGSHA}). \begin{figure}[h] \centering \input{period_fig_\UB.tex} \caption{Illustration of one period of the coloring, drawn in floating point from \texttt{\CFG}. The dashed parallelogram is the fundamental domain $F$ spanned by $P_1$ and $P_2$; the dark cells are the cells $c_i+g_i+C(h_i)$, with $g_i\in\Gamma$ chosen so that the center lies in $F$, and the light ones are some of their other translates.\ifnum\UB=62{} The two cells of the near pair are drawn in orange.\fi\ifnum\UB=60{} The $44$ cells that belong to near pairs are drawn in orange.\fi} \label{fig:period} \end{figure} \begin{remark}[Other cell shapes]\label{rem:shapes} Claim~A below uses only $c_i+g+C(h_i)\subseteq D(c_i+g,R_i)$, and the second proof of Claim~B (Section~\ref{sec:method2}) uses only $D(c_i+g,h_i)\subseteq c_i+g+C(h_i)$. So Theorem~\ref{thm:upper}, with the bound $\UB$, holds for every coloring whose red set is $\bigcup_{g,i}(C_i+g)$ with $D(c_i,h_i)\subseteq C_i\subseteq D(c_i,R_i)$, for instance for the $24$-gons in any orientation or for the closed disks of radius $h_i$. The inclusion tests of the second proof are strict, so it in fact uses only the open disks: $\mathrm{RED}\supseteq\bigcup_{g,i}D^\circ(c_i+g,h_i)$, where $D^\circ(z,r)$ is the open disk (Section~\ref{sec:method2}). Hence the same conclusion holds when $D(c_i,h_i)$ is replaced by $D^\circ(c_i,h_i)$ in the hypothesis, for instance for the open disks of radius $h_i$. The first proof of Claim~B (Section~\ref{sec:method1}) is written for the $24$-gons $C(h_i)$ above. \end{remark} \subsection*{Claim A: no two red points are at distance $1$} The cells of~\cite{CMXZ26} are pairwise far apart. We also allow pairs of cells that are close together. \begin{lemma}[Near or far]\label{lem:nearfar} Let $\mathrm{RED}=\bigcup_{\alpha\in A}Q_\alpha$, where each piece $Q_\alpha$ lies in a closed disk $D(z_\alpha,r_\alpha)$ with $2r_\alpha<1$. Call two distinct indices $\alpha,\beta$ \emph{far} if $|z_\alpha-z_\beta|>1+r_\alpha+r_\beta$, and \emph{near} if $|z_\alpha-z_\beta|+r_\alpha+r_\beta<1$. If every two distinct indices are far or near, then no two points of $\mathrm{RED}$ are at distance $1$. \end{lemma} \begin{proof} Let $p\in Q_\alpha$ and $q\in Q_\beta$. If $\alpha=\beta$, then $|p-q|\le 2r_\alpha<1$. Otherwise $|p-z_\alpha|\le r_\alpha$ and $|q-z_\beta|\le r_\beta$, so $|z_\alpha-z_\beta|-r_\alpha-r_\beta\le|p-q|\le|z_\alpha-z_\beta|+r_\alpha+r_\beta$. If $\alpha,\beta$ are far, the left-hand side exceeds $1$; if they are near, the right-hand side is less than $1$. \end{proof} So the distances between the points of two far pieces are all greater than $1$, and those between the points of two near pieces are all less than $1$. Near pieces may overlap; the lemma does not need disjoint pieces. The extra freedom matters: a small cell can sit next to a large one, inside the annulus of width $1$ around it from which all far cells are excluded. \begin{proposition}[Claim A]\label{prop:claimA} The red cells, with $z=c_i+g$ and $r=R_i$, satisfy the hypothesis of Lemma~\ref{lem:nearfar}. Hence no two red points are at distance $1$. \NEARTEXT \end{proposition} \begin{proof} Let $c^+$ be a rational number with $c^+>1/\cos(\pi/24)$ (checked in Arb) and put $R_i^+=h_ic^+$, so $R_i0$ and $q<(1-R_i^+-R_j^+)^2$, and otherwise requires $q>(1+R_i^++R_j^+)^2$, that is, that the pair is far. All triples pass. The smallest margin among the far pairs is attained for \FARPAIR. \NEARMARGIN \end{proof} \ifnum\UB=64 Two further programs (\texttt{claimA.py}, written for colorings in which all pairs are far, and the first part of the Method~1 verifier) check the same statement with their own windows and their own rigorous bounds on the $R_i$, and find the same closest pair. \else A second program, \texttt{indep\_nearfar.py}, which was written separately, in an AI-assisted review of \texttt{claimA\_nf.py}, checks the same statement in exact rational arithmetic only: it bounds $\pi$ by Machin's formula and $\cos(\pi/24)$ from below by a truncated Taylor series, so it uses its own rational upper bound for the $R_i$; and it uses its own window: for each pair $(i,j)$, every $g\in\Gamma$ for which both coordinates of $c_i+g-c_j$ are at most $1+2\max_iR_i$ in absolute value. It finds no pair that is neither near nor far, \INDEPNEAR{} and the same closest far pair. \fi \section{Claim B: every $\ell_{\UB}$ contains a red point}\label{sec:claimB} \begin{proposition}[Claim B]\label{prop:claimB} For every $x\in\R^2$ and every unit vector $u$, at least one of the points $x,x+u,\dots,x+\MM u$ is red. Hence the coloring of Section~\ref{sec:colouring} has no blue $\ell_{\UB}$. \end{proposition} Proposition~\ref{prop:claimB} is proved by computation with Method~2 (Section~\ref{sec:method2}). Method~1 (Section~\ref{sec:method1}) is a separately written second check with a different reduction; \ifnum\VoneDone=1 it confirms the proposition\else for this coloring its run had not been completed when this version was written\fi. We first state the common reduction, which is rigorous, and then the two methods and what exactly each of them checks. \subsection{Common reduction} Write $u(\theta)=(\cos\theta,\sin\theta)$ and, for an integer $M$, let $B(M)$ be the statement: for every $x\in\R^2$ and every $\theta\in[0,\pi]$ some point $x+ju(\theta)$ with $0\le j\le M$ is red. A copy of $\ell_{M+1}$ with direction $\theta+\pi$ is also a copy with direction $\theta$ (start from its other end), so $B(M)$ implies that every copy of $\ell_{M+1}$ contains a red point. We show $B(\MM)$. The following reformulation is immediate, since $x+ju\in\mathrm{RED}$ if and only if $x\in\mathrm{RED}-ju$. \begin{lemma}\label{lem:torus} Let $u$ be a unit vector and $M\ge0$. There is a start $x$ with $x,x+u,\dots,x+Mu$ all blue if and only if the $M+1$ translates $\mathrm{RED}-ju$, $0\le j\le M$, do not cover $\R^2$. Since $\mathrm{RED}$ is $\Gamma$-periodic, this holds if and only if their images do not cover the torus $\R^2/\Gamma$, that is, if and only if they do not cover some (equivalently, every) fundamental domain of $\Gamma$. \end{lemma} Both methods cover the directions by finitely many closed intervals (``boxes'') and, for each box, cover a fundamental domain of $\Gamma$ by finitely many pieces, each of which is shown to lie in $\mathrm{RED}-ju(\theta)$ for one $j\le \MM$ and \emph{all} $\theta$ in the box. They differ in the direction boxes, the fundamental domain, the shape of the pieces and the enclosure of the red set, and in the code. \subsection{Method 1: strips and one-dimensional coverings}\label{sec:method1} This is the method of an earlier draft of this note, generalized to a rational period lattice, to $24$-gonal cells and to cells of different sizes. \emph{Direction boxes.} Fix $N$, let $\eta=\pi/(2N)$ and, for $0\le iU$). Since $Z+C(h_Z)$ is convex, a rectangle $[\sigma',\sigma'']\times[\tau',\tau'']$ lies in it if and only if its four corners do, that is, if and only if $[\sigma',\sigma'']$ lies in both sections at the heights $\tau'$ and $\tau''$. For each cell and each strip $[t_0,t_1]$ (below) the program first determines a candidate window $j_0\le j\le j_1$ of indices (omitting an index is conservative, see below), and then uses the single enlarged height range $[\tau',\tau'']=[t_0-j_1\eta,\ t_1+j_1\eta]$, which contains $[t_0-j\eta,\,t_1+j\eta]$ for every $j\le j_1$. With $a_Z=\max\bigl(L(\tau'-\tau_Z),L(\tau''-\tau_Z)\bigr)$ and $b_Z=\min\bigl(U(\tau'-\tau_Z),U(\tau''-\tau_Z)\bigr)$ put \[ I_{Z,j}=\bigl[\,\sigma_Z+a_Z-j+j\eta^2/2,\ \ \sigma_Z+b_Z-j\,\bigr]\qquad(j_0\le j\le j_1). \] If $s\in I_{Z,j}$ then $Q_j(s)\subseteq Z+C(h_Z)$, so for \emph{every} start $x=se+tn$ with $t\in[t_0,t_1]$ and every direction $\theta\in\Theta_i$ the point $x+ju(\theta)$ is red. (The enlarged range only shrinks the intervals, so it is conservative; empty intervals are discarded.) \emph{Strips.} Let $[t_{\min},t_{\max}]$ contain the range of $t$ over the fundamental parallelogram $F$ (Section~\ref{sec:colouring}), and cover it by consecutive closed strips $[t_0,t_1]$ of width $W$ (the last one possibly longer), each starting exactly where the previous one ends. For each strip let $[s_{\min},s_{\max}]$ contain the range of $s$ over the part of the closure $\bar F$ in the strip. These enclosures are computed as follows. Since $t$ is linear, its range over $\bar F$ is attained at the vertices $0,P_1,P_1+P_2,P_2$. The set $\bar F\cap\{t_0\le t\le t_1\}$ is a convex polygon whose vertices lie on the edges of $\bar F$, so its range of $s$ is attained on the edges: a point $v+\lambda(v'-v)$ of the edge from $v$ to $v'$ with $t\in[t_0,t_1]$ has $\lambda\in[0,1]\cap([t_0,t_1]-t(v))/(t(v')-t(v))$ (or $\lambda\in[0,1]$ if the enclosure of $t(v')-t(v)$ contains $0$), and then $s=s(v)+\lambda(s(v')-s(v))$; $[s_{\min},s_{\max}]$ is the hull of these four enclosures, and the strip is skipped only if all four are empty, in which case it does not meet $\bar F$. For $s\in[s_{\min},s_{\max}]$ let $f(s)$ be the least $j0$ and $s^2-|q-z|^2>0$. \emph{Arithmetic.} A first stage in floating point (not trusted) builds the tree and records for each leaf one disk, named by $(i,j,a,b)$ with $g=aP_1+bP_2$. A second stage (trusted) walks the tree again from the root grid, so that the leaves tile $G$ by construction and independently of the first stage; recomputes every leaf square exactly from integers; asserts $1\le i\le\NCELLS$ and $0\le j\le \MM$; and checks both inequalities of the test, with the radius $h_i-j\delta$ of the disk's own cell $i$, as certain statements in Arb ball arithmetic at $96$ bits, with $P_1$, $P_2$, $c_i$, $h_i$ as exact rationals, $\theta_l,\theta_h,\theta_m$ as exact binary numbers and $\cos\theta_m$, $\sin\theta_m$ as Arb balls. It checks that $\theta_l\le\theta_m\le\theta_h$ and that $\delta=\max(\theta_h-\theta_m,\theta_m-\theta_l)$ is computed exactly (an Arb ball of radius $0$), so that $h_i-j\delta$ is an Arb enclosure of the exact radius. Finally, the trusted stage checks in exact rational arithmetic that the boxes it has certified tile the direction interval: sorted, the first starts at $0$, each starts exactly where the previous one ends, and the last ends at the double nearest to $3.1416$, which exceeds $\pi$ (checked in Arb). This also checks that every bisection replaced a box by two halves covering it. No floating-point error bound enters the trusted stage. The inequalities are strict: they give $|q-z|