The positive irrational range conjecture

Let $\alpha>0$ be irrational, and let $f_\alpha$ be the function defined in the paper. The positive irrational range conjecture.

$$\{1,\ldots,\lfloor\alpha\rfloor\}\subseteq\operatorname{Range}(f_\alpha).$$

Together with the paper's established upper bound on the range, this would determine the principal positive values attained by $f_\alpha$ for every positive irrational $\alpha$. The statement is based on computational experimentation and is unproved.