Ceiling orbits of rational bases are not P-recursive

Abstract

Let $p>q\ge2$ be coprime integers, let $x_{0}$ be a positive integer, and let $x_{n}=\lceil px_{n-1}/q\rceil$ be the ceiling orbit of the rational base $p/q$, with associated word $w_{n}=qx_{n+1}-px_{n}\in\{0,\dots,q-1\}$. We give an elementary proof that $w$ is not $P$-recursive: it satisfies no nontrivial linear recurrence with polynomial coefficients. At $p/q=3/2$ we prove the same for the orbit itself, which for $x_{0}=1$ is the sequence A061419 and whose parity is the minimal word $g_{3/2}$ of the rational base number system of Akiyama, Frougny and Sakarovitch. All results are formally verified in the Lean~4 proof assistant.

Keywords