定理を支える大きな有限の計算は、どのように確かめられているのか。独立に書かれた二つのプログラムと、機械が確かめる証明。そして、それぞれの層が保証すること、しないこと。
論文 Finite graph certificates for composite terms in rational floor sequences（Yuri Odagiri）の第9節と付録 A、および補足資料を解説するアニメーションです。有限計算の八つの義務、独立な二つの実装と全要素の比較、Lean による形式化（7/5 のカーネルで確かめる証明書と、5/2 の語ラベル法の手順を native_decide で受け入れる方法）、形式化が扱わない範囲、そして再現の方法を扱います。1ステップ法・語ラベル法・待ち時間・限界・未解決問題の動画の続編で、英語版と同じ内容です。
画面の Lean のコードは supplement/lean からそのまま引用しています。示している公理への依存は論文が報告しているもので、#print axioms の出力の記録はリポジトリに含まれていません。論文の謝辞にあるとおり、数学・プログラム・Lean による形式化は AI システムが作成したもので、人間の数学者による独立な査読は受けていません。著者は読者に確かめるよう求めています。
ナレーション音声は Gemini 3.8 Flash TTS で作成し、字幕と同期して流れます。画面の日本語は Zen Old Mincho（SIL Open Font License）の字形で描いています。最初はウィンドウいっぱいに表示します。W で目次のあるページ表示に、F で全画面に切り替えられます。音声ファイルを読み込めない環境（HTML だけを手元で開いた場合など）では、ブラウザの音声合成で字幕を読み上げます。
論文: DOI 10.5281/zenodo.22997709 ／ ソースと再現資料: github.com/ixixi/rational-floor-certificates ／ 1ステップ法 ／ 語ラベル法 ／ 待ち時間・限界・未解決問題