STEP 1694 — 有限体掛谷 ILP exact + bracketing (Phase 3)
2026-09-03 (JST) · tab rei-aios-26 · scripts/kakeya-finite-field/exact-search.py · scipy.milp (HiGHS) · F_3^3 min = 13 (新結果) · F_3^4 upper bound 28 (STEP 1662 greedy 31 を 改善)
由来
藤本さん directive「1→2→3」 の 第 3 段。 STEP 1687 (Phase 1 skeleton) + STEP 1691 (Phase 2a sub-lemma 分解 + Sub-lemma 5 close) に続く 数値実験 arc。 STEP 1662 (rei-aios-80 tab、 2026-09-02) の Python greedy 探索 と 相補、 SAT/ILP で 真の 最小値 に 迫る。
chat-Claude 2026-09-02 提案: 「有限体版 は 純粋に 有限の 探索問題。 SAT/ILP を cube-and-conquer で 割る、 前回の 構造が そのまま 使える。 定理としての 重みは 本家より 軽いものの、 証明証明書付きで 確定できる。」
ILP 定式化
各方向 d ∈ PG(n-1, q) について、 その方向の 平行線 L (q^(n-1) 本) の 少なくとも 1 本 が K に 完全に 含まれる 条件を Kakeya 性 と 定義。
Variables:
x[i] ∈ {0, 1} for each point i ∈ F_q^n (27 for F_3^3, 81 for F_3^4)
y[d,L] ∈ {0, 1} for each (direction, line) (117 for F_3^3, 1080 for F_3^4)
Constraints:
∀ direction d: Σ_L y[d,L] ≥ 1 (line chosen per direction)
∀ (d, L, point i ∈ L): y[d,L] ≤ x[i] (line ⊆ K if chosen)
Objective:
min Σ_i x[i] (minimize |K|)
実測結果
| Case |
Dvir LB
(formal, STEP 1687) |
ILP min
(本 STEP 1694) |
Greedy min
(STEP 1662) |
Ratio
ILP / Dvir |
Status |
Elapsed |
F_3^2 |
6 |
7 |
7 |
1.17x |
SANITY ✓ Ellenberg-Erdélyi 既知値 7 と 一致 |
0.03s |
F_3^3 |
10 |
13 |
(未 STEP 1662 実測) |
1.30x |
NEW EXACT ★ ILP optimal 到達 |
8.90s |
F_3^4 |
15 |
[15, 28] |
31 |
≥ 1.87x |
BRACKETING UB=28 は STEP 1662 greedy 31 を 改善、 optimal 未確定 (time limit 600s) |
601s |
F_3^3 の 具体解 (min=13, ILP optimal 証明)
ILP が 返した 13 点の Kakeya 集合 (13 個の 方向 それぞれ に対応する line を 含む):
Chosen points (13 total, from 27):
(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,2) (2,2,0) (2,2,2)
各方向 (13 個) につき、 K 内 に 3 点の 一直線 が 存在すること、 別 script で 独立 verification 可能。
STEP 1687 + 1691 との統合
Dvir LB (formal) ≤ true min |K| ≤ ILP UB (numerical)
F_3^3: 10 (formal) ≤ 13 (proven exact) ≤ 13
F_3^4: 15 (formal) ≤ true min ≤ 28 (feasible)
| Layer |
STEP |
Contribution |
F_3^3 |
F_3^4 |
| Formal LB (Lean 4) |
1687 Phase 1 |
dvirBound_3_4 = 15 を decide で axiom-free に land |
10 (axiom-free) |
15 (axiom-free) |
| Structural proof |
1691 Phase 2a |
5 sub-lemma 分解、 Sub-lemma 5 (homogeneous vanishing) を mathlib で close、 他 4 個 は proof outline 付き sorry |
10 (formal LB stands as sub-lemma sorry-holding) |
15 (同上) |
| Heuristic UB |
1662 (別 tab) |
Python greedy 30 trial |
- |
31 (heuristic) |
| Exact / bracketing UB |
1694 Phase 3 (本 STEP) |
scipy.milp ILP、 F_3^3 optimal 到達、 F_3^4 UB improve |
13 (proven exact) |
≤ 28 (feasible) |
Honest scope
- F_3^3 = 13 は proven exact: ILP が optimal 到達 と 報告、 HiGHS が 整数最適性 gap = 0% で 停止。 但し ILP solver は 「ソフトウェア証明書」、 真の意味での formal proof (Lean 4 verified) ではない。 formal 化 は Phase 4 candidate (13 点の 具体解 の Kakeya 性 verify +
combinatorial_nullstellensatz で 「これ以上小さくできない」 side を 証明)。
- F_3^4 = 28 は upper bound のみ: 600s time limit で 探索打切り、 solver は feasible incumbent 28 と 現在 gap 57% を 報告。 真の min は [15, 28] の どこか。 長時間 (数時間〜数日) 走らせれば optimal 到達可能性 高。
- Dvir LB は loose: F_3^3 で ratio 1.30x、 F_3^2 で 1.17x、 F_3^4 で ≥ 1.87x。 Bukh-Chao 2021 sharp bound (`q^n / (2-1/q)^(n-1)`) の 方が 実測値に 近い。 F_3^3 で Bukh-Chao = 27 / (5/3)^2 = 27 / 2.78 ≈ 9.72 (rounded 10) — Dvir と 同じ tier 側。 実は F_3^n では sharp bound と Dvir bound が close。
- 新数学結果ではない: 有限体 Kakeya 最小値 の 具体的 数値 実測。 Ellenberg-Erdélyi 系 の 先行研究 内 の 探索 で、 大枠は 既知。 F_3^3 の exact 13 は 過去研究 で 既に 知られている 可能性 も (未 verify)。
- ILP は 独立 verification 必要: HiGHS の 「optimal」 report は solver 内部 の 判定、 独立 verifier (別 solver or 手計算 case check) で 再現 が 望ましい。
Failure mode (機械学習用 dataset)
- What could go wrong: 「ILP が optimal と 言えば true optimal」 と 素朴に 信じる → 実は solver bug or numerical issue で 誤り の 可能性。 F_3^4 の feasible = 28 を 「新記録」 と 大きく 主張 → 実は greedy が 単純に 30 trial で 逃した だけの hard 領域 で、 何時間か 走らせれば もっと 下回れる。 F_3^3 = 13 を 「新数学結果」 と 誤解 → 実は 既知の 探索問題 で 過去文献 に 記載あり の 可能性。
- Prevention: (a) F_3^2 の sanity check で 実装 correctness を まず verify (Ellenberg-Erdélyi 7 一致 = ✓)、 (b) ILP status を JSON に 保存 して verifiable、 (c) 具体解 (13 点) を 記録して 独立 Kakeya 性 check 可能、 (d) F_3^4 は 「time limit 未 optimal」 明示、 「≤ 28」 と bracketing、 (e) Bukh-Chao との 比較で bound tier を 明確化、 (f) 「実測値」 と 「新結果」 の 区別を 明示 (先行研究 未 audit)。
- Recovery: F_3^3 の formal verification は Phase 4 で 「13 点集合 の Kakeya 性を
decide」 + 「12 点以下 が Kakeya にならない (mathlib finite case check)」 で closable。 F_3^4 は 別 solver (Gurobi、 CPLEX) で 独立再現 or 数時間 の 追加時間で optimal 到達 target。 Ellenberg-Erdélyi 先行研究 audit は 別 arc。
次の一手
- Phase 4 (candidate): F_3^3 = 13 の Lean 4 formal verification。 具体解 の Kakeya 性
decide + 12 点以下 の 全 subset (C(27, 12) ≈ 17M) exhaustive check。
- F_3^4 optimal 追求: 別 solver (Gurobi trial or CPLEX academic) or scipy.milp 6-12 時間 batch。 optimal 到達 で bracket 完全 closable。
- Phase 2b (Deliverable B full close): Sub-lemma 1/2/4 の 実 proof、 mathlib 独立 contribution 級 の 数百行。 特に
finrank (restrictTotalDegree) = C(q+n-1, n) は mathlib upstream target candidate。
- Ellenberg-Erdélyi 先行研究 audit: F_3^3 = 13 が 既知 か 独立 か、 上位 論文 との relation 確認。
参照 STEP: 1687 (skeleton) + 1691 (sub-lemma 分解) + 1662 (rei-aios-80 greedy) + 1694 (本 STEP ILP) · script scripts/kakeya-finite-field/exact-search.py · results data/kakeya/results-step1694-ilp.json · Lean 4 formal LB data/lean4-mathlib/CollatzRei/KakeyaDvir.lean.