Sparse Polynomial-Weighted Expansions

Abstract

Let $b\ge 2$ be an integer, let $p\in \mathbb{Q}[x]$ be nonzero, and let $S\subseteq \mathbb{N}$ be infinite. We prove that if ${\sum }_{n\in S}p(n)b^{-n}$ is rational, then, for every fixed $0<\theta \le 1$, there is a constant $c>0$ such that $|S\cap (N,N+W]|\ge cW$ for all sufficiently large $N$ and every $N^{\theta }\le W\le N$. Thus rationality forces positive lower density; if $S=\{a_1<a_2<\cdots \}$ and $d=°p$, it also forces $a_{j+1}-a_j\le d{\log }_b{a}_j+O(1)$. In the binary linear case, the result implies the irrationality conjectured by Erdős whenever $a_j/j\to \infty$. The proof turns rationality into an integer carry orbit of polynomial height. Repeated gap words lock the orbit onto rational polynomial graphs, while the normalized highest Newton coefficient evolves by an expanding affine map. Denominator preservation, polynomial sampling, and an interior--exterior count then rule out sparse polynomial-scale windows.

arXiv commentThe formalization proof for lean4 is available at https://github.com/Hanziwww/erdos260