主張の台帳
自然哲学の記事で言えたことを、一行ずつ並べた一覧です。各行に、どこまで確かめてあるか（札）、Lean で閉じたものはその定理名、文献との関係（既知性）、詳しく書いた記事を添えます。主張の状態が変われば、その行を書き換えます。
Lean機械検査済み（Lean 4 + mathlib、標準三公理以下、sorryAx・native_decide なし）
紙証明はあるが機械検査は未了
計算この端末で確かめた範囲。外に出す主張にはしない
既知既知の定理・言い換え・外の文献の確認
既知性の欄は三通りです。既知＝文献にある（または既知の結果の言い換え）。見当たらない＝探した範囲で同じ形の記述は見当たらない（範囲は各記事に書いてある）。劣る＝既知の結果より弱い。「—」は文献との照合をしていない行です。定理名の欄で「部品」とあるものは、紙の証明の一部の段だけが Lean で閉じていることを示します。主張の全体ではありません。札の基準と、外に出す主張の考え方は 進め方 にあります。
01
コラッツ予想
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| 3n+1 の乗数 3 は、この形の写像で唯一の「ちょうど臨界」（臨界乗数が整数になるのは 3 だけ） | Lean | Collatz.CriticalMultiplier.qcrit_eq_three・Collatz.CriticalMultiplier.qcrit_not_int_of_three_le | — | 3n+1 だけが、ちょうど臨界だった |
| Syracuse 写像の符号の共役：3m − 1 = 2ar ならば 3(−m) + 1 = 2a(−r)。二つの写像は n ↦ −n で共役 | Lean | Collatz.LadderHeight.syracuse_sign_conjugation | 既知 | コラッツ予想 |
| 3 進の極限測度は、単数の六類のうち mod 9 で類 7 に最小を持つ（最小は最大の倍の点） | Lean | Collatz.LambdaMeasure.lam_seven_min・Collatz.SubtractionSteps.min_over_six_classes（六類の間の倍の関係と m₇ ≤ m₄ の仮定の下） | 既知（mod 9 の水準は一次資料にある） | コラッツ予想 |
| 確率的な優マルチンゲールの筋は、3n−1 の巡回（長さ 2 と 7）によって閉じる：同じ計算が 3n−1 について偽を結論する | 紙 | — | 3n+1 だけが、ちょうど臨界だった | |
| 模型 ek+1 − ek = vk+1 − gk（v ≥ 1 だけを仮定）で、三歩続けて下がることはなく、非対称 A = (3·log₂3 − 5)/4 は負。どちらも 3³ < 2⁵ から | Lean | Collatz.no_three_consecutive_descents・Collatz.eK_three_step_lower・Collatz.asymmetry_negative・Collatz.three_cA_lt_five | 部品（Terras の分布・Sturmian 語）は既知。符号と禁止語が同じ不等式から出ることは見当たらない | 1/3 の符号が決めているもの |
| 停止時間の裾：ukρ−kk3/2 = A({ak}) + o(1)。A は周期 1・平均 10.892710・振幅 7.59%、フーリエ係数は閉じた形 | 紙 | 前因子の振動は一般論として既知。閉じた形とこの数列への適用は見当たらない | コラッツ予想 | |
| 定数 C = q²p/(ln2·(log₂3 − 4/3)) = 0.4215205965。極限には閉じた式があり、各深さの値には無い | 紙 | 既知（閉じた式は既出。固有構造の記述を加えた） | その定数は、まだ定数になっていない | |
| C の振動は log₂3 の収束分母で添字づけた鋸歯の重ね合わせ。転送作用素の最大固有値はちょうど 1/2、スペクトルギャップは無い | 紙 | — | その定数は、まだ定数になっていない |
02
リーマン予想
どの行もリーマン予想そのものについては何も言っていません。
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| 明示公式を両方向に——零点から素数の階段を、素数から零点の高さを。Λ = 0 ちょうど、という余裕の無さ | 既知 | 既知 | リーマン予想 | |
| Polymath15 の公開ログだけから Λ ≤ 0.19 が出る | 計算 | 既知 | 論文のログだけで、どこまで届くか | |
| Li の判定法の係数 λn は、零点の個数関数だけから作った合成の零点列でも n = 199 で 0.75% 以内に再現される（余裕は算術を検査していない） | 計算 | 見当たらない | Weil の二次形式の沈んだ固有値 | |
| Weil の二次形式も同じ検問を通る：Λ(k) の値の多重集合を保ったまま別の素数冪に並べ替えるだけで、最小固有値は ≈ −20 に落ちる（L = 2, 3, 4・乱数化 12 回中 12 回） | 計算 | 見当たらない | Weil の二次形式の沈んだ固有値 | |
| 定理 A：台を切った Weil 形式の、ε 以下に沈んだ固有値の本数の下界 n(WL; ε) ≥ Sh(T) − N(T) − 1 − 𝔇(ε/κ)。リーマン予想を仮定しない | 紙 | 部品：SunkCount.card_le_of_form_le・SunkCount.card_eigenvalues_le（有限次元の線形代数の段） | 本数がおよそ e2L で増えることは既知。下界を定理にした形は見当たらない | Weil の二次形式の沈んだ固有値 |
| 沈んだ本数の見積り n(L) = e2L − 7/8 − S(T*)（T* = 2πe2L）。9 枡で実測との差 0.39〜1.46 | 計算 | 見当たらない | Weil の二次形式の沈んだ固有値 | |
| Landau の次元定理の代わり：tr Q − tr Q² = (1/2π²) log(4LT) + O(1) | 紙 | 部品：TimeBand.compress_sub_sq・TimeBand.trace_compress_sub_sq・TimeBand.card_gt_ge_trace_sub | 見当たらない | Weil の二次形式の沈んだ固有値 |
| 跡の 1/k 則：ak = Λ/(π²k)（Λ = log(4LT) + γE + 1） | 紙 | 部品：TimeBand.cluster_identity（k ≤ 12 の個別の版） | 見当たらない | Weil の二次形式の沈んだ固有値 |
| 組合せ恒等式 Σn≥1 C(k, 2n) On = 2k−2 Hk−1（すべての k ≥ 1） | Lean | TimeBand.binom_oddH_identity | 見当たらない（初等的で、知られている可能性が高い） | Weil の二次形式の沈んだ固有値 |
| 定理 T（移送）：尾δ(f) ≤ 2e2L|δ|u(1+ω)/2‖f‖²、ω = (2/π)arctan(σ/|δ|) | 紙 | 部品：TimeBand.transfer_of_ratio・TimeBand.harmonic_measure_ge | 見当たらない | Weil の二次形式の沈んだ固有値 |
| この道はリーマン予想に届かない：上の結果はリーマン予想を仮定せずに成り立ち、その証明にも反証にも使えない | 紙 | 既知（正値性の道が単独では届かないことは Zhu, arXiv:2608.24827 も明記） | Weil の二次形式の沈んだ固有値 |
03
エルデシュ等差数列予想（#169）
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| 3 項等差数列を含まない有限集合で、逆数和が 3.0085385 を超えるものがある（1984 年の記録 3.00849 を超える） | Lean | APFree.BellmanRecord.erdos169_lower_record_939・APFree.BellmanRecord.setA939_apfree_and_lower | 見当たらない（一次資料 9 系統と照合） | エルデシュ等差数列予想 |
| 4 項等差数列を含まない有限集合で、逆数和が 4.439753369254541（Walker 2025 の記録を 15 桁で切り上げた数）を超えるものがある。下界 4.439753474215620 | Lean | APFree.FourTermRecord.setA4_apfree_and_beats_walker・APFree.FourTermRecord.setA4_lower_full | 見当たらない（Walker 2025 の表と照合） | エルデシュ等差数列予想 |
| k 項等差数列を含まない集合の入れ子補題（Wróblewski の補題 2 の k 一般の形） | Lean | APFree.Nesting.core_strong・APFree.Nesting.lemma2_four | 既知（補題の形は Wróblewski 1984） | エルデシュ等差数列予想 |
| Walker の Theorem 1.2 の一例：桁集合が mod b で 4 項等差数列を含まなければ K(S, b)+1 も含まない | Lean | APFree.FourTermRecord.KSet55_apfree | 既知（Walker 2025） | エルデシュ等差数列予想 |
| 3 項等差数列を含まず A ⊆ [x, ∞) なら Σ1/n ≪ (log x)−c | 既知 | 既知（Bloom–Sisask から二行） | エルデシュ等差数列予想 | |
| 接頭辞カット：Kempner 型の集合の逆数和が記録 13.5332472 以上なら、各 v₀ で |S ∩ [0, v₀]| ≥ mreq(v₀) | 紙 | — | エルデシュ等差数列予想 | |
| 円分性の命題の帰納の一歩：S が 3 項等差数列を含まず (1+xc) ∣ PS、3c > D なら S = {0, c} ⊕ S′ で S′ も同じ性質を持つ | 紙 | 見当たらない（近いのは de Bruijn 1950/53・Billey–Swanson・Filaseta–Kalogirou） | エルデシュ等差数列予想 | |
| 円分性の命題は deg ≤ 52（67,236 集合）で反例なし | 計算 | — | エルデシュ等差数列予想 |
04
ロヴァース予想
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| 既知の例外 4 個（K₂ を除く）はどれも「閉路は無いが路はある」。ケイリー版 9,805 個で反例なし | 計算 | 例外の一覧は既知 | ロヴァース予想 | |
| HGL₄(F₄)・SGL₆(F₂) のケイリーグラフはハミルトン閉路を持つ（証明書つき） | 計算 | — | 証明書の配布 | |
| 30 頂点の三価二部グラフで、連結・非ハミルトン・欠損 def = 2 のものが同型を除いて 3 類ある | Lean | CubicBipartite.ClassI.G30_def2・CubicBipartite.Search.G30b_def2・CubicBipartite.Search.G30c_def2 | 見当たらない | ロヴァース予想 |
| def = 2 の連結三価二部グラフの最小位数は 30（28 頂点以下に無い） | 計算 | 見当たらない | ロヴァース予想 | |
| 20 頂点の連結三価二部グラフで、周長 14・非ハミルトンのものがある | Lean | CubicBipartite.Search.G20_def6 | — | ロヴァース予想 |
| 一般化ペテルセングラフ GP(n, 3) のハミルトン閉路の個数は、奇数 n ≥ 7 のすべてで n の倍数 | Lean | GeneralizedPetersen.Descent.gp3_dvd_hc_odd | 見当たらない（OEIS にこの列は無い） | ロヴァース予想 |
| GP(n, 3) のハミルトン閉路の個数は n = 7, 9, 11, 13, 15 で 7, 9, 11, 26, 75 | Lean | GeneralizedPetersen.Small.GP7_hc_card ほか（GP9・GP11・GP13・GP15） | — | ロヴァース予想 |
| 切頭は一世代で凍結する（T(G) がハミルトン ⟺ G がハミルトン、T²(G) は頂点推移でない）。切頭型の 5 個目は 3,840 頂点まで無い | 既知 | 既知（3,840 頂点までの探索は計算） | ロヴァース予想 | |
| 辺推移な d-正則グラフの辺連結度は d。系：semisymmetric で def = 2 なら三価は n ≥ 50、四価は n ≥ 26 | 紙 | — | ロヴァース予想 | |
| 予想「def = 2 の連結頂点推移グラフは無い」は Grünbaum 1974 の予想の頂点推移版を含む | 既知 | 既知 | ロヴァース予想 |
05
ハドヴィガー・ネルソン問題
f(α) は、独立数が α 以下の単位距離グラフの最大点数。
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| f(3) ≥ 10、f(4) ≥ 14（Moser spindle ⊔ K₃・Moser spindle ⊔ Moser spindle） | Lean | HadwigerNelson.Witness.fGe_10_3・HadwigerNelson.Witness.fGe_14_4 | 見当たらない（専門家には自明でありうる） | ハドヴィガー・ネルソン問題 |
| f(2k) ≥ 7k・f(2k+1) ≥ 7k+3 | Lean | HadwigerNelson.Family.hn_lower_family | — | ハドヴィガー・ネルソン問題 |
| 11 点の候補 117 類・16 点の候補 2,100 類は、平面に単位距離で実現しない（非実現の証明書）。よって f(3) = 10、14 ≤ f(4) ≤ 15 | Lean | UnitDistance.Order11.no_realization・UnitDistance.Order16.no_realization | 見当たらない（専門家には自明でありうる） | ハドヴィガー・ネルソン問題 |
| 上の候補の列挙が尽くされていること（同型判定を含む）／f(5) ≤ 24 | 計算 | — | ハドヴィガー・ネルソン問題 | |
| 「α を最も増やさない点を足す」生成器の形は決まる。α = 2 なら n ≤ 7 | 紙 | — | ハドヴィガー・ネルソン問題 | |
| 分数彩色数の道は 4.36 で天井に当たる（単位距離を避ける可測集合の最良密度 0.22936 から） | 既知 | 既知 | ハドヴィガー・ネルソン問題 | |
| n/α > 4 の有限単位距離グラフは存在する | 既知 | 既知（Dúcz–Varga, arXiv:2606.28157） | ハドヴィガー・ネルソン問題 |
06
ホッジ予想
どの行も、ホッジ類の代数性については何も言っていません。
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| CM アーベル多様体のホッジ類は CM 型の組合せに落ちる（許容集合 T ⟺ すべての σ で |T ∩ σΦ| = |T|/2） | 既知 | 既知（Pohlmann 1968・Kubota 1965・Ribet 1980） | ホッジ予想 | |
| 「例外類は因子と Weil 類で生成される」がこの組合せ模型で壊れる最小次元は 8（g ≤ 7 は全数で反例なし）。その行は Q 上で実現する | 計算 | 見当たらない | ホッジ予想 | |
| 奇数次元で例外類が出る最小は g = 9：Q(ζ19) の CM 型 512 個のうち、退化かつ原始的なものは 54 個で、自己同型をこめてただ 1 類 | Lean | CMHodge.card_deg_prim | 見当たらない | ホッジ予想 |
| その多様体で、退化の重み d(A) は 3 以上（零化イデアルの元の ℓ¹ ノルムは 6 以上）。等号 d(A) = 3 は紙 | Lean | CMHodge.weight_ge_three | 見当たらない | ホッジ予想 |
| 余次元 3 の例外ホッジ類はちょうど 6 個（許容 |T| = 6 は 90 ＝ 因子の積 84 ＋ 例外 6） | Lean | CMHodge.Texc_card | 見当たらない | ホッジ予想 |
| WF(1) ≅ H¹(E)⊕3：ΦW = {0, 2, 4} は Q(√−19) から誘導される | Lean | CMHodge.PhiW_eq・CMHodge.level1_breakdown | 見当たらない | ホッジ予想 |
| H⁴(A×E) のホッジ類は 51 = 36 + 9 + 6 次元。因子の積が張るのは 45 次元 | Lean | CMHodge.count31_eq | 見当たらない | ホッジ予想 |
| 例外類 ξ の位置づけは既知の定理で確定する（分裂 Weil 類の引き戻し・絶対ホッジは無条件・代数性は Lefschetz 標準予想から） | 既知 | 既知（André 1992・Deligne 1982・Abdulali） | ホッジ予想 | |
| ξ に台を持つ因子を、テータ因子・孤立特異点・完全交叉（c = 2, 3）・単独の曲線・巡回被覆のヤコビアンから作る道は、どれも閉じる | 紙 | 部品：CMHodge.places_nonneg_of_mult・CMHodge.not_gorenstein・CMHodge.T0_not_generated_by_divisors | 見当たらない | ホッジ予想 |
| ξ の代数性は、一般化ホッジ予想 GHC(1, 3) の WF 部分とちょうど同値 | 紙 | GHC が CM で未解決であることは既知（Vial） | ホッジ予想 |
07
P 対 NP
この節に機械検査された主張はありません。
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| 三つの障壁（相対化・自然な証明・代数化）を同時に避けている既存の技法は、実質 Williams の方法だけ | 既知 | 既知 | P 対 NP | |
| 単調な側の相関下界の天井 n−1/2 は原理的で、帯を狭める道では窓に入れない | 紙 | 天井そのものは既知（Rossman） | P 対 NP | |
| 否定の前後にある単調な塊は、共有で得をする（n = 4 の全数で分解しない） | 計算 | — | P 対 NP | |
| 重み中立の植え込み測度では、床は落ちない | 紙 | — | P 対 NP | |
| 式サイズを真理値表の上の関数として見る：V₂(XORn) = L(XORn)、天井は n²（65,536 個の関数すべてで確認） | 計算 | — | 式サイズを、真理値表の上の関数として見る | |
| 鳩の巣原理 PHPn+1n の最小の木状導出反駁の葉の数は n = 1..4 で 3, 11, 43, 189（独立な二つの実装が一致） | 計算 | 見当たらない（OEIS に無い） | — |
08
小さな問題
番号はエルデシュ問題集（erdosproblems.com）の番号。
| 主張 | 札 | 定理名 | 既知性 | 記事 |
|---|---|---|---|---|
| #827：一般の位置の 7 点は、四つの三角形の外接半径がすべて異なる 4 点を必ず含む。6 点ではそうならない配置がある（n₄ = 7） | Lean | DistinctCircumradii.sInf_isGood_eq_seven | 既知（値は先行記録がある。こちらは別の道の証明を鎖の全体で機械検査したもの） | 外接半径の相異なる四点 |
| #827：一般の位置の 6 点で、どの 4 点部分集合にも外接半径の等しい三角形の対がある整数座標の配置。かつ n₄ ≤ 9 | Lean | DistinctCircumradii.seven_le_sInf_isGood_and_sInf_isGood_le_nine | 既知（n₄ ≤ 9 は Martínez–Roldán-Pensado 2015） | 外接半径の相異なる四点 |
| 78557 未満に被覆集合を持つ奇数 k は無い。リーゼル側も 509203 未満に無い | 計算 | 既知 | 未解決問題を、無作為に引く | |
| m×m 格子の相異距離 D を n/√log n で割った比は 1.11 前後で止まり、n/log n で割った比は伸び続ける（m ≤ 2048） | 計算 | — | 未解決問題を、無作為に引く | |
| #1087：頂点推移的な有限平面点集合は一つの円に乗る。この族からは log n の因子が出ない | 紙 | — | — | |
| #104：格子の 3-リッチ円は n1+o(1) 個。単一の格子からの Behrend 型の移送は効かない | 紙 | — | — | |
| #99：仮定 (J) の下で、最適配置は直径の対を c√n − 3 以上持つ | 紙 | —（Eppstein 2018 の二つの界を並べたもの） | — | |
| #40：g(N) = Nε は答えにならない。#39 の Erdős–Rényi 構成から 1 ≪ g(N) ≤ No(1) | 紙 | — | — | |
| #30：Sidon 集合の誤差項 b∞ ≤ 1.89715（折れ点を固定すると凸計画になり、証明書は接平面 1 枚） | 紙 | 劣る（Hou–Zhao, arXiv:2607.01169。この方法の天井でも届かない） | — | |
| #563：β(n, m) ≥ k ⟺ n < R(𝒢m, k)。極限の存在は Pα(m)1/m の収束と同値で、積の形の構成からは出ない | 紙 | 既知（Erdős–Pach 1983 の擬ラムゼー数の言い換え） | — |
09
残っている問い
上の主張の先に、まだ答えの出ていない問いです。どれも未解決問題そのものではなく、その手前の一段です。
| 問題 | 残っている問い |
|---|---|
| コラッツ予想 | 停止時間の裾の定理の機械検査と、誤差項の位 |
| エルデシュ等差数列予想 | k ≥ 5 を「対数の指数」の土俵に乗せること／円分性の命題の一般の場合（帰納の一歩は c > D/3 で止まる） |
| ロヴァース予想 | def ≥ 2 で切頭でない頂点推移グラフの有無（三価に限れば 1,280 頂点まで例は既知の 4 個だけ）／def = 2 の三価二部グラフの最小位数 30 の機械検査 |
| ハドヴィガー・ネルソン問題 | n = 15・α = 4 の一枡（閉じれば f(4) = 14、当たれば f(4) = 15）／候補の列挙の完全性の機械検査 |
| ホッジ予想 | 特異軌跡が完全交叉でない非正規な因子と、法束が分解しない 6 次元の軌跡。この二箇所だけが、ξ に台を持つ因子の候補として残る |
| P 対 NP | 否定の個数の梯子が止まる、幅 log log N の窓に入る道具 |
| #827 | k ≥ 5 の値 |
| シェルピンスキー数 | 被覆集合を持たないシェルピンスキー数はあるか（#1113） |
関連：進め方（札の基準と、外に出す主張の考え方）・Lean 検証一式（配布物と確かめ方）・記録の保管（この台帳の前身にあたる日付入りの一覧）
改訂 2026-10-02：新設。