The 4-color Rado number of x+y+c=z: general case

For a constant $c$, the 4-colour Rado number $R(c)$ is the least $N$ such that every colouring of $\{1,\ldots,N\}$ in four colours contains a monochromatic solution to $x + y + c = z$. Myers (Rutgers thesis, 2015, Conjecture 4.9) and Ahmed, Boza, Emamy-Khansary, Marin, Revuelta and Sanz (Math. Comp. 85, 2016, §5.5) conjectured $$R(c) = 40c + 41$$ for all sufficiently large $c$, with the small values $R(0) = 45$ and $R(1) = 83$ as exceptions. Previous methods reached individual values but not the general case. This claims the conjecture for every $c \ge 2$, by reducing it to three finite facts: the single base value $R(2) = 121$ and the unsatisfiability of two "spoke" templates. The reduction is formalised in Lean 4 and holds for every $D \ge 1$; the two templates are settled by SAT with DRAT certificates.

The claim is $R(c) = 40c+41$ for every $c \ge 2$, reduced to three finite facts: the base value $R(2) = 121$, and the unsatisfiability of a 321-position and a 521-position spoke template. The reduction is Lean-checked and holds for every $D \ge 1$; the two unsatisfiability results carry DRAT proofs. This completes the partial entry for the same conjecture, which proved it for roughly two thirds of integers via a scaling lemma; that lemma is now one of three legs, covering the branch where $d$ is divisible by 3. The supporting results are worth more than the headline for anyone deciding whether to believe it: the paper also shows every band relaxation is satisfiable, which is why previous attempts stalled, and that the affine method alone is exactly sharp and can never finish.