STEP 1694 (Phase 3) の scipy.milp/HiGHS ILP が F_3^3 で min = 13 optimal 到達 (gap 0%)。 これは solver 内部判定 = 「ソフトウェア証明書」 レベル。 藤本さん directive「上記の推奨」 応答で Phase 4 = Lean 4 formal verification に格上げ。 UB half (13 点の Kakeya 性) を native_decide で machine-check 完了。
def K13 : Finset (Fin 3 → ZMod 3) :=
{ ![0, 0, 1], ![0, 1, 0], ![0, 2, 1], ![0, 2, 2],
![1, 0, 0], ![1, 1, 0], ![1, 1, 1],
![2, 0, 1], ![2, 0, 2], ![2, 1, 0], ![2, 1, 1], ![2, 1, 2], ![2, 2, 1] }
ILP 出力 (STEP 1694 results-step1694-ilp.json) の 13 点。 sanity: 方向 (0,0,1) の line = {(2,1,0),(2,1,1),(2,1,2)} が K13 ⊆ (手計算 verify)。
theorem K13_is_kakeya : IsKakeyaFinite (n := 3) K13 := by
show ∀ v : Fin 3 → F, v ≠ 0 → ∃ a : Fin 3 → F, ∀ t : F, a + t • v ∈ K13
native_decide
theorem kakeya_F33_upper_bound :
∃ K : Finset (Fin 3 → F), IsKakeyaFinite (n := 3) K ∧ K.card = 13 :=
⟨K13, K13_is_kakeya, K13_card⟩
| declaration | axioms | badge |
|---|---|---|
K13 | propext, Classical.choice, Quot.sound | mathlib base |
K13_card = 13 | propext, Classical.choice, Quot.sound | axiom-free tier |
K13_is_kakeya | propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound | ★ machine-checked (native_decide 標準) |
kakeya_F33_upper_bound | 同上 | ★ machine-checked |
kakeya_F33_lower_bound | propext, sorryAx, Classical.choice, Quot.sound | Phase 4b target |
kakeya_F33_exact | 両者の union | Phase 4a partial |
| Layer | STEP | Type | F_3^3 result | F_3^4 result |
|---|---|---|---|---|
| formal LB (axiom-free) | 1687 Phase 1 | Lean 4 decide | 10 (Dvir LB) | 15 (Dvir LB) |
| structural proof | 1691 Phase 2a | Lean 4 (5 sub-lemma + 1 close) | 10 (LB stands as sorry-holding) | 15 (同上) |
| numerical UB (heuristic) | 1662 | Python greedy | - | 31 |
| numerical UB (ILP) | 1694 Phase 3 | scipy.milp/HiGHS | 13 (ソフトウェア証明書 optimal) | ≤ 28 (feasible) |
| machine-checked UB | 1700 Phase 4a (本 STEP) | Lean 4 native_decide | ≤ 13 (machine-verified) | (未実施、future STEP) |
kakeya_F33_lower_bound : ∀ K, IsKakeyaFinite K → 13 ≤ K.card は 現状 sorry。 実現戦略 4 option:
| Option | 手法 | Feasibility | Cost 見積 |
|---|---|---|---|
(a) Exhaustive native_decide | ∀ K, K.card = 12 → ¬ IsKakeyaFinite K を 17M subset 全探索 | 時間限界 | C(27, 12) × 55K ops ≈ 1T ops = 数時間〜数日 |
| (b) LP relaxation lower bound | mathlib linear algebra で ILP dual 論証を formal 化 | 高難度 | 数百行、 mathlib 独立 contribution 級 |
| (c) case-by-case combinatorial | F_3^3 特有 finite affine geometry の 手計算 argument | 可能だが 大変 | 数百-千行、 case explosion 管理 |
| (d) Dvir 定理 hook | STEP 1691 の Phase 2b 完了後 dvir_kakeya を hook | Dvir LB = 10 < 13 なので 直接使えない | Bukh-Chao 2021 sharp bound (Rei scope 外) 経由 必要 |
K13_is_kakeya は Lean 4 kernel + native_decide compiler chain で 検証済、 Lean.ofReduceBool + Lean.trustCompiler は 標準 native_decide axiom (mathlib 慣習)。sample_chosen_points が [:10] slice で 13 → 10 truncate、 私が 3 点 推測で 埋めた K13 は native_decide で 「Kakeya でない」 と 正しく 拒絶。 ILP を 再実行して 全 13 点取得 + JSON schema fix (chosen_points field 追加) で 正しい K13 land、 教訓: 「ILP output の JSON serialization が silent truncation で 誤 formal proof を 招く」 pattern (future 予防対象)。decide より weak (kernel evaluate では なく LLVM 経由 native execution)。#print axioms で 実測 記載 (Lean.ofReduceBool + Lean.trustCompiler を hidden せず)、 (3) Phase 4a title に 「UB」 明示、 kakeya_F33_exact は 「partial」 明記、 (4) LB 実現戦略 4 option を 表 で 明示、 Dvir との 相対関係 (Dvir LB=10 vs 実測 13 の gap) を 直接記載。