number-theory / Number Theory, Complete Sequences
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.
Temporal state
No reconciled state yet.
Append-only history
The problem statement is ambiguous: the limit-exists reading is claimed proved (Lean), while the convergence-from-hypotheses reading was disproved by a Lean-checked construction of Price that the community classes as a variant
Research memory
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.
The problem statement is ambiguous: the limit-exists reading is claimed proved (Lean), while the convergence-from-hypotheses reading was disproved by a Lean-checked construction of Price that the community classes as a variant
Evidence graph
No public relationships recorded yet.