A conjecture of Hopkins on golden Rado numbers

A 2-coloring of $\{1,\dots,N\}$ satisfies the golden mean shift if no two consecutive integers both receive color 1. For $1\le a\le b$, Hopkins defined the golden Rado number $R_0^{\varphi}(a,b)$ as the least $N$ such that every such coloring with $1$ colored $0$ contains a monochromatic solution of $ax+by=z$, and conjectured that $R_0^{\varphi}(a,\ell a)=a^2(\ell+1)^2$ for all positive integers $a$ and $\ell$. Hopkins proved the case $\ell=1$, and determined $R_0^{\varphi}(1,b)$ for every $b$; that evaluation shows the formula fails when $a=1$ and $\ell\ge2$. We prove the formula for every $a\ge2$ and $\ell\ge1$, which settles all the remaining cases of the conjecture. The lower bound is the coloring that gives color 1 exactly to the multiples of $a$ that are at least $a(\ell+1)$. The upper bound is a forcing argument: a descent in steps of $\ell$ shows that a residue $r\le\min(a,\ell)$ has color 1, and two families of solutions then make color 1 invariant under shifts by $\ell$ on an initial interval, which leads to a contradiction. The proof is elementary, and the theorem, both bounds included, is checked in the Lean proof assistant from the definitions. 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.