STEP 1704 — F_3^4 Kakeya UB ≤ 29 formal Lean 4 machine-check (Phase 4a-F34)
2026-09-03 (JST) · tab rei-aios-26 · data/lean4-mathlib/CollatzRei/KakeyaF34UBFormal.lean · mathlib v4.27.0 + native_decide · K29 (29 点集合) を IsKakeyaFinite で 0-sorry machine-checked · lake build 14s
由来
藤本さん directive「上記の推奨」 応答 の 第 2 段。 STEP 1700 (Phase 4a-F33) で F_3^3 UB = 13 を native_decide で 格上げした 手法 を F_3^4 に 拡張。 STEP 1694 の ILP は F_3^4 で 600s time limit で incumbent = 28 (未 persist、 JSON slice bug で lost)、 STEP 1704 では script fix 後 の 300s 再実行 で incumbent = 29 点、 これを 全 point 保存 + Lean 4 で machine-check。
実装
K29 (29 点集合、 全4次元)
def K29 : Finset (Fin 4 → ZMod 3) :=
{ ![0,0,1,0], ![0,0,2,2], ![0,2,0,0], ![0,2,0,1],
![0,2,0,2], ![0,2,1,0], ![0,2,1,2], ![1,0,0,2],
![1,0,1,2], ![1,0,2,1], ![1,0,2,2], ![1,1,0,1],
![1,1,0,2], ![1,1,2,0], ![1,1,2,2], ![1,2,0,0],
![1,2,0,2], ![1,2,1,1], ![2,0,0,0], ![2,0,0,1],
![2,0,0,2], ![2,0,1,1], ![2,0,2,0], ![2,0,2,2],
![2,1,0,1], ![2,1,1,2], ![2,1,2,0], ![2,2,1,2],
![2,2,2,1] }
STEP 1704 の scipy.milp ILP re-run (300s time limit, HiGHS solver、 status = `time_limit_incumbent`、 gap ≈ 46%) の 出力。 全 29 点、 Lean-ready matrix literal 形式で 直接埋込。
UB proof (0 sorry, machine-checked)
theorem K29_is_kakeya : IsKakeyaFinite (n := 4) K29 := by
show ∀ v : Fin 4 → F, v ≠ 0 → ∃ a : Fin 4 → F, ∀ t : F, a + t • v ∈ K29
native_decide
theorem kakeya_F34_upper_bound :
∃ K : Finset (Fin 4 → F), IsKakeyaFinite (n := 4) K ∧ K.card = 29 :=
⟨K29, K29_is_kakeya, K29_card⟩
Axiom profile 実測 (全 declaration)
| declaration | axioms | badge |
|---|
K29 | propext, Classical.choice, Quot.sound | mathlib base |
K29_card = 29 | propext, Classical.choice, Quot.sound | axiom-free tier |
K29_is_kakeya | propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound | ★ machine-checked (native_decide) |
kakeya_F34_upper_bound | 同上 | ★ machine-checked |
**注**: STEP 1700 の F_3^3 と 異なり、 本 file には kakeya_F34_lower_bound は 含まない (Dvir formal LB=15 は既 STEP 1687 で land)。 UB half のみ machine-checked、 exact 化 は 未着手 (true min ∈ [15, 29])。
掛谷 arc 進捗 update
| Layer | STEP | F_3^2 | F_3^3 | F_3^4 |
|---|
| formal LB (axiom-free) | 1687 | 6 ✓ | 10 ✓ | 15 ✓ |
| structural proof | 1691 | - | - | (4 sub-lemma sorry) |
| numerical UB (heuristic) | 1662 | - | - | 31 (greedy) |
| numerical UB (ILP) | 1694 | 7 (opt) | 13 (opt) | ≤ 28 (feasible, not persisted) |
| ILP incumbent (300s re-run) | 1704 | - | - | ≤ 29 (persisted) |
| machine-checked UB | 1700 + 1704 | - | ≤ 13 ✓ (F_3^3) | ≤ 29 ✓ (F_3^4、 本 STEP) |
Rei stack progress: two-substrate machine-checked
Dvir LB (formal, axiom-free) ≤ true min |K| ≤ UB (machine-checked native_decide)
F_3^3: 10 (formal) ≤ 13 (proven exact) ≤ 13 (machine-checked)
F_3^4: 15 (formal) ≤ true ≤ 29 (machine-checked、 本 STEP)
Honest scope
- UB のみ machine-checked: 「min |K| ≤ 29」 は Lean 4 で proven、 「min |K| ≥ 16」 は 依然 unproven (Dvir LB = 15 stands as formal floor)。 exact 判定 は 未実現。
- 29 vs 28 の discrepancy: STEP 1694 の 600s run は 28-incumbent (未 persist)、 本 STEP の 300s re-run は 29-incumbent。 HiGHS の 内部 heuristic path 差、 どちら も optimal ではない。 「29 が best known formal UB」 が 現状 accurate 表現、 「STEP 1694 の 28 を restore」 する には ILP 再度 600s+ 実行 必要。
- native_decide 依存 axiom:
Lean.ofReduceBool + Lean.trustCompiler は 純粋 decide より weak、 mathlib 標準 「computational proof」 tier。 「axiom-free」 とは 呼ばない (mathlib base 3 axiom + native 2 axiom = 5 axioms)。
- F_3^4 exact min 主張しない: bracket [15, 29] の 中身 不明、 true optimal は 別 solver or 数時間 batch で closable candidate。
- Ellenberg-Erdälyi 先行研究 audit 未実施: F_3^4 の 既知 upper bound 値 との 比較 未 verify。 arxiv/MathSciNet search は 別 arc。
Failure mode (機械学習用 dataset)
- What could go wrong: (1) STEP 1704 の 29 を 「STEP 1694 の 28 の regression」 と 誤解 → 両者 は 独立 heuristic path、 「best known persisted UB」 と 「lost incumbent」 の 区別 必要、 (2) native_decide が F_3^4 で 14s と 遅め → 25 点 or 30 点 で 「build 落ちる」 と 誤解、 実は 19,440 checks × O(29) membership で cost 律速、 timeout ではない、 (3) 「Rei は F_3^4 掛谷 UB=29 を 確定した」 と 主張 → 実は STEP 1694 で 28 を得ていた (persist bug)、 本 STEP は 「29-persisted machine-checked」 レベル、 (4) LB 15 を 「Dvir が全部」 と 誤解 → Dvir 定理 は 本 STEP と 独立、 formal 化 は STEP 1691 で partial (Phase 2b sorry)。
- Prevention: (1) 29 vs 28 の 経緯 (JSON persist bug + heuristic path 差) を honest 明記、 (2) native_decide 14s は 「acceptable but non-trivial」 明示、 F_3^5 以上 は cost 予測 必要、 (3) 「best known persisted UB」 表現 使用、 「確定」 用語 回避、 (4) Dvir formal LB と native_decide UB の layer 分離を 表 で 明示。
- Recovery: (1) 28 restore は ILP 600s+ 再実行 で 可能、 (2) F_3^n (n ≥ 5) の 大規模 problem は 別 solver (Gurobi/CPLEX) or 数時間 batch、 (3) exact 化 は 別 STEP、 (4) 先行研究 audit は 別 arc。
次候補
- F_3^4 28 restore: ILP 600s 以上 の 再実行 で 28-incumbent 取得 → 同 手法 で K28 machine-check、 UB 一段 tighten
- F_3^4 optimal 追求: 別 solver (Gurobi/CPLEX academic trial) or 数時間 batch、 [15, 29] 収束
- Phase 4b LB: F_3^3 exact 化 (K.card < 13 → ¬ Kakeya)、 4 option 検討済
- Ellenberg-Erdälyi 先行研究 audit: F_3^3 = 13 / F_3^4 min の 既知値 verify
- Phase 2b: Dvir main の 4 sub-lemma 実 proof (mathlib upstream 級)
参照 STEP: 1687 (skeleton) + 1691 (sub-lemma) + 1694 (ILP) + 1700 (F_3^3 formal UB) + 1704 (本 STEP F_3^4 formal UB) · main file data/lean4-mathlib/CollatzRei/KakeyaF34UBFormal.lean · AxiomCheck KakeyaF34UBFormalAxiomCheck.lean · ILP 再実行結果 data/kakeya/results-step1704-f34-incumbent.json.