Let $A=\{1\leq a_1< a_2<\cdots\}$ be a set of integers such that $A\backslash B$ is complete for any finite subset $B$ and not complete for any infinite subset $B$. If $a_{n+1}/a_n \geq 1+\epsilon$ for all $n$, must $\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2$? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.