Finite graph certificates for composite terms in rational floor sequences

Abstract

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, and that ⌊ξ(5/3)ⁿ⌋ is divisible by at least one of 2, 3, 7, 11, 13, 17, 19, 23, 29, 31, 37 for infinitely many positive integers n. Consequently all three 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 5/3 chains of in-degree one are also contracted exactly, which keeps the largest graph at about 2.1·10⁷ vertices instead of about 3.1·10⁸. 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. The base 5/3 belongs to the finitely certifiable class, and no certificate of this kind for 5/3 uses only primes up to 23. Every adopted finite computation, including the certificate computation for 5/3, was performed by two implementations with disjoint scientific cores, which agree element by element on all compared finite data; the 5/3 obstruction witness is checked by one direct program. Lean proofs cover all three divisibility theorems and their compositeness corollaries: the one-step proof for 7/5 is kernel-checked, and the word-labelled proofs, including the one for 5/3, 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. For the ratio 5/3, Novikas (2012) states that the nearest integers to ξ(5/3)ⁿ include infinitely many terms divisible by 2 or 3. The rounding and shift conventions matter: the present theorems concern the unshifted integer parts ⌊ξ(7/5)ⁿ⌋, ⌊ξ(5/2)ⁿ⌋ and ⌊ξ(5/3)ⁿ⌋. To the author's knowledge, the results for these integer parts are new; in the terminology of Dubickas (2006), they give unavoidable sets of primes for these three 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 implementations of the finite computations (including those for 5/3), 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 to the original work 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. For version 3.0.0, which adds the base 5/3, the author proposed reversing the direction of the search: to look for bases that admit a finite certificate instead of trying to prove preselected bases. GPT-6 Pro in ChatGPT carried out this search and found the certificate for 5/3; the second implementation, the Lean formalization and the integration into the paper were carried out by AI through Claude Code. The author has personally confirmed that the Lean proofs are accepted by Lean. The acknowledgments of the paper describe the process in detail. Changes in version 3.0.1Wording only. Sections 5.3, 9.2, 9.3 and 9.5 and Appendices A, D.5 and F.5 now describe the computation programs as the programs of this work: the programs written in the original research on which the paper is based, and the program with which the certificate for 5/3 was first computed. The theorems, proofs, computations and Lean formalization are unchanged. Changes in version 3.0.0Adds the base 5/3. Theorem 1(iii) and Corollary 2 now state that, for every ξ > 0, infinitely many terms of ⌊ξ(5/3)ⁿ⌋ are divisible by one of 2, 3, 7, 11, 13, 17, 19, 23, 29, 31, 37, and hence infinitely many are composite. The new Appendix F gives the certificate, which also contracts chains of in-degree one, shows that 5/3 belongs to the finitely certifiable class, and shows that every certificate of this kind for 5/3 uses a prime at least 29. The new Section 9.5 describes the computation for 5/3 by two implementations with disjoint scientific cores, which agree on all 20 graphs, and Section 9.4 now covers the Lean proof of the 5/3 theorem. The results for 7/5 and 5/2 are unchanged.