Finite graph certificates for composite terms in rational floor sequences

This record contains the preprint "Finite graph certificates for composite terms in rational floor sequences" by Yuri Odagiri, in English (paper-en.pdf) and Japanese (paper-ja.pdf). AbstractFor every real number ξ > 0, we give computer-assisted proofs that ⌊ξ(7/5)ⁿ⌋ is divisible by at least one of 2, 3, 5, 11, 13 for infinitely many positive integers n, and that ⌊ξ(5/2)ⁿ⌋ is divisible by at least one of 2, 3, 7, 11, 13, 17, 19, 23, 29, 31 for infinitely many positive integers n. Consequently both sequences contain infinitely many composite terms. The proofs represent an orbit avoiding the given primes by a walk in a finite labelled graph whose vertices record residues and fractional cells and whose edges carry signed carries. Components whose output depends only on a cyclic phase are excluded by an elementary nonperiodicity lemma. In the word-labelled construction the edges carry finite carry words; deterministic paths are contracted exactly, and each new prime is imposed at every intermediate time of a word. For the ratio 7/5 we also prove an explicit waiting-time bound: if P = ⌊ξ⌋ > 13, then some term with index at most 428 + 12L(P), where L(P) = min{h ≥ 0 : 5ʰ ≥ P + 2}, is divisible by one of the five primes. We then determine the reach of this certificate method: contraction, prime powers, and the primes dividing 2ab do not enlarge the class of finitely certifiable bases; the method cannot terminate when a ≥ 2 rad M; and the product R of the auxiliary primes not dividing 2ab must satisfy a ≤ 2R·J(N₀) for the Jacobsthal function J, whence R ≥ a^(1−o(1)) by an elementary bound. Every adopted finite computation was performed by two implementations with disjoint scientific cores, which agree element by element on all compared finite data. Lean proofs cover both divisibility theorems and their compositeness corollaries: the one-step proof for 7/5 is kernel-checked, and the word-labelled proofs combine kernel-checked soundness theorems with native_decide finite evaluations, which add trust in the compiler and native evaluation. Relation to earlier workForman and Shapiro (1967) proved that ⌊(3/2)ⁿ⌋ and ⌊(4/3)ⁿ⌋ contain infinitely many composite numbers, and Dubickas and Novikas (2005) gave explicit sets of primes for the bases 3/2, 4/3 and 5/4, together with results for the nearest integers to ξ(7/5)ⁿ and for the shifted sequence ⌊ξ(5/2)ⁿ⌋ − 1. The results for the integer parts ⌊ξ(7/5)ⁿ⌋ and ⌊ξ(5/2)ⁿ⌋ themselves are new; in the terminology of Dubickas (2006), they give unavoidable sets of primes for these two rational bases. The nonperiodicity lemma used in the proofs is already contained in the work of Dubickas and Novikas. For the integer base 7, Stephan (2026) proved that ⌊ξ·7ⁿ⌋ contains infinitely many composite terms for every ξ > 0, by a closely related finite-graph method also verified in Lean; the paper describes the shared ingredients and the differences. MaterialsThe TeX and Markdown sources, the two implementations of the finite computations, the Lean formalization, the reference data, and reproduction instructions with pinned environments are available in the source repository: https://github.com/ixixi/rational-floor-certificatesProject page with explanatory animations: https://ixixi.github.io/rational-floor-certificates/ Provenance and AI involvementThe author's sole mathematical contribution was the initial conjecture that every Mills number is irrational, a question this paper does not resolve. All subsequent mathematical development, programming, writing and Lean formalization were carried out by AI systems, without mathematically substantive guidance from the author. The author has not fully verified the mathematical arguments, but has personally confirmed that the Lean proofs are accepted by Lean. The acknowledgments of the paper describe the process in detail. Changes in version 2.1.0The account of earlier work was revised: it now introduces unavoidable sets (Dubickas 2006), compares the method in detail with Stephan's proof for base 7 (2026), and relates Theorem 46 to a theorem of Dubickas (2009). The acknowledgments were updated. The mathematical results are unchanged.