ハドヴィガー・ネルソン問題 — 独立数 α 以下の単位距離グラフの最大点数 f(α)：f(3) = 10、f(4) は 14 か 15
平面の彩色数は 5・6・7 のどれかで、1950 年ごろからの上界 7 と 2018 年の下界 5 の間が空いています。この記事が扱うのはその本体ではなく、独立数を α 以下に抑えた有限の単位距離グラフは何点まで持てるかという量 f(α) です。f(3) = 10、14 ≤ f(4) ≤ 15——下界の証人と、上界を与える候補の非実現は機械検査済みで、候補の列挙が尽くされていることだけがこの端末の計算です。
Lean機械検査済み（Lean 4 + mathlib、標準三公理以下、sorryAx・native_decide なし。定理名を添える）
紙証明はあるが機械検査は未了
計算この端末で確かめた範囲。外に出す主張にはしない
既知言い換え・既知の定理・外の文献の確認
- この問題は何か
- 世界はどこまで来ているか — χ ∈ {5, 6, 7}・χf ≥ 4・独立比 1/4 未満の有限グラフ
- この端末で扱った量 — f(α)
- やったこと ①：f(3) = 10
- やったこと ②：f(4) は 14 か 15
- やったこと ③：道具と、副産物
- 残ったこと
- 出典と再現
この問題は何か
平面の点を、距離 1 の二点が同じ色にならないように塗るには、何色要るか。
（この最小数が平面の彩色数 χ(ℝ²)。距離 1 の点対を辺で結んだ無限グラフの彩色数）
有限の部分グラフ——平面の有限個の点を、距離 1 の対だけ辺で結んだ単位距離グラフ——の彩色数が χ(ℝ²) の下界を与えます（de Bruijn–Erdős）。上界 7 は正六角形の敷き詰めから。難しいのは、下界の側で「密に繋がった」有限グラフを作ることです。
世界はどこまで来ているか
| 問い | 状態 |
|---|---|
| χ(ℝ²) の値 | 未解決。5・6・7 のどれか。上界 7 は 1950 年ごろから、下界 5 は de Grey 2018（1,581 頂点の単位距離グラフ）既知 |
| 分数彩色数 χf(ℝ²) | ≥ 4（arXiv:2311.10069）。上界 4.36 は、単位距離を避ける可測集合の最良の既知密度 0.22936（Croft 1967）の逆数既知 |
| 独立比 α/n が 1/4 未満の有限単位距離グラフ | ある（Dúcz–Varga, arXiv:2606.28157）。χf ≥ n/α なので、上の下界と整合既知 |
| 独立数 2 の単位距離グラフの最大点数 | 7（Moser spindle。n/α = 3.5）既知 |
分数彩色数の道には天井があります。χf ≤ 4.36 なので、この道からは χ ≥ 5 は出ません。de Grey の 5 とは別の量を測っていることを、先に書いておきます。
この端末で扱った量 — f(α)
ここで単位距離グラフは、n 点の単純グラフ G と、相異なる点への配置 p : Fin n → ℝ² の組で、辺の端点だけが距離 1（非辺は制約なし）のものです。Lean での定義は Realiz G p := (∀ i j, G.Adj i j → sq2 (p i) (p j) = 1) ∧ Function.Injective p、FGe n α := ∃ G, (∃ p, Realiz G p) ∧ G.indepNum ≤ α（f(α) ≥ n の意味）。
f(α) は χf ≥ f(α)/α を与えます。ただし §02 のとおり、独立比が 1/4 を切る有限グラフの存在は既知なので、この量の意味は「比を下げること」ではなく、f(α) の確定値と、それを達成する最小のグラフにあります。
やったこと ① — f(3) = 10
下界。Moser spindle と三角形の非交和 Moser ⊔ K₃（10 点・14 辺）は単位距離グラフで、独立数は 3 です。LeanShiori1183.fGe_10_3 : FGe 10 3。座標は Q(√3, √11, √33) の中で、s3² = 3・s11² = 11・s3·s11 = s33 の三つの等式だけで各辺が閉じます。
上界。11 点で独立数 ≤ 3 の単位距離グラフは無い、を二段で言います。
- 候補の列挙（この端末の計算）：11 点・α ≤ 3 のグラフのうち、ω ≤ 3・K2,3 を含まない・最小次数の条件・u(m) 検問（m 点の単位距離グラフの最大辺数、OEIS A186705）を通る同型類は 117 類。計算
- 非実現の証明書（Lean）：117 類のそれぞれについて、
∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E p。LeanShiori1178.hn11_no_realiz（cands_card = 117）
したがって f(3) = 10——証明書は Lean、列挙の完全性は計算、と分けて読んでください。
やったこと ② — f(4) は 14 か 15
下界 14。Moser ⊔ Moser（14 点・22 辺）、独立数 4。LeanShiori1183.fGe_14_4 : FGe 14 4。一般に α(G₁ ⊔ G₂) = α(G₁) + α(G₂) と実現の非交和から、f(2k) ≥ 7k・f(2k+1) ≥ 7k+3 が k について一本で出ます。LeanShiori1192.hn_lower_family（indepNum_sum・fGe_add）。自明な下界で、新しさはありません。
上界 15。16 点で α ≤ 4 の単位距離グラフは無い。
- 候補の列挙：次数 5 の点 v₀ を取り、A = N(v₀)（5 点）、H = 非隣接の 10 点に分けて組み上げる。H は α ≤ 3 の 10 点グラフ（666 類）のうち最小次数 ≥ 3 の 571 類で、そのうち平面に実現しない 296 類を先に捨てて 275 類を回す。組み上げた候補は 2,100 類（真の同型類 993）。計算
- 非実現の証明書：2,100 類すべてについて
∀ p : Fin 16 → ℝ × ℝ, ¬ Realiz E p。LeanShiori1185.hn16_no_realiz（cands16_card = 2100。うち 2,093 類は単射性すら使わない強い形hn16_no_edges）。H フィルタが捨てた 296 類の非実現も Lean：Shiori1189.hn10_no_realiz（candsH_card = 296）。さらに 103 類が同じ機械で落ちる：hn10_no_realiz2（candsH2_card = 103）
したがって 14 ≤ f(4) ≤ 15。Lean の外に残るのは組合せの側だけです——列挙の完全性・枡ごとの同型判定・H の最小次数 ≥ 3 の導出。幾何の側（実現しないことの証明）は候補と H フィルタの両方が Lean に入っています。
n = 15・α = 4 は未決です。146 枡のうち 114 枡が完了し、生き残った候補は 0——残りの枡は三辺測量の自由段が 2 個ある（単位距離では 4 閉路が菱形になり、拘束が一本従属になる）ところで止まっています。閉じれば f(4) = 14、当たれば f(4) = 15 の証人です。計算 f(5) ≤ 24 も計算だけです。
やったこと ③ — 道具と、副産物
非実現の証明は三辺測量です。既に位置の決まった二点 x, y から単位距離にある点 v は、xy の中点を通る垂線上の二点に限られる（trilat_core：u ⊥ d なら位置は λ の一次式で書けて平方根が消える）。座標は 160 ビット固定小数点の区間演算で持ち、どの枝でも矛盾すれば候補は実現しません。自由度が残る頂点は、箱を二分する自由角つきの分枝限定で潰し、自由度 0 の頂点は平行四辺形の段 pv = px + py − pu（x, y の双方から単位距離にある二点は xy の中点について対称）で等式として解きます。列挙の側では 60°類の補題——どの 60°類も 3α 点しか張らない——が候補を先に落とします。
Lean の証明書は、木の形と整数二つだけです。枝ごとに λ の上下界を整数で渡し、箱そのものは Lean が計算します（lam_box は整数の掛け算だけ）。だから証明書は小さく、核の評価（decide +kernel）で閉じます。n = 16 の候補 2,100 類は代表 993 本の証明書と、残りを頂点写像で写す close_relabel で足りました。
副産物 — 座標の体について
Moser spindle の座標体 Q(√3, √11) の単位ベクトルは 9 方向だけで、その方向で作るケイリーグラフは 4-彩色可能です。de Grey の構成はこの体の中にありますが、階数 4 の群の外に出ています。計算 有限体 Fq²（q ≡ 3 mod 4）の単位距離グラフの彩色数からは体の側の必要条件が出ます——3 か 7 が剰余次数 1 の素を持つ体の上には、5 色を要する有限単位距離グラフは載りません（χ = 3 (q=3)・4 (7)・5 (11)・5 (19)・> 4 (23) を SAT で）。de Grey の体はこの必要条件を満たします。計算
残ったこと
動いた宿題の現在地は 残っていること にある。ここには現時点の未決だけを置く。
| 内容 | |
|---|---|
| 言えた | f(3) ≥ 10・f(4) ≥ 14・f(2k) ≥ 7k・f(2k+1) ≥ 7k+3Lean |
| 言えた | 11 点の候補 117 類・16 点の候補 2,100 類・H フィルタの 296＋103 類は平面に実現しないLean |
| 言えた | 候補の列挙が尽くされている ⟹ f(3) = 10・f(4) ≤ 15計算 |
| 言えない | f(4) の確定値。n = 15・α = 4 の一枡が未決 |
| 言えない | χ(ℝ²) について何か。この記事の量は分数彩色数の側にあり、その道は 4.36 で天井に当たる |
現時点の未決
| 未決 | どこで止まっているか |
|---|---|
| f(4) の確定 | n = 15・α = 4：枡 114/146・生存 0。残りは自由段 2 個の実現列挙 |
| 完全性の Lean 化 | 候補の列挙（v₀・A・H の分解と組み上げ）・同型判定・H の最小次数 ≥ 3 の導出。どれも組合せの側で、G をグラフとして Lean に持つ必要がある |
| n/α > 3.5 の最小グラフ | 比 3.5 を超える最小の有限単位距離グラフは何点か。n = 15・α = 4（3.75）が最初の候補で、そこが未決 |
出典と再現
| もの | 種別 | 出典・道具 |
|---|---|---|
| χ(ℝ²) ∈ {5, 6, 7} | 既知 | 上界は正六角形の敷き詰め。下界 5 は de Grey, Geombinatorics 28 (2018) |
| χf(ℝ²) ≥ 4 | 文献 | arXiv:2311.10069 |
| χf(ℝ²) ≤ 4.36 | 既知 | 単位距離を避ける可測集合の密度 0.22936（Croft 1967）の逆数 |
| 独立比 1/4 未満の有限単位距離グラフ | 文献 | Dúcz–Varga, arXiv:2606.28157 |
| f(2) = 7（Moser spindle） | 既知 | α = 2 なら n ≤ 7：R(3,4) = 9 と (3,4)-Ramsey グラフ 3 類の列挙・K2,3 の排除・C₈(2,3) の距離の矛盾 |
| f(3) ≥ 10・f(4) ≥ 14 | 機械検査 | Shiori1183.fGe_10_3・fGe_14_4。公理は Lean 検証一式 の台帳 |
| f(2k) ≥ 7k・f(2k+1) ≥ 7k+3 | 機械検査 | Shiori1192.hn_lower_family・indepNum_sum・fGe_add |
| 11 点の候補 117 類の非実現 | 機械検査 | Shiori1178.hn11_no_realiz・cands_card |
| 16 点の候補 2,100 類の非実現 | 機械検査 | Shiori1185.hn16_no_realiz・cands16_card・hn16_no_edges |
| H フィルタの 296＋103 類の非実現 | 機械検査 | Shiori1189.hn10_no_realiz・hn10_no_realiz2 |
| 候補の列挙の完全性（n = 11・16） | この端末で計算 | ω・K2,3・u(m)（OEIS A186705）・最小次数の検問と同型判定。陰性対照（実現するグラフを棄却しないこと）を通してある |
| n = 15・α = 4 | この端末で計算（未決） | 枡 114/146・生存 0 |
| f(5) ≤ 24 | この端末で計算 | — |
| 三辺測量の一歩・区間演算・平行四辺形の段 | 機械検査 | Shiori1178.trilat_core・lam_box・Shiori1185.par_core |
| Q(√3, √11) の 9 方向・Fq² の彩色数 | この端末で計算 | SAT |
この記事に、既知の枠を動かす数学はありません。f(α) の確定値 f(3) = 10・f(4) ∈ {14, 15} は探した範囲で活字に見当たりませんが、専門家には自明でありうる種類の値です。新しさは「探した範囲で見当たらない」までしか書きません。