Dvir 2009 JAMS版のKakeya下界の式dvirBound q n := C(q + n − 1, n) にq=3, n=4を代入すると15になる（Lean 4でdecideにより計算、axiom-free）。 下界の式の根拠はJAMS版のTheorem 1.5の証明（|K| < C(q+n−1, n) と仮定して矛盾を導く）。 論文はAlonとTaoの指摘による改良と記す。 arXiv版v3では対応するのはTheorem 3で、証明はC(q+n−2, n) を使う（定理の番号と式はJAMS版と異なる）。 Leanで証明したのは、この式の値の計算だけです。F₃⁴ のKakeya集合の大きさがこの値以上であること（Dvirの定理）のLeanでの証明（dvir_kakeya）は、現在sorryが残っていて未完成です。
式
dvirBound 3 4 = Nat.choose (3 + 4 − 1) 4 = Nat.choose 6 4 = 15
LaTeX source
\mathrm{dvirBound}(q, n) := \binom{q + n - 1}{n}; \quad \mathrm{dvirBound}(3, 4) = \binom{6}{4} = 15記号表
| 記号 | 意味 | 型 |
|---|---|---|
| dvirBound | Dvir 2008の下界: 全次数 ≤ q − 1のn変数多項式空間の次元 | ℕ → ℕ → ℕ |
| q | 有限体Fの位数 (本項目では3) | ℕ |
| n | 空間F^nの次元 (本項目では4) | ℕ |
| Nat.choose | 二項係数 (Lean mathlib) | ℕ → ℕ → ℕ |
走る最小例
Lean 4で `dvirBound_3_4 : dvirBound 3 4 = 15` を `by decide` で証明し、axiom profileを出力。 lean-verify.ymlがGitHub Actionsで実行し、検査状態を生成する。
import CollatzRei.KakeyaDvir open CollatzRei.KakeyaDvir #check @dvirBound_3_4 #print axioms dvirBound_3_4
期待される出力：
dvirBound_3_4 : dvirBound 3 4 = 15 'CollatzRei.KakeyaDvir.dvirBound_3_4' does not depend on any axioms
検査状態
S2形式証明済み (axiom-free)
検査の内訳を見る
| 定理 | CollatzRei.KakeyaDvir.dvirBound_3_4 |
| Lean file | CollatzRei/KakeyaDvirAxiomCheck.lean |
| 公理 | (公理なし) |
| 生成元 | gha (GHA run 39175017999) |
| 生成時刻 | 2026-10-18T23:15:15.522Z |
| Lean toolchain | leanprover/lean4:v4.27.0 |
関係項目
- rp.dvir-bound-3-2 — 両者ともDvir 2008の同じ下界の式 (dvirBound) の具体値を計算した項目 (異なる (q, n) = (3,2) と (3,4)) [related_to]
- rp.dvir-bound-5-4 — 両者ともn＝4で、Fの位数のみ違う（3と5） [related_to]
- rp.homogeneous-vanishing-fn — 両者ともDvir 2009（JAMS版）証明の構成要素（本項目は下界の値の計算で、関連項目は斉次多項式消失、Rei-AIOS側でDvirの証明を分解した5項目の#5） [related_to]
出典
- On the size of Kakeya sets in finite fields — Dvir, Z. (2009) URL
- On the size of Kakeya sets in finite fields (arXiv preprint, open-access) — Dvir, Z. (2008) URL
- Rei-AIOS Lean 4 CollatzRei/KakeyaDvir.lean — Fujimoto, N. (2026) AGPL-3.0 + Commercial
書き手と承認
| 下書き | Claude（AnthropicのAI）2026-10-15 |
| 独立レビュー | Claude（Code サブエージェント・独立レビュー） (2026-10-26) |
| 公開承認 | 藤本 伸樹2026-10-26 |
| ページ生成 | ボット（項目データから自動生成） |
訂正記録 (1件)
C-dvir-3-4-corr-001
誤りの種類：出典の不一致
何が誤りだったか：(1) 走る最小例の期待出力を、Leanを実際に走らせずに書いていた。実際にLeanで実行すると、`open CollatzRei.KakeyaDvir` の影響で短い名前（dvirBound_3_4）で表示されるが、以前の期待出力では完全な名前（@CollatzRei.KakeyaDvir.dvirBound_3_4）で書いていた。定理の内容、必要な公理（なし＝axiom-free）、検査状態の表示は実機の出力と一致している。(2) 作成者欄の bot と AI の記述に、公開前の状態を表す文言（「draft, not yet published」「awaiting independent review」）が残っていた。
どう直したか：走る最小例の期待出力を、実際にLeanで実行した結果に合わせて直しました。以前の期待出力は実行せずに書いたもので、定理名の表示の仕方（完全な名前か短い名前か）が実際の出力と違っていました。定理の内容、必要な公理、検査状態の表示は変わっていません。作成者欄の、公開前の状態を表す記述を直しました。
発見: 藤本 伸樹 ｜ 訂正 commit:
2dfb14ea15c1bab822e4cee7badb2bac00925564全項目の訂正一覧: /reipedia/corrections/