STEP 1710 — F_3^4 Kakeya UB ≤ 28 restore (Phase 4a-F34-28)
2026-09-03 (JST) · tab rei-aios-26 · data/lean4-mathlib/CollatzRei/KakeyaF34UB28Formal.lean · mathlib v4.27.0 + native_decide · K28 (28 点集合) を IsKakeyaFinite で 0-sorry machine-checked · lake build 13s
由来
藤本さん directive「推奨」 応答 の 第 3 段。 STEP 1694 の 600s ILP run で 一度 28-incumbent を 得ていた が JSON persist bug で lost、 STEP 1704 の 300s re-run では 29-incumbent (persisted、 machine-checked)。 本 STEP 1710 は script fix (STEP 1704 で 実施) 後 の **700s re-run で 28-incumbent restore 成功**、 これを Lean 4 で native_decide machine-check、 F_3^4 UB を 29 → 28 に 一段 tighten。
実装
K28 (28 点集合、 全4次元)
def K28 : Finset (Fin 4 → ZMod 3) :=
{ ![0,0,1,0], ![0,0,2,2], ![0,1,1,0], ![0,1,1,2],
![0,1,2,2], ![0,2,0,1], ![0,2,1,0], ![1,0,0,2],
![1,0,2,0], ![1,0,2,1], ![1,1,0,1], ![1,1,0,2],
![1,1,1,1], ![1,1,2,1], ![1,2,0,1], ![1,2,0,2],
![1,2,1,0], ![2,0,0,0], ![2,0,1,0], ![2,0,1,1],
![2,0,1,2], ![2,0,2,1], ![2,0,2,2], ![2,1,0,2],
![2,1,1,0], ![2,1,2,2], ![2,2,0,1], ![2,2,2,0] }
STEP 1710 の scipy.milp ILP re-run (700s time limit, HiGHS solver、 status = time_limit_incumbent、 gap ≈ 46%) の 出力 28 点、 全 point 埋込。
UB proof (0 sorry, machine-checked, 13s)
theorem K28_is_kakeya : IsKakeyaFinite (n := 4) K28 := by
show ∀ v : Fin 4 → F, v ≠ 0 → ∃ a : Fin 4 → F, ∀ t : F, a + t • v ∈ K28
native_decide
theorem kakeya_F34_upper_bound_28 :
∃ K : Finset (Fin 4 → F), IsKakeyaFinite (n := 4) K ∧ K.card = 28 :=
⟨K28, K28_is_kakeya, K28_card⟩
Axiom profile
| declaration | axioms | badge |
|---|
K28 | propext, Classical.choice, Quot.sound | mathlib base |
K28_card = 28 | propext, Classical.choice, Quot.sound | axiom-free tier |
K28_is_kakeya | propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound | ★ machine-checked |
kakeya_F34_upper_bound_28 | 同上 | ★ machine-checked |
F_3^4 UB progression
| STEP | Method | UB | Status | Machine-checked? |
|---|
| 1662 (rei-aios-80) | Python greedy 30 trial | 31 | heuristic best | - |
| 1694 (Phase 3) | ILP 600s | 28 | persist bug で lost | - |
| 1704 (Phase 4a-F34) | ILP 300s + native_decide | 29 | persisted | ✓ K29 |
| 1710 (本 STEP) | ILP 700s + native_decide | 28 | persisted + restored | ✓ K28 |
掛谷 arc 累積 progression
formal LB (axiom-free) ≤ true min |K| ≤ UB (native_decide)
F_3^2: 6 (formal) ≤ 7 (proven exact) ≤ 7
F_3^3: 10 (formal) ≤ 13 (proven exact) ≤ 13 (machine-checked STEP 1700)
F_3^4: 15 (formal) ≤ true ≤ 28 (machine-checked、 本 STEP)
Honest scope
- UB のみ machine-checked: 「min |K| ≤ 28」 は Lean 4 で proven、 「min |K| ≥ 16」 は依然 unproven (Dvir LB = 15 stands as formal floor)。 exact 判定 未実現。
- 29 vs 28 は heuristic path 差: どちらも optimal ではない、 STEP 1704 の K29 も STEP 1710 の K28 も HiGHS 内部 randomness の path 差、 gap 46% 残る。
- 「F_3^4 exact min = 28」 は 主張しない: bracket [15, 28] 中身 依然不明、 true min は 別 solver or 数時間 batch で closable。
- native_decide 依存 axiom:
Lean.ofReduceBool + Lean.trustCompiler、 mathlib 標準 「computational proof」 tier、 「axiom-free」 とは 呼ばない。
- K29 (STEP 1704) は historical artifact として 保持: KakeyaF34UBFormal.lean は 未削除、 STEP boundary の 明示的 record。
- Ellenberg-Erdälyi 先行研究 audit 未実施: F_3^4 min の 既知 bound value との 比較 未 verify。
Failure mode (機械学習用 dataset)
- What could go wrong: (1) 「28 は new record」 と 主張 → 実は STEP 1694 で 既に 得ていた (persist bug)、 「restored」 accurate 表現、 (2) 「700s で 必ず 28」 と 誤解 → HiGHS random path で 別 run では 27 or 29 も 可能、 (3) 「native_decide 13s = fast enough」 と 過信 → F_3^5 or larger で cost 予測 必要、 (4) 「K28 が K29 を 完全 supersede」 と 誤解 → K29 は STEP 1704 の evidence として artifact 保持、 削除しない。
- Prevention: (1) 「restore」 用語 使用、 STEP 1694 → 1704 → 1710 の 3 step progression 明示、 (2) HiGHS heuristic path randomness を 表 で 明示、 (3) build time 実測記載、 dimension 拡張 cost 予測、 (4) K29 file (KakeyaF34UBFormal.lean) は 未削除、 STEP boundary preserve。
- Recovery: (1) 27 or better を 狙うなら ILP 1800s+ or 別 solver、 (2) exact 化 は 別 STEP、 (3) F_3^5 対応 は 別 solver (Gurobi/CPLEX) 推奨。
次候補
- F_3^4 optimal 追求: 別 solver (Gurobi academic trial) or ILP 数時間 batch で [15, 28] 収束、 optimal 到達
- Ellenberg-Erdälyi 先行研究 audit: F_3^3 = 13 / F_3^4 min の 既知値 との 比較 verify
- Phase 4b LB (F_3^3 exact 化): K.card ≤ 12 → ¬ Kakeya の formal proof (4 option 検討済)
- Phase 2b: Dvir main の 4 sub-lemma 実 proof (mathlib upstream 級)
- F_3^5 exploration: 3^5=243 points、 grep 手法 spelunking、 別 solver 必須
参照 STEP: 1687 (skeleton) + 1691 (sub-lemma) + 1694 (ILP first、 28 lost) + 1700 (F_3^3 formal UB) + 1704 (F_3^4 formal UB=29) + 1710 (本 STEP F_3^4 formal UB=28 restore) · main file data/lean4-mathlib/CollatzRei/KakeyaF34UB28Formal.lean · AxiomCheck KakeyaF34UB28FormalAxiomCheck.lean · ILP re-run data/kakeya/results-step1710-f34-restore.json.