math.NT — Number Theory
An unavoidable set of divisors for the nearest integers to ξ(3/2)^n
We prove that for every real ξ ̸= 0 the sequence of nearest integers [ξ(3/2)^n + 1/2], n ∈ N, contains infinitely many elements divisible by 2 or by 5. In particular, for ξ > 0 infinitely many of these nearest integers are composite. This is the nearest-integer counterpart of the theorem of Forman and Shapiro on [ξ(3/2)^n], for which Dubickas and Novikas give the unavoidable set {2, 5, 7, 11}; for nearest integers two primes suffice. The proof follows the method of Dubickas and Novikas: if 2 and 5 divide only finitely many terms, the sequence of operations is forced to become (A^2B^2)^∞, which is impossible by their Lemma 2. All results are machine-verified in Lean 4.