Integer-valued sequences near polynomial branches are polynomial on progressions

Fix natural numbers $n$, $w$, $L$, $m_0$ and $D$ with $D > 0$, a complex number $\mu$, and a family $P : \mathrm{Fin}\,n \to \mathbb{C}[t]$ of complex polynomials each of degree at most $w$ (in the sense that $\deg P_i \le w$ for every $i$, with the degree taken as a natural number). Let $x : \mathbb{N} \to \mathbb{Q}$ be a sequence subject to two conditions on its tail: for every $m \ge m_0$ the rational number $D\,x_m$ equals an integer, and for every $m \ge m_0$ there is an index $i$ with $\lvert x_m - P_i(\mu m)\rvert < 1/(D\,2^{w+1})$, the absolute value being that of $\mathbb{C}$, where $x_m$ is viewed in $\mathbb{C}$ and $P_i$ is evaluated at $\mu \cdot m$. The conclusion is that there exist natural numbers $a$ and $b$ with $a > 0$ and $b \ge m_0$, and a polynomial $G \in \mathbb{Q}[X]$ of degree at most $w$, such that $x_{b + aj} = G(j)$ for all natural numbers $j < L$. Thus the sequence agrees exactly with a single rational polynomial of degree $\le w$ along an arithmetic progression of any prescribed length $L$ inside the range $m \ge m_0$; no bound on $a$ or $b$ is asserted.

This is the combinatorial and finite-difference step of Dörge's elementary proof of Hilbert's irreducibility theorem: a sequence whose tail is $D$-integral and everywhere close to one of finitely many polynomial branches is genuinely polynomial along long arithmetic progressions. It is used in the proof of Polynomial.exists_forall_not_isRoot_of_weighted, where it rules out rational roots of specialisations along progressions.