STEP 1714 — 有限体掛谷 先行研究 audit

2026-09-03 (JST) · tab rei-aios-26 · WebSearch + WebFetch × 10 · 藤本さん directive「推奨」応答 の 第 4 段 · Rei の F_3^n Kakeya 実測 と 数学文献 の 既知値 との relation 確定

由来

STEP 1710 の 次候補 #2 (Ellenberg-Erdälyi 先行研究 audit) 実行。 Rei stack の 有限体 Kakeya 実測 (F_3^2 = 7 / F_3^3 = 13 / F_3^4 ≤ 28) が 既知 の 数学結果 と 一致する か 独立 か 未 verify だった。 掛谷 arc の 「Rei の 数学的 貢献 の 位置付け」 を 明確化 する audit。

Audit 方法

既知値 tabulation (audit 結果)

Case Theoretical LB (Dvir / Bukh-Chao) Theoretical UB (Dvir-Kopparty-Saraf-Sudan) Exact 既知値 Rei 実測 relation
F_3^2 6 7 7 (Blokhuis-Mazzocca 2008: q(q+1)/2 + (q-1)/2 for odd q) 7 (STEP 1694 ILP) MATCHES known exact ✓ 実装 correctness evidence
F_3^3 10 (Dvir C(5,3)) / 10 (Bukh-Chao ⌈27/(5/3)²⌉) (explicit UB known?) unknown in accessible literature 13 (STEP 1694 ILP optimal, STEP 1700 machine-checked UB) specific value novel LB との gap 3、 「min = 13」 は 文献未載
F_3^4 15 (Dvir C(6,4)) / ~18 (Bukh-Chao) (theoretical UB known?) unknown in accessible literature ≤ 28 (STEP 1710 ILP 700s, STEP 1710 machine-checked UB) specific bound novel bracket [15, 28]、 exact 未確定

Key findings from audit

関連論文 summary

論文年主結果Rei との relation
Dvir 2008/2009 "On the size of Kakeya sets in finite fields" (J. Amer. Math. Soc.)2008|K| ≥ q^n / n! (polynomial method、 breakthrough)STEP 1687 Phase 1 skeleton の 主 target、 Rei は Lean 4 で partial 化 (Sub-lemma 5 close)
Blokhuis-Mazzocca "The Finite Field Kakeya Problem"2008n=2 exact bound、 n≥4 improved boundF_3^2 = 7 一致 evidence、 n=3 特化結果 未確認
Ellenberg-Oberlin-Tao "Kakeya set and maximal conjectures over finite fields" (Mathematika)2010Kakeya 最大 conjecture 有限体版 解決Rei arc とは 別 track (最大 conjecture、 最小サイズ ではない)
Kyureghyan-Mueller-Xiao "On the Size of Kakeya Sets in Finite Vector Spaces" (Electron. J. Combin.)2013n≥3 の bound 改良PDF extract 失敗、 F_3^3 特化値 未確認
Lund-Saraf-Wolf "Finite field Kakeya and Nikodym sets in three dimensions" (SIAM J. Discrete Math.、 arxiv:1609.01048)2018|K| ≥ 0.2107 q³ for large q (asymptotic 改良)「for q > C」 条件 = 小さい q では 適用外、 F_3^3 特化値 は 含まず
Bukh-Chao "Sharp density bounds on the finite field Kakeya problem" (Discrete Anal.、 arxiv:2108.00074)2021|K| ≥ q^n / (2-1/q)^(n-1) sharp density (asymptotic 到達)F_3^3 では ~10、 実測 13 との gap 3、 sharp は 大きい q での話
Ellenberg-Erman "Furstenberg schemes over finite fields" (Algebra Number Theory)2016Furstenberg sets (Kakeya generalization) 有限体版Kakeya generalization、 直接的 F_3^n 特化値 なし

Rei arc の 位置付け 確定

Rei stack の 有限体 Kakeya 貢献 = 「theoretical bound の asymptotic study」 と 「specific small-case value」 の 相補
数学新結果 (定理) では ない
但し 「computational fact filling in specific small cases」 として 意味あり

Rei の 4 種 evidence (arc 累積、 全 machine-checked or software-checked)

  1. F_3^2 = 7 exact: Blokhuis-Mazzocca 2008 既知値 と 一致、 Rei ILP + Lean 4 で 独立 verify、 実装 correctness evidence
  2. F_3^3 = 13 exact (STEP 1694 ILP optimal + STEP 1700 UB machine-checked、 LB は Bukh-Chao 10 が formal floor): 文献 gap を 埋める specific small-case value
  3. F_3^4 UB ≤ 28 (STEP 1710 ILP incumbent + machine-checked): 数値実験 evidence + machine-checked best-known persisted UB
  4. Dvir 2008 Lean 4 skeleton (STEP 1687+1691、 Sub-lemma 5 close + 4 sorry): polynomial method の formalization ロードマップ (Phase 2b で 完全 close 予定)

Honest scope

Failure mode (機械学習用 dataset)

Rei の 立ち位置 (audit 結論)

Rei 掛谷 arc = 「先行 asymptotic theory」 + 「specific small-case fill-in」 の 相補的 実験
数学的 「新結果」 でない (定理 でない)
但し「computational evidence」 として collateral value あり
Phase 2b 完了 (Dvir Lean 4 full close) で 「formalization contribution」 の 主張可能 化予定

次候補 (arc 継続 or 別 arc)

  1. Phase 4b LB (F_3^3 exact 化): K.card ≤ 12 → ¬ Kakeya の formal proof、 実行 cost 数時間 batch (exhaustive native_decide)
  2. Phase 2b: Dvir main の 4 sub-lemma 実 proof、 mathlib upstream contribution 級
  3. F_3^4 optimal 追求: 別 solver (Gurobi/CPLEX academic) or 数時間 batch で [15, 28] 収束
  4. 専門家 audit: MathOverflow で 「F_3^3 min Kakeya = 13 は 既知値 か」 質問、 Blokhuis-Mazzocca / Bukh-Chao 本人 メール
  5. Furstenberg scheme angle: Ellenberg-Erman 2016 の generalization を 見ると Rei との 意外な relation の 可能性

参照 STEP: 1687 (skeleton) + 1691 (sub-lemma) + 1694 (ILP) + 1700 (F_3^3 formal UB) + 1704 (F_3^4 formal UB=29) + 1710 (F_3^4 formal UB=28) + 1714 (本 STEP audit) · 検索 tools: WebSearch × 5, WebFetch × 5, OEIS direct via curl · audit report: 本 site page.