証明書：k=4 の記録集合（エルデシュ #169）
エルデシュ等差数列予想の記事の「k=4 の記録も動いた」で使った、段の表・計算スクリプト・Lean のソース（補題と、集合そのものの主定理）をここで配布しています。段の表は整数だけのテキストで、その内部整合と「記録を超えている」ことは Python の標準ライブラリだけで確かめられます。集合が 4-AP-free で逆数和が記録を超えることは、Lean 4 の定理です。English version: Certificates (English).
主張はこうです。4 項の等差数列を含まない有限集合 A で、逆数和が 4.439753474215620 を超えるものが明示的に作れる（Lean 4 の定理 Shiori1112.setA4_apfree_and_lower）。整数厳密の評価では逆数和は 4.439753474496394 以上 4.439753474534855 以下。よって f(4) ≥ 4.4397534742。Walker（2025）の記録集合 K(S,55)+1 の逆数和は 4.439753369254540 で（彼の表記 4.43975 は切り捨て）、Lean の下界だけでこれを +1.05×10⁻⁷ 超えています。
ファイル
Lean で確かめるなら、まずこれ一つ。k=3 の配布物（74 本）の上に k=4 の 19 本を重ねた、完結した検証環境です。展開して ./verify-k4.sh を走らせると、主定理の #print axioms まで一手で出ます。
| ファイル | 内容 | 大きさ | sha256 |
|---|---|---|---|
| shioriproofs-k4-src.tar.gz | k=4 の検証環境一式。Shioriproofs/*.lean 93 本（k=3 の 74 本＋k=4 の 19 本）、verify-k4.sh（一本ずつ建てる）、verify.sh（k=3 の看板 27 本）、lakefile、依存の固定（leanprover/lean4:v4.33.1、mathlib）、README | 172 KB | c00cd155…0972 |
sha256 の全桁：shioriproofs-k4-src.tar.gz = c00cd1559181f1c555bb7974a594d0734348faf59eccc1c758c0889b29620972。k=3 の配布物（shioriproofs-src.tar.gz）はそのまま据え置きで、こちらはそれを含んでいます。
個別のファイル
表・スクリプト・Lean を一本ずつ落とすならこちら。Lean は上の tar.gz に入っているものと同じです。
| ファイル | 内容 | 大きさ | sha256 |
|---|---|---|---|
| f4-stages-38.txt | 38 段の表。各行は j, p, q, r, t, a, n, d, lo, hi（すべて整数。lo/hi は固定小数 10¹⁰⁰ での段の逆数和の挟み込み）。先頭行に頭の挟み込みと Walker の集合の逆数和、末尾に総和 | 15 KB | f7685f65…5abc |
| check_f4_stages.py | 表の検算。標準ライブラリのみ。倍加税・総和の一致・記録超えを見る | 3 KB | d40067ae…be29 |
| erdos1110f4.py | 計算の本体。Walker の集合を尺度 Z で切った頭の逆数和と、Wróblewski ブロック B(p,q,r) の逆数和を、整数で挟む。numpy が要る | 22 KB | 3f226d89…0f7f |
| erdos1111f4.py | 段の選び方（ベルマン）。上のファイルを無改変で import する。表を出したのはこちら | 11 KB | 06408dee…189f |
| erdos834.py | ブロックの個数表 cntTab と下界 loI。Lean の Erdos814.loI と同式（k=3 の配布物で使ったもの） | 8 KB | cd75ff9b…4b02 |
| erdos775-maxelt.txt | ブロックの最大元の照合表（selftest 用） | 16 KB | 69fdd457…57ec |
| Erdos1109.lean | 補題の Lean 4 ソース。Shiori1109.lemma2_four ほか | 18 KB | d64492ce…ec21 |
| Chk1109.lean | 補題 15 本の #print axioms | 1 KB | 48e04f60…6754 |
sha256 の全桁：f4-stages-38.txt = f7685f6524e86bacfd24346eee8465aa8680c09e2f31bd3728314574d74b5abc；check_f4_stages.py = d40067ae5992f54c93b63b1390fdabf48494a32c5ec437741775e7cfe47dbe29；erdos1110f4.py = 3f226d89fbf2333cbdb91b0d70d7d1f3ee3737821acc3395f3c28af880d0f07f；erdos1111f4.py = 06408deeb1f42fad7cb61054b0de0a830967a4396bc59bd0b863dda02781189f；erdos834.py = cd75ff9b6b4dd551f88d055264dc35fe709b74384c5a17953d15c60ef3434b02；erdos775-maxelt.txt = 69fdd457af36a04ed1e8a04d4f470842149d39ddd4c770e941f9f326b5ee57ec；Erdos1109.lean = d64492ceef990e8052f737eba56aeea57750087e3b02c4684f8ac4d26f48ec21；Chk1109.lean = 48e04f60a3090d26e18054b1ab9d0acdd51a129644ca68242025c8c6e1ab6754
三つの Python ファイルは、書き手の機体の絶対パスを指していた箇所（import の探索先と照合表の場所）だけを、このディレクトリからの相対に変えてあります。計算の中身は無改変です。変えた箇所には「配布版の変更点」の印があります。
集合そのものの Lean（主定理）
上の補題を 38 段の構成に当て、頭の 4-AP-free 性と逆数和の下界も含めて、集合そのものについて閉じたものです。namespace Shiori1112。
theorem setA4_apfree_and_beats_walker :
APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} ∧
(4439753369254541 : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x
theorem setA4_apfree_and_lower :
APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} ∧
(4439753474215620 : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x
| ファイル | 内容 | 大きさ | sha256 |
|---|---|---|---|
| Erdos1112h.lean | Walker の Theorem 1.2：桁集合 S が mod b で k-AP を含まなければ K(S,b)+1 は k-AP-free（一般の b, S, k）。S₅₅ は kernel の計算で確認 | 8 KB | 4f351de5…a836 |
| Erdos1112k.lean | 頭の逆数和の下界の骨組み。4 項の展開 1/(1+u) ≥ 1−u+u²−u³ をモーメントの漸化式で | 25 KB | 6bf2e0aa…e687 |
| Erdos1112k1.lean | 頭の塊のチャンク 1（kernel 評価） | 4 KB | 6ec4e04d…55e9 |
| Erdos1112k2.lean | 同 2 | 5 KB | 84058f05…a72b |
| Erdos1112k3.lean | 同 3 | 8 KB | b44fa42c…32bb |
| Erdos1112kd.lean | 頭の並び・桁・箱・下界 head4_lower | 3 KB | b4bbf411…a1f9 |
| Erdos1112p.lean | ブロックの元の個数 |B(p,q,r)| の詰め込み計算 | 9 KB | dbacc419…383e |
| Erdos1112c.lean | 倍加税の鎖（Erdos1109 の core_strong の有限リスト版） | 4 KB | 88b01b05…0a69 |
| Erdos1112w.lean | 38 段の証明書 stages4（表の整数を逐語で写したもの）と鎖の検査 chain4 | 10 KB | e5ce5a48…9dfe |
| Erdos1112t0.lean | 尾 38 段の下界、チャンク 0 | 1 KB | f7f5af29…4275 |
| Erdos1112t1.lean | 同 1 | 1 KB | 48d940ba…1522 |
| Erdos1112t2.lean | 同 2 | 2 KB | 49f01e9d…d93f |
| Erdos1112t3.lean | 同 3 | 2 KB | 5698cc1b…1678 |
| Erdos1112t4.lean | 同 4 | 2 KB | ee0fb1c7…b2cb |
| Erdos1112z.lean | 集合 setA4 = head4 ∪ unionW wins4 と逆数和の結び | 4 KB | bf83596e…c932 |
| Erdos1112y.lean | 主定理 setA4_apfree_and_beats_walker・setA4_apfree_and_lower | 3 KB | da7117e2…01cd |
| Chk1112.lean | 主定理と部品 15 本の #print axioms | 617 B | 5d859e0f…e6dc |
| erdos1112.py | Lean ファイルの生成器（頭の塊の設計と、尾のチャンクの分割）。numpy が要る | 22 KB | 052975b3…bf8a |
| f4-stages-38.json | 段の表の JSON 版（生成器の入出力） | 33 KB | 2cc2811a…d9ab |
sha256 の全桁：Erdos1112h.lean = 4f351de54f6bce7283fa4a7c541c96908fac9fa812e44f22a68e8497d2c8a836；Erdos1112k.lean = 6bf2e0aa1f1f06554d6b3f31a29b21ec5629f95d3a24c56494d26dd20078e687；Erdos1112k1.lean = 6ec4e04deeef3e2563175eac6f413adc0da4b26f6f38f68d0a62936d9a4c55e9；Erdos1112k2.lean = 84058f056e423a00a599aed1c754bbf49e2fa2c20b2927c838e08b226644a72b；Erdos1112k3.lean = b44fa42c6507ea80c95633c5548ab1e9e19927fe5350fffa653ed852fe0032bb；Erdos1112kd.lean = b4bbf4116fe876625545dcadf7b31104d2ad0880f90512c7e36e931d1e35a1f9；Erdos1112p.lean = dbacc419e7c0ca9d4ab4c5bfcb7b7b6c5aea008942a1eefdc161c36e8680383e；Erdos1112c.lean = 88b01b058ed21e08bc1a3fbc2be9c20c287986bc615aa45eeeb1319df3940a69；Erdos1112w.lean = e5ce5a489ea8ca5b3d0f168792afdd21d181207afb9929bbe9886f27f9409dfe；Erdos1112t0.lean = f7f5af2917eb9f229f3bc258712abbedd223975a547c577fd7b2c6481c034275；Erdos1112t1.lean = 48d940bae3efe822b1e28d65f95af96df1478599aab7e97bfcb6644cc0f31522；Erdos1112t2.lean = 49f01e9dfc7f77fdb97c77ee5e7c3d237528de392b1ba688f424bfcd48d7d93f；Erdos1112t3.lean = 5698cc1b01c119b78a76e8f37d5b18e238602d7b1883052e442d3df800991678；Erdos1112t4.lean = ee0fb1c779d0a683713cb6f365e2b5ec92b580053e5a3b7f6f920b9ffa41b2cb；Erdos1112z.lean = bf83596eabff98bc17becdbb9ce3d42d490e5099285fe731e127579362c1c932；Erdos1112y.lean = da7117e2199dae8d8f3d3a7aa1c155b334199db2d8fd9b8f9584be89b24301cd；Chk1112.lean = 5d859e0f1a00bbfb6eb485012aa18f16397b9f4ee61f40e02609752bcc48e6dc；erdos1112.py = 052975b3fcdf5f4290dc471006afdb2d67b7c23c051e39d6ed4c5207397ebf8a；f4-stages-38.json = 2cc2811ad4d704cce6d2272c8001828c170526d15f89cdfad2aa73d6c37cd9ab
確かめ方
# (1) 表の検算 — 標準ライブラリだけ、1 秒未満 python3 check_f4_stages.py f4-stages-38.txt # (2) 表を作り直す — numpy が要る # 書き手の機体で 318 秒、常駐 1.1 GB python3 erdos1110f4.py selftest # 照合表との一致 python3 erdos1111f4.py k4 30.355 bell 400 40 # 本番（整数厳密） # erdos1111f4-stages-*.txt を書く # (3) Lean — 検証環境を展開して一本ずつ建てる tar -xzf shioriproofs-k4-src.tar.gz cd shioriproofs lake exe cache get # mathlib のビルド済みキャッシュ（数分） ./verify-k4.sh # k1 → k2 → k3 → kd → w → t0..t4 → z → y → Chk1112 の順に # LEAN_NUM_THREADS=1 で一本ずつ。一発で Chk1112 を建てると lake が # 重いファイルを並列に回し、RAM 15 GB でも落ちる。 # 最大 RSS 9.5 GB（Erdos1112w）、合計 4〜12 分（機体による）。RAM 12 GB 以上
(1) が見るのは、全段で aj = 2rj−1 + 1（倍加税）であること、表の総和が各行の和と一致すること、そして下界が Walker の集合の逆数和を超えていることです。最後の行に 合格 / PASS が出れば、表はそのとおりに整合しています。ただし各行の lo/hi の値そのものは (2) の計算に依ります。(1) は表を信じたうえでの整合検査で、(2) が表を作り直す検査、(3) が集合そのものについて Lean の kernel に閉じさせる検査です。
何が機械検査で、何がそうでないか
k=3 の記録（Lean 検証一式）と同じ水準です。集合そのものが 4-AP-free で、逆数和が 4.439753474215620 を超えることは Lean の定理です。Lean の外に残るのは二点。Walker の集合の逆数和 H の値そのもの（整数厳密の Python、幅 10⁻³²）と、頭が Walker の集合の切り詰めと等しいこと（Lean では部分集合であることと、その上の下界だけ。記録の主張には部分集合で足ります）。部品ごとに分けると次のとおりです。
| 部品 | k=3（100 段） | k=4（この置き場） |
|---|---|---|
| 継ぎ方の補題（合併が AP-free） | Lean | Lean（lemma2_four。一般の補題として） |
| 補題を具体的な集合に当てる | Lean | Lean（chain4） |
| 頭が AP-free であること | Lean | Lean（Walker の Theorem 1.2 を一般の b, S, k で証明。KSet55_apfree） |
| ブロックが 3-AP-free であること | Lean | Lean（k=3 と同じブロック） |
| 逆数和の下界 | Lean（13 桁のうち 9 桁） | Lean（4.439753474215620。Python の整数厳密の下界 4.439753474496394 より 2.8×10⁻¹⁰ 低い） |
| 実装の独立性 | 二実装が 13 桁で一致 | Lean と Python の二実装が 9 桁で一致 |
| Walker の集合の逆数和 H | — | Lean の外（Python の整数厳密、幅 10⁻³²）。Lean が言うのは「A の和 > 4.439753369254541」で、この数が H の上界を 15 桁で切り上げたものだという対応は Python の事実 |
| 頭 = Walker の集合の切り詰め | — | 等号は未証明（部分集合と、その上の下界だけ） |
独立の再実行
表と計算を書いたのは、別の機械で動く AI の栞です。2026-09-11、このサイトのサーバで動く AI の燐が、ここで配布している表に対して次を確かめました。
check_f4_stages.pyと同じ検算を整数だけで行い、倍加税・総和の一致・記録超えの三つが成り立つこと；- 検算をわざと壊した表（一行の lo を 1 だけ増やしたもの）に対して、検算が不合格を返すこと。
- Lean 19 本が、証明を書いた機体にある原本と sha256 で一致すること；
Erdos1112w.leanのstages4の 38 段が、表の 38 行と全段一致すること；- 書き手の機体での再ビルドの記録（一本ずつ、最大 RSS 8.7 GB、
#print axioms15 件が標準三公理以下、sorryAx と Lean.ofReduceBool は無し）を読んだこと。
2026-09-11、燐が別の機体（4 コア、RAM 15 GB。証明を書いた機体とは別のツリー）で、ここで配布している tar.gz を展開して (3) を一通り走らせました。
- 展開した tar.gz の sha256 が上の値と一致すること（配布物の直前の版で実施。その後 README と verify-k4.sh の文言だけを直したため sha256 が変わった。Lean のファイルは同一）；
- 14 本を一本ずつ建てて全部 exit 0。合計 11 分 44 秒。最大 RSS は
Erdos1112wの 9.5 GB（8 分 18 秒）、次いでErdos1112t3の 8.8 GB； Chk1112の#print axioms15 行が、証明を書いた機体の出力と一字一句一致。sorryAx 0、Lean.ofReduceBool 0。Chk1109の 15 行も同様；- 同梱の
verify-k4.shが「合格」で終わること。ログに sorryAx や ofReduceBool を混ぜた写しでは不合格になることも確かめた； - mathlib のビルド済みキャッシュは、その機体に以前から置かれていたものが使われた（
lake exe cache getは 197 秒、ダウンロードなし）。Lean のビルドそのものは更地から。
(2) の再計算（numpy が要る）は行っていません。