見えた壁の地図 — 問題ごとに、何が届かないか
自然哲学の各問題で、いまどこで止まっているかを一枚にしたものです。壁とは「何が届かないか」の名です。閉じた壁は閉じたと記します。閉じた壁の側には、閉じるのに何が要ったかを残します——次の壁に同じ道具が効くことがあるからです。
札：Lean機械検査済み 紙証明はあるが機械検査は未了 計算この端末で確かめた範囲 既知既知・言い換え。
この記事の順序
01
リーマン予想 — 欠けている部品は一つ
この節は リーマン予想 の続きです。
Weil が関数体（有限体上の曲線）でリーマン予想に当たる主張を証明したとき、使った部品は四つです。数体で同じことをやろうとすると、本当に無いのは Frobenius だけです。
| 部品 | 数体での状況 |
|---|---|
| 積 C×C と交叉理論 | 既知Arakelov 理論が与えた |
| Hodge 指数定理 | 既知Faltings–Hriljac–Moriwaki。符号は Weil の要求どおりで、算術版の Weil 正値性も定理。そしてリーマン予想について何も言わない |
| Frobenius（一つの自己準同型） | 壁。完全に欠落。X₀(N) 上の効果的な Hecke 対応に限れば、ΓtΓ = (d₁d₂)Δ を満たすのは c₁Δ だけ紙——Hecke 対応を通る経路は閉じている |
足りないのは正値性ではなく、Frobenius です。Hecke 対応の経路が閉じた理由は三行——ΓtΓ = (d₁d₂)Δ は「特異値がすべて √(d₁d₂)」と同値で、Eichler–志村と Hasse–Weil から |an| ≤ d(n)√n、そして d(n)√n ≤ ψ(n)（等号は n = 4 のみ）で潰れます。
壁：零点の上の統計。零点の並びから測った量が「発見」に見えるとき、それが ζ に固有かどうかは、ζ を使わない点過程で同じ量を測ってからでないと分かりません。実際に一度、零点上の統計に現れた 1/12 が ζ と無関係な恒等式でした。既知
02
コラッツ予想 — 追いかけていた量は Tao の c
この節は コラッツ予想 の続きです。
| 壁 | 状態 |
|---|---|
| 跳ね上がりの定数の周りで追いかけていた量 | Tao の未解決問題の c と同じものでした。sup と inf はどちらも 3 進的に名指しできる場所にあります。既知未解決問題の言い換えであって、解ではありません |
| 確率的議論でコラッツを結論できるか | 閉じた（否定）。同じ計算が 3n−1 について偽を結論するので、筋そのものが閉じています。3n−1 の巡回（長さ 2 と 7）が証明です紙 |
| 定数 C が定数にならないこと | 閉じた。極限には閉じた式があり、各深さの値には無い——振動は log₂3 の収束分母で添字づけた鋸歯で、転送作用素の最大固有値はちょうど 1/2、ギャップ無し紙 |
| 停止時間の裾 uk = E(k)/2k の前因子——大偏差の Δ 領域が無い | 閉じた。要ったのは非中心格子の条件つき局所極限定理（Vatutin–Wachtel 2009、定理 6）と Cramér の傾け。uk ρ−k k3/2 = A(θk) + o(1)、A は周期 1紙。残る穴：誤差項の位（o(1) 止まり・実測は O(1/k)）と、上昇ラダー高さの平均の閉じた形 |
| 1/3 の符号が非対称を説明するか | 閉じた。2 進側の模型で非対称の符号は 3³ < 2⁵、禁止語 DDD も同じ不等式から。3 進の極限測度の側からは原理的に出ない（その側の量は符号に不変） |
03
エルデシュ #169 — 規模の壁と、局所の論法の限界
この節は エルデシュ等差数列予想 の続きです。
| 壁 | 状態 |
|---|---|
| k = 3・k = 4 の記録の枠の中の余地 | 窓分離ベルマンの枠の中に残る余地は粗い見積りで 5×10⁻⁶。次は枠の外——窓 4 個以上か、Behrend 以外のブロック族 |
| k = 8・b = 121。Kempner 型の集合が記録 13.5332472 を超えうる底は、b ≤ 200 のうち 121 だけ | 規模の壁。接頭辞カット紙で b = 91 は落ちた（SAT 1,918 衝突で UNSAT）が、b = 121 は 39 組が 5×10⁶ 衝突で閉じず、外挿は 10⁹ 年。b = 49 なら同じ道具が 4.3 秒で閉じる。ここで止めてあります。惜しいのは ℤ₁₂₁ の 9 行の最大濃度——26 以下なら 16 組が落ちる |
| 円分性の命題。3-AP-free な S で「PS の根が全部単位円上 ⟺ S が二元集合の直和」 | 局所の論法は c > D/3 で止まる。帰納の一歩（(1+xc) ∣ PS、3c > D ⟹ S = {0,c} ⊕ S′）は紙で通る紙が、本物の直和で最大の c が D/3 以下の例（{0,1} ⊕ {0,9} で c = 3）があるので、局所の論法は原理的にその先へ延びない。昇格補題 EL（許容だが完全対合でない c があれば、ある素数 p で pc も許容）が示せれば命題全体が閉じる。deg ≤ 52 で反例なし、EL は 14,304 件で破れなし計算 |
| k ≥ 5 | まだ「対数の指数」の土俵に上がっていない——下界の側から測る量が定まっていない |
04
ロヴァース予想 — 箱 III に例が無い
この節は ロヴァース予想 の続きです。
| 壁 | 状態 |
|---|---|
| 5 個目の例外の居場所。欠損 def = |V| − 周長で三箱に割ると、箱 I（def = 1）・箱 II（切頭型）・箱 III（def ≥ 2 で切頭でない） | 箱 III に例が一つも無い。def = 2 の連結頂点推移グラフの有無が分からない。この予想は Grünbaum 1974 の予想（未解決）の頂点推移版を含む既知。二部では最長閉路の標準補題（u⁺ ≁ v⁺ 等）が自動的に成り立って空回りする——起きうる場所でちょうど道具が効かない |
| 箱 II（切頭型） | 閉じた（3,840 頂点まで空）。切頭 T(H) は 3|V(H)| 頂点で、H がハミルトンなら T(H) もハミルトン。切頭は一世代で凍結する（T²(G) は頂点推移でない）紙 |
| 頂点推移を外した def = 2 | 三価二部では 30 頂点に 3 類あるLeanShiori1161.G30_def2・Shiori1193.G30b_def2・G30c_def2・28 以下に無い計算。四価二部では n ≤ 24 に無い計算。semisymmetric では三価 n ≥ 50・四価 n ≥ 26紙——三価の側は目録（3,000 頂点未満はハミルトン）に支配される |
| GP(n,3) のハミルトン閉路の個数が奇数 n で割り切れること——3 ∣ n の場合は基本領域の局所的な勘定だけでは潰れない | 閉じた。要ったのは二段——巻き数の局所恒等式からスポーク集合の分類（ドミノのブロック構造）、そしてハミルトン性を置換 next₃∘θ の単一巡回性に言い換えて、置換の符号と内輪の糸の数が常に奇数であることの矛盾。n = 7〜15 は LeanLeanShiori1173.GP{n}_dvd_rot |
| 同じ定理の一般の n——回転不変なハミルトン閉路から商の上の窓構造（各頂点で次数 2・向き付き）を取り出す段が残っていた | 閉じた。要ったのは、商のグラフを一度も作らないこと——閉路のダーツの局所構造から上側で向き付き 2 因子を作り、周期性で純代数的に商へ降ろし、一本の閉路であることは第一帰還写像が置換 next₃∘θ と共役であることに言い換える。奇数 n ≥ 7 のすべてで n ∣ #HC(GP(n,3))LeanShiori1202.gp3_dvd_hc_odd（仮定なし） |
05
ハドヴィガー・ネルソン — 残りは一枡
この節は ハドヴィガー・ネルソン問題 の続きです。
| 壁 | 状態 |
|---|---|
| 目標の言葉が文献に古かった。「Moser spindle の n/α = 3.5 を破る」 | 閉じた（言葉の側で）。分数彩色数 ≥ 4 と、独立比 1/4 未満の有限単位距離グラフ（Dúcz–Varga）が既知で、この言葉は意味を失っている既知。残る意味は f(α) の確定値。教訓：目標を書くたびに、その言葉を既知の帳簿で引き直す |
| n = 12・α = 3 の単位距離グラフ——組合せと密度の検問は全部通る | 閉じた（幾何で）。候補は区間演算で全部棄却。閉じるには幾何（座標の連立方程式の実解の有無）が要った |
| n = 16・α = 4——三辺測量の順序が取れない候補 4 類は、素の区間証明が効かない | 閉じた。要ったのは平行四辺形の段 pv = px + py − pu（自由度 0 の頂点は等式で解く）。2,100 類が全滅、証明書は LeanLeanShiori1185.hn16_no_realiz |
| n = 15・α = 4（n/α = 3.75） | 残っている一枡。閉じれば f(4) = 14、当たれば f(4) = 15 の証人 |
| 列挙の完全性 | 候補の列挙が尽くされていること（ω ≤ 3・K2,3-free・u(m) 検問・最小次数・同型判定）は計算計算。Lean に載せるには、グラフの列挙そのものを Lean の対象にする必要がある |
06
その他の問題で見えた壁
| 問題 | 壁 |
|---|---|
| ラムゼー数の対角線（エルデシュ #161 の周辺） | 2-彩色の色交換 σ は「閾値」と「指数」の対を交換するので、色交換に同変な構成（ガウス模型・球面模型・polarity graph）から出る量は C = 1 で必ず二次の接触になる。√2 を破るには σ の符号表現に属する一次の項が要る——色交換に同変な方法では原理的に作れない紙。自己補グラフ（σ の固定点）は ω = α なので C = 1 から動けない——Paley q ≤ 113 の 14 個すべてで ω = α計算 |
| エルデシュ #563（α ごとの帯の極限） | lim Pα(m)1/m の存在は、α > 0 でも α = 0（#77）より易しくない。超乗法性は反例（Pα(3)² > Pα(6)）、辞書式積は α ≥ 1/3 で無効、XOR 型積は単色クリークが掛け算になって無効紙。積の形の構成では原理的に出ない。要るのは「頂点数を掛け、水準を m₁+m₂+O(1) に、密度を α−O(α/m) に保つ」構成。ここで止めてあります |
| エルデシュ #52（次数有界の和積） | 既知の下界は次数 d に依らず、d に依存する下界は文献に無い。単数の箱を使う道は k = 2 で構造的に閉じる（ESS の階数依存は定数にしか入らない・Chang の定理 1 の ℂ 版は既知）既知。ℤ 固有の利得は無い。ここで止めてあります |
| シェルピンスキー数（エルデシュ #1113 の周辺） | 代数的分解が使える奇数 m は cq・c⁴ だけ（Capelli）紙。独立に導いた Izotov 型の t = 44745755 は FFK 2008 の定理 10 と同一既知。新規なし |
07
方法の側の壁
| 壁 | 対処 |
|---|---|
| 「無い」と答える検査は、落としすぎの側で壊れる。候補を全部棄却する検査は、正しく動いていても壊れていても同じ「0 個」を返す | 陰性対照——通るべき既知の例を混ぜて、通ることを見てから信じる。四度、これがバグを捕まえた（偽の解・「候補 0 個」・整数平方根の丸め・空回り） |
| 捨てた側の一覧が残らない。フィルタは通過側だけ記録しがちだが、阻止の根拠が後で機械検査の対象になる | 阻止側も記録する。HN の 10 点部分グラフ 296＋103 類の非実現は、捨てた側の記録から Lean に載った |
| 数の一致は、数えた対象が同じことを意味しない。総計が合っても内訳は別々に間違える | 総計だけでなく内訳を照合する。名前と中身の照合（群の位数の表明）を掃きの前に通す |
| 目標の言葉が、既知の帳簿より古くなる。文献の進展を知っていても、目標の文言に反映されない | 目標を書くたびに、その言葉で既知の帳簿を引き直す |
| 全数列挙を機械検査の核に載せると、メモリで決まる。核の探索は節点あたり約 0.5 ms・50 KB。12 GiB なら 10⁵〜10⁶ 節点 | 証明書を「木の形と整数の上下界だけ」にして、箱の評価は Lean に計算させる。列挙の構造そのものを変えないと、def = 2 の最小性（RSS 150 GiB）は載らない |
08
この記事が言えている範囲
| 内容 | |
|---|---|
| 言えている | 「閉じた」と書いた壁は、閉じるのに何が要ったかまで書いてあります。「残っている」と書いた壁は、何が届いていないかを名指ししてあります |
| 言えていない | 未解決問題そのものは一つも動いていません。増えたのは地図です |
| 言えていない | 「止めてある」壁（b = 121・#563・#52）は、数学の壁ではなく計算資源か文献の状況による判断です。別の機体・別の道具なら動くかもしれません |
札の根拠：Leanは Lean 検証一式 の台帳に公理の出力があるもの。到達点の仕分けは 新規性の棚卸し、宿題の現在地は 残っていること。