⌊ξ(7/5)ⁿ⌋・⌊ξ(5/2)ⁿ⌋・⌊ξ(5/3)ⁿ⌋ に現れる合成数

01結果

累乗の整数部分についての三つの定理

1967 年、Forman と Shapiro は ⌊(3/2)ⁿ⌋ と ⌊(4/3)ⁿ⌋ に合成数が無限にあることを証明しました。その議論は、どんな ξ > 0 を掛けても成り立ちます。のちに Dubickas と Novikas が 5/4 を加えました。7/5 については最も近い整数、5/2 については 1 だけずらした数列が扱われていました。5/3 についても、Novikas の博士論文が扱っているのは最も近い整数です。本研究は、ずらさない整数部分そのものについて証明します。これまでに分かっていたこと、この論文で新しいこと →

定理 1 (i)7/5

どんな ξ > 0 に対しても、無限に多くの n で成り立つ

4290 = 2351113

1ステップ法のグラフ証明書、4段階
Lean：カーネルで検査

定理 1 (ii)5/2

どんな ξ > 0 に対しても、無限に多くの n で成り立つ

40112098026 = 23711131719232931

語ラベル法の証明書、10段階（素数 5 は不要）
Lean：健全性はカーネルで検査、有限の評価は native_decide

定理 1 (iii)5/3

どんな ξ > 0 に対しても、無限に多くの n で成り立つ

1484147626962 = 2371113171923293137

両方向に縮約する語ラベル法の証明書、10段階（素数 5 は不要）
Lean：健全性はカーネルで検査、有限の評価は native_decide

系 2どんな ξ > 0 に対しても、⌊ξ(7/5)ⁿ⌋、⌊ξ(5/2)ⁿ⌋、⌊ξ(5/3)ⁿ⌋ のどれにも合成数が無限に現れます。法と共通の約数をもつ 37 より大きい項は合成数で、項はいくらでも大きくなるからです。

定理 37/5 では、待ち時間の具体的な上限まで分かります。428 + 12L(P) 歩以内に合成数。

02位置づけ

これまでに分かっていたこと、この論文で新しいこと

この種の数列に現れる合成数は、1967 年から研究されてきました。左は、本研究が土台にしている、あるいは比較している先行研究です。右は、この論文が新しく加えたものです。

これまでに分かっていたこと

1967
Forman & Shapiro — ⌊(3/2)ⁿ⌋ と ⌊(4/3)ⁿ⌋ に合成数が無限にあることを証明しました。その議論は、どんな ξ > 0 を掛けても成り立ちます。
2005
Dubickas & Novikas — どんな ξ に対しても無限に多くの項を割り切る、具体的な素数の集合を与えました。対象は 3/2、4/3、5/4 と、ξ(7/5)ⁿ に最も近い整数、そして ⌊ξ(5/2)ⁿ⌋ − 1 です。整数の底 2〜6 も解決しました。本研究が刈り込みに使う事実、つまり本物の数列の繰り上がりは周期的にならないことも、すでにこの論文に含まれています。
2006
Dubickas — このような素数の集合を回避不能（unavoidable）と名づけました。整数の底では、5 のときと、b − 1 が平方因子をもつ b ≥ 3 のときには存在しません。2, 3, 4, 6 以外の整数の底では存在しない、と予想しました。
2009
Dubickas — 戻ってくる定理：適当な整数の漸化式で決まる数列は、ある決まった係数と互いに素などんな q を法としても、周期的にくり返します。そのため数列は、自分の大きな素数の項の倍数に何度も戻ってきます。特に、桁が周期的にくり返すと、合成数の項が必ず現れます。
2012
Novikas （博士論文） — どんな ξ > 0 に対しても、ξ(5/3)ⁿ に最も近い整数には、2 または 3 で割り切れる項が無限にある、と述べています。
2022
Dubickas & Jonuška — 底 7 では、その定理から、どんな有限個の素数の集合に対しても、どの項もそのどの素数でも割り切れないような ξ があることが従います。つまり回避不能な集合は存在しません。
2026
Stephan （プレプリント） — どんな ξ > 0 に対しても ⌊ξ7ⁿ⌋ に合成数が無限にあることを証明しました。未解決だった最小の整数の底です。証明には本研究と近い有限グラフの証明書を使い、Lean で検証しています。下で比較します。

この論文で新しいこと

定理 1。 ずらさない整数部分 ⌊ξ(7/5)ⁿ⌋、⌊ξ(5/2)ⁿ⌋、⌊ξ(5/3)ⁿ⌋ について、無限に多くの項を割り切る決まった素数の集合（回避不能な集合）を与え、そこから合成数が無限にあることを導きます（系 2）。これまで 7/5 と 5/3 は最も近い整数、5/2 は 1 だけずらした数列しか扱われていませんでした。
証明書。 有理数の底に対して、余りと小数部分のセルからなる有限のグラフを作り、繰り上がりが周期的にならないことを使って刈り込みます。語ラベル法では、道を正確に縮約し、語の途中のどの項でも素数を確かめます。5/3 では、入ってくる道が一本しかない頂点の鎖も縮約します。
定理 3。 7/5 の待ち時間の具体的な上限。
方法そのもの。 正規形、二つの障害、そして証明書に必要な追加の素数の下限。5/3 については、証明できる底の類に入ること、そして 23 以下の素数では足りないことを示す障害。
追加の結果。 再帰的な繰り上がりは合成数を生む（定理46。Dubickas の 2009 年の定理と同じ発想の、戻ってくる議論）。6/5 と 9/7 の高さまでの確認。(6t+3)/(6t+1) の停止問題。
検証。 別々に書いた二つの実装の出力を全要素で比較し、定理 1 の三つの部分と系 2 を Lean で形式化しました。

03試してみる

自分で ξ を選ぶ

好きな正の数を入力してください。各項を厳密に計算し、合成数には、それを割り切る最小の証明書の素数を添えます。項をいくら並べても定理の証明にはなりません（それを担うのが有限の証明書です）。それでも、印のついた項が現れ続ける様子は確かめられます。

ξ =

項数

3 この証明書の素数で割り切れる合成数証明書の素数では割り切れない合成数素数

04しくみ

例外を有限のグラフに閉じ込め、何も残らないまで刈り込む

仮に、⌊ξ(7/5)ⁿ⌋ のある項から先に、2, 3, 5, 11, 13 のどれでも割り切れない項しか現れないとしましょう。その先の項の並びを「例外のしっぽ」と呼びます（その項が素数とは限りません。たとえば 323 = 17 × 19 は、5つのどれでも割り切れません）。証明は、例外のしっぽが存在しないことを、次の三段階で示します。

繰り上がりは小さい

n 番目の項を Q_n と書きます。繰り上がり c_n = 5Q_n+1 − 7Q_n は、いつも −4 から 6 までの 11 個の整数のどれかです。ですから例外のしっぽは、有限個の局所的な規則に従います。4290 を法とする余り、小数部分、繰り上がりの組み合わせ方は、有限通りしかありません。

ξ = π の項 3, 4, 6, 8, 12, 16, 23 と、その繰り上がり。

有限のグラフが例外のしっぽを閉じ込める

有理数の底では新規比較：Stephan の底 7

状態は、項の 4290 を法とする余りと、小数部分が K 等分したどのセルに入るかを記録します。辺は、繰り上がりを添えた、規則にかなう一歩です。例外のしっぽは、どれもこの有限のグラフの中の無限の道になります。7/5 では、状態は最初 960 × 32 = 30,720 個です。

例外のしっぽがあれば、グラフの中を永遠に歩き続けます（黄色）。本物の数列が住めない成分を刈り込むと、何も残りません。

何も残らないまで刈り込む

非周期性の補題：Dubickas–Novikas 2005刈り込みの証明書：新規

無限に続く道は、やがてひとつの強連結成分の中にとどまります。その中のどの道でも繰り上がりが周期的になってしまうなら、その成分は取り除けます。本物の数列の繰り上がりは周期的にならないことが、Dubickas–Novikas（2005）にすでにある初等的な非周期性の補題で分かっているからです。残った部分はセルを四つに分けて細かくし、判定をくり返します。7/5 では第4段階で何も残らず、例外のしっぽは存在しません。

7/5 の4段階（論文の表1）。棒全体がその段階のすべての頂点で、左端の黄色が残す一つの成分です。ほかはすべて取り除かれます。残った頂点はそれぞれセルを4つに分けるので、次の段階の頂点はちょうど4倍になります。K = 2048 では何も残りません。

5/2：辺に語を載せる

新規

⌊ξ(5/2)ⁿ⌋ で 10 個の素数すべてを一度に入れたグラフを直接作ると、状態は 30,656,102,400 個になります。語ラベル法は代わりに、4 頂点と、−1, 1, 3 の3つだけの繰り上がりから始めます（2 で割り切れない項は奇数で、奇数の項の次の繰り上がりは奇数になるため）。辺に繰り上がりの語をまるごと載せ、枝分かれのない道を正確に縮約し、素数をひとつずつ加えます。そのたびに、語の途中のどの項でも余りを確かめます。作るグラフの最大は 2,856,938 頂点で、最後の出力は空になります。同じ方法で 7/5 の別証明も得られます。

5/2 の10段階の入力頂点数（表6、対数目盛り）と、各段階で加える素数。

5/3：両方向に縮約する

新規

⌊ξ(5/3)ⁿ⌋ では、2 でも 3 でも割り切れない項のあとの繰り上がりは −2, 2, 4 の三つだけで、セルは三つから始められます。ところが前向きの縮約だけでは、最後の素数 37 のグラフは 313,651,296 頂点になります。そこで 5/3 の証明書では、入ってくる道が一本しかない頂点の鎖も縮約します。そのような頂点を通る道は必ずその一本の矢印から来るので、前向きの一本道と同じように、語を後ろ向きにつなげられるのです。両方向に縮約すると、最大のグラフは 21,077,909 頂点に収まります。素数 37 の段では、ループをもつ 14,920 個の成分がすべて判定を通り、出力は空になります。

5/3 の10段階の入力頂点数（表17・18、対数目盛り）。灰色は前向きの縮約だけの場合で、37 の灰色の棒は数えただけで作っていません。青は証明書と同じく両方向に縮約した場合です。

近い親戚：Stephan による底 7 の証明

この論文の少し前、2026 年 8 月に、Ralf Stephan は、どんな ξ > 0 に対しても ⌊ξ7ⁿ⌋ に合成数が無限にあることを証明したプレプリントを公開しました。その方法は本研究といくつかの要素を共有しています。余り（2 · 3 · 5 · … · 31 を法とする）の有限のグラフを素数ひとつずつ加えて組み立てること、グラフのアルゴリズムの正しさを証明する代わりに検査器でランク関数を確かめること、そして有限の計算を native_decide で実行する Lean による検証です。違いは、周期的なふるまいの扱いにあります。

観点	Stephan（2026）・底 7	この論文・7/5、5/2、5/3
グラフの状態	余り	余りと小数部分のセル。本物の数列はどれも道になるが、道が数列になるとは限らない
どの道も周期的になる部分	残す。桁が周期的にくり返し、どの項も 31 以下の素数で割り切れない数列が実際にある	取り除く。本物の数列の繰り上がりは周期的にならない
最後に残るもの	371,702 状態の核	何も残らない
合成数が出る理由	Dubickas の戻ってくる定理（2009）：桁が周期的にくり返すと、合成数の項が必ず現れる	決まった素数の集合が、無限に多くの項を割り切る
どの ξ にも通用する素数の集合	底 7 では存在しない（Dubickas–Jonuška 2022）	7/5 は {2, 3, 5, 11, 13}、5/2 は {2, 3, 7, 11, …, 31}、5/3 は {2, 3, 7, 11, …, 37}
Lean	番号付きのすべての主張。有限の計算は native_decide	定理 1 と系 2。7/5 の 1 ステップの証明書はカーネルで、語ラベル法の実行は native_decide で

Stephan の計算は、この論文のどの証明にも使っていません。二つの方法の比較は論文の序論にあります。Stephan のプレプリント・その Lean ファイル

05待ち時間

次の合成数まで、どれだけ待つか

この論文で新規

定理 3 P = ⌊ξ⌋ > 13 ならば、0 ≤ n ≤ 428 + 12L(P) のどれかで gcd(⌊ξ(7/5)ⁿ⌋, 4290) > 1 となり、その項は合成数です。

どの項から数え始めても使えるので、13 より大きい項 Q_N から 428 + 12L(Q_N) 歩以内に合成数が現れます。合成数どうしの間隔は、項の対数程度より速くは広がりません。証明では、491,520 状態・891,990 本の矢印からなるもう一つのグラフを作ります。そのブロックは 65 段に積み重ねられ、道が各段で過ごせる時間を厳密に足し合わせます。

黄色：証明された上限。青：14 ≤ ⌊ξ⌋ < 10⁷ のすべての ξ を厳密に探索して見つかった最長の待ち。最長は 13 歩で、初めて現れるのは ⌊ξ⌋ = 8,887,499（そこでの上限は 548）。この探索は解説動画のために行ったもので、論文には含まれません。

06届く範囲と限界

この方法にできること、できないこと

この論文で新規

論文は、一般の底 a/b について、証明書の方法そのものについての定理も証明しています。

正規形

操作を正確に定めると、有限の証明書が存在するのは、あるセル数と、2ab を割らない素数のある有限集合について、ある一つのグラフのすべての巡回成分が位相判定を通るときに限ります。縮約、素数のべき、2ab を割る素数は、証明できる範囲を広げません。

大きすぎる分子

a ≥ 2 rad M のとき、この方法は決して終わりません。たとえば 4290 の素数だけでは、7/5 に近づいていく分数 (14k+1)/(10k+1) を、k ≥ 613 ではどれも証明できません。

素数の予算

二つの繰り上がりの語を組み合わせると、どのグラフでも排除できない擬軌道ができます。これを防ぐには素数を追加する必要があり、その積 R は次を満たさなければなりません。

2 と 5 以外の素数を使わない 5/2：時間をさかのぼる向きに、語 U = (1) と V = (3, 1) は区間 I = [1/3, 17/21] を、その中の重ならない二つの部分へ移します。語をどう無限に選んでも、空にならない入れ子の区間が続き、擬軌道になります（枠で囲んだ部分）。

障害であって、反例ではない

これらの結果が述べているのは、決まった手順が終わらないということです。何かの算術的な主張への反例ではなく、どの底でも合成数が有限個しかない、と言っているわけでもありません。この種の有限の証明書がどこまで届き、どこで届かないかの地図です。

5/3 を両側から

新規

5/3 の証明書から、5/3 が正規形の意味で証明できる底の類に入ることが分かります。そのグラフの 413,857,382,400 頂点を作る必要はありません。反対側からは、長さ 119 と 134 の二つの繰り上がりの語が、23 以下の素数で作るどのグラフにも残る擬軌道を与えます。ですから 5/3 のこの種の証明書には、29 以上の素数が必要です。29 で足りるかどうかは分かっていません。

07追加の結果と未解決問題

主定理の先へ

再帰的な繰り上がり

新規Dubickas 2009 と同じ発想

互いに素な a > b ≥ 2 について、軌道の繰り上がりの列が再帰的なしっぽをもつなら、その軌道には合成数が無限にあります（定理46）。

高さまでの確認

新規

6 < ⌊ξ⌋ ≤ 5⁴⁰ なら ⌊ξ(6/5)^j⌋ の最初の 41 項のどれかが、9 < ⌊ξ⌋ ≤ 7¹⁸ なら ⌊ξ(9/7)^j⌋ の最初の 19 項のどれかが合成数です（定理47）。

停止問題

新規

9/7 を含む分数の族 (6t+3)/(6t+1) では、すべての係数についての主張が、ある整数プログラムが必ず止まるかどうかに帰着します（定理58）。

五つの未解決問題

ほかの底と無限の族。 ほかにどの有理数の底が有限の証明書をもつか。一つの証明書で無限の族を扱えるか。付録 F で、証明できると分かっている底に 5/3 が加わりました。
有限の高さと、すべての係数。 6/5 と 9/7 の確認を、示した高さの先まで広げられるか。
再帰性。 素数だけが並ぶしっぽが、再帰的でない繰り上がりをもつことはあるか。
追加の操作。 もっと鋭い操作で証明できる底は増えるか。停止プログラムは必ず止まるか。
最小性と部分列。 素数の集合は最小か。5/3 について分かっているのは、29 以上の素数がどれか必要なことだけです。番号の等差数列に沿うとどうなるか。素数の項はどれほどまれか。

08検証

二重の確認：独立なプログラムと Lean

二つの実装

すべての有限の計算は、中心部分を別々に書いた二つの実装で行い、完全な出力を全要素で比較しました。個数やハッシュ値の一致ではありません。

1ステップ法（表1〜3）：コサラジュ法の A とタージャン法の B。B は A を読まずに仕様から書き、比較の前に出力を固定しました。97,772 頂点、168,474 本のラベル付きの辺、94,006 個の成分で一致し、B の検査プログラムはわざと壊した 13 個の証明書をすべて拒否します。
語ラベル法（表4・6・7）：29 組のグラフのファイルすべてが全要素で一致します。
5/3（表17）：証明書を最初に計算したプログラム（持ち上げたすべての辺と縮約を、実行しながら検査する）と、そのプログラムを読まずに補題から後ろ向きの縮約を加えた実装 B。20 個のグラフすべてがバイト単位で一致します。頂点 35,289,089、辺 48,786,290、文字 1,245,585,922。

Lean 4 による形式化

7/5：4段階の証明書を Lean のカーネルの中で検査します。論文の報告によれば、最終的な定理が依存するのは標準の公理 propext、Classical.choice、Quot.sound だけです。
5/2：手順全体を Lean の中で実行し、その健全性の定理はカーネルで検査します。有限の実行には native_decide を使うので、Lean のコンパイラとネイティブな実行も信頼することになります。Python や C++ の成功フラグ、グラフのファイル、ハッシュ値は信頼しません。
5/3：入方向の縮約を元の向きのまま証明し、後ろ向きのパスを加えたパイプラインのプリコンパイル版（WordExec）を native_decide で評価します（記録した環境で 657 秒、12.7 GiB）。信頼の種類は 5/2 と同じです。独立の監査はこの追加より前に行ったもので、5/3 は含みません。
形式化の外：定理3、第6〜8節と第10節、付録 B〜E、付録 F の系77・78、表の数値。そこでの根拠は、書かれた証明と A・B の比較です。

Lean で書いた定理 1 (i)

theorem floor_seven_fifths_visits (ξ : ℝ) (hξ : 0 < ξ) (N : ℕ) :
    ∃ n : ℕ, max N 1 ≤ n ∧ 1 < Int.gcd ⌊ξ * (7 / 5 : ℝ) ^ n⌋ 4290 := by
  exact finite_success_visits 7 5 4290 (by decide) (by decide) (by decide)
    (by decide) mainFiniteSuccess ξ hξ N

supplement/lean/MathPaper/Main.lean

再現する

# ファイルの同一性：パッケージの目録とファイルのハッシュ値
python3 -B reproduce.py verify
# 事前検査：単体検査と、選んだ小さな計算
python3 -B reproduce.py check --output /tmp/floor-paper-check
# すべての有限の結果。二つの実装を全要素で比較
python3 -B reproduce.py recompute --output /tmp/floor-paper-full

どのコマンドも決まった制限の中で動きます。コマンドごとに 600 秒と 8 GiB、全体では check が 1800 秒、recompute が 3600 秒です。recompute には 5/3 の計算が含まれ、約 10 GB のグラフのデータを書き出します。Lean の証明は、Lean 4.29.1 と固定した Mathlib で別にビルドします。REPRODUCE.md、COMPUTATION.md、FORMALIZATION.md を参照してください。

09解説動画

ナレーション付きの解説アニメーション

四本のアニメーションで論文を順にたどります（それぞれ英語版と日本語版）。高校数学の言葉で基本を解説する、日本語の長めの動画もあります。

1ステップ法

どの ⌊ξ(7/5)ⁿ⌋ にも、2, 3, 5, 11, 13 のどれかで割り切れる項が無限にある理由。有限のグラフを、何も残らなくなるまで段階ごとに刈り込みます。

日本語 · 約28分 English · 23 min

語ラベル法

⌊ξ(5/2)ⁿ⌋ と 10 個の素数。辺に語を載せた 4 頂点のグラフを、素数ひとつずつ持ち上げていきます。さらに ⌊ξ(5/3)ⁿ⌋ では、入口が一つしかない鎖も縮約します。最後に、方法ごとのグラフの大きさを比べます。

日本語 · 約37分 English · 30 min

待ち時間・限界・未解決問題

次の合成数はいつ現れるのか、証明書の方法はどこまで届き何がそれを止めるのか、そして何がまだ分かっていないのか。

日本語 · 約33分 English · 27 min

検証と Lean

独立な二つのプログラムと、機械が確かめる証明。それぞれの層が保証すること、しないこと。

日本語 · 約20分 English · 16 min

論文解説アニメーション（第1〜3章）

高校数学の知識で読める解説。付属の PowerPoint スライド（99 枚）もあります。扱うのは 7/5 と 5/2 で、5/3 は含みません。

日本語 · 約40分スライド（PPTX）

10論文・コード・引用

読む・再現する・引用する

論文（英語）PDF 論文（日本語）PDF DOI10.5281/zenodo.22997709 ソースコードGitHub Lean による形式化supplement/lean 有限の計算実装 A と B

引用

Yuri Odagiri. Finite graph certificates for composite terms in rational floor sequences. 2026. doi:10.5281/zenodo.22997709

@misc{odagiri2026finite,
  author    = {Odagiri, Yuri},
  title     = {Finite graph certificates for composite terms in rational floor sequences},
  year      = {2026},
  publisher = {Zenodo},
  doi       = {10.5281/zenodo.22997709},
  url       = {https://doi.org/10.5281/zenodo.22997709}
}

11成り立ち

この研究の成り立ち

論文の謝辞には、その成り立ちが詳しく書かれています。出発点は「すべてのミルズ数は無理数ではないか」という著者の問いで、本稿はその問いを解決するものではありません。

最初の予想のあと、数学的な展開、計算プログラム、文章、そして Lean による形式化は、すべて AI システムが行いました。途中の検討は AI による自動的な批評で、人間の数学者による独立した査読ではありません。Lean による形式証明が検査を通ることは、著者自身が確認しています。議論、再現可能な計算、形式証明は、読者自身が評価するよう求めています。

5/3 を加えたバージョン 3.0.0 では、あらかじめ選んだ底の証明を試みるのではなく、証明書をもつ底を探すという逆向きの探索を、著者が提案しました。探索と 5/3 の証明書は ChatGPT 上の GPT-6 Pro が作り、第二の実装、Lean による形式化、論文への統合は、Claude Code を通じて AI が行いました。

解説アニメーションとこのページも、AI の支援を受けて作成しました。

論文の開示の全文を読む →