STEP 1687 — Dvir 有限体掛谷 Lean 4 skeleton (Phase 1)
2026-09-03 (JST) · tab rei-aios-26 · mathlib v4.27.0 · data/lean4-mathlib/CollatzRei/KakeyaDvir.lean (137 行) + AxiomCheck pair · 7 declaration の axiom profile 実測 · 4 sanity theorem 完全 axiom-free · 主定理 sorry 1 件 (skeleton phase として honestly counted)
由来
藤本さんが chat-Claude 2026-09-02 対話で 「掛谷集合は 前回の 分散計算話の 良い反例」 と提示。 ℝⁿ 掛谷予想 (Wang–Zahl 2025 が n=3 解決、 Guth Bourbaki 2026-04) は Hausdorff 次元 (δ→0 の 極限量) についての主張で 「閾値の上は理論、 下は計算」 の分業が構造的に作れない = 分散計算がほぼ役に立たない type の問題。 その中で 3 点だけ計算・形式化が触れる: (1) 有限体版 (Dvir 2008 が 多項式法で 1 ページ証明)、 (2) 形式化 (Wang–Zahl 側は Flyspeck 級、 有限体側は現実的)、 (3) 高次元 (n≥4) への 離散モデル 実験証拠。
藤本さん directive: 「Dvir の 形式化から入るなら、 定理の 骨格を Lean4 の statement に 落とすところから 一緒にできます」
応答方針: prior art audit → mathlib scaffolding 確認 → Rei-native skeleton → axiom profile 実測 → 藤本さん judgment → Phase 2 (full proof) → Phase 3 (数値 bracketing)。
Prior art 確認結果 (2026-09-03 実測)
| 層 | 状況 | Rei 貢献余地 |
|---|
mathlib v4.27.0 Combinatorial.Nullstellensatz | Alon 1999 formalization 存在 (Chambert-Loir 2024)、 eq_zero_of_eval_zero_at_prod_finset + combinatorial_nullstellensatz_exists_linearCombination + combinatorial_nullstellensatz_exists_eval_nonzero の 3 主定理 | scaffolding として 使用 |
| mathlib v4.27.0 Kakeya file | 存在せず (grep 実測) | Rei 独立追加余地 |
FormalConjectures Wikipedia/Kakeya.lean | IsKakeyaFinite def + kakeya_finite は Bukh-Chao 2021 sharp bound で sorry | Dvir 2008 original bound (weaker) は skeleton 化余地 |
| Rei stack STEP 1662 (rei-aios-80) | Python greedy 探索、 F_3^4 min=31 vs informal Dvir LB=15 | formal witness 提供余地 |
構造
Deliverable A (本 STEP): Rei-native skeleton
def IsKakeyaFinite (K : Finset (Fin n → F)) : Prop :=
∀ v : Fin n → F, v ≠ 0 → ∃ a : Fin n → F, ∀ t : F, a + t • v ∈ K
def dvirBound (q n : ℕ) : ℕ := Nat.choose (q + n - 1) n
theorem dvir_kakeya
(K : Finset (Fin n → F)) (hK : IsKakeyaFinite K) :
dvirBound (Fintype.card F) n ≤ K.card := by
sorry
sanity 4 件 (dvirBound_3_2 = 6 / _3_4 = 15 / _5_4 = 70 / _3_5 = 21) は decide で 完全 axiom-free に closable。
Bound 比較
Dvir 2008 (本 file): |K| ≥ C(q + n − 1, n) ≈ qn / n! ⋯ 「original weak form」
Bukh–Chao 2021 (sharp): |K| ≥ qn / (2 − 1/q)n−1 ⋯ FormalConjectures 側の target
Axiom profile 実測 (lake build + lean 実行済)
| declaration | axioms | badge |
|---|
IsKakeyaFinite | propext, Classical.choice, Quot.sound | mathlib base |
dvirBound | does not depend on any axioms | axiom-free |
dvirBound_3_2 = 6 | does not depend on any axioms | axiom-free |
dvirBound_3_4 = 15 | does not depend on any axioms | axiom-free ★ STEP 1662 の LB=15 に formal witness |
dvirBound_5_4 = 70 | does not depend on any axioms | axiom-free |
dvirBound_3_5 = 21 | does not depend on any axioms | axiom-free |
dvir_kakeya | propext, sorryAx, Classical.choice, Quot.sound | sorryAx skeleton phase, honestly counted |
Proof outline (Dvir 2008, ≤ 1 ページ、 Phase 2 の 実装 target)
- |K| < C(q + n − 1, n) と 仮定。 総次数 ≤ q − 1 の 多項式空間 の 次元 > |K| なので K で 消える 非零 P が 存在 (線形代数)。
- P の 最高次同次成分 Ph (次数 d ≤ q − 1) を 取る (WLOG 非零)。
- 任意方向 v ≠ 0 に対し Kakeya 性で ∃a, ∀t, a + tv ∈ K → P(a + tv) = 0 (∀t ∈ F)。
- P(a + tv) は t の 多項式 で 次数 ≤ q − 1 = |F| − 1。 F の 全 q 元で 0 なので 恒等的に 零。
- td 係数 = Ph(v)。 これが 全 v ≠ 0 で 0。
- Ph は 次数 d < q の 同次多項式 で Fn \ {0} で 0 → Schwartz-Zippel で Ph = 0。
- 矛盾。
Honest scope
- Proof は sorry:
dvir_kakeya は statement only、 Rei-AIOS 3,542 axiom-free tally には 加算しない (skeleton phase として 明示 counting)。 sorryAx は hidden ではなく #print axioms で公開。
- 弱い bound: Bukh-Chao 2021 sharp bound ではなく Dvir 2008 original。 sharp bound は out of scope (Phase C の 別 STEP candidate)。
- 新数学結果ではない: Dvir 2008 の Lean 4 skeleton、 「Rei は Kakeya を解いた」 は 絶対に 主張しない。
- Kakeya arc の 総合可能性の 限界: 本 STEP は 「有限体」 変種のみ に formal 化 触れる、 ℝn 本体 (Wang-Zahl 2025 の n=3) は 依然 130 ページ の 多重スケール 帰納法 で Flyspeck 級。
- 未 build 統合:
CollatzRei/Basic.lean の default target には 未追加、 個別 lake build CollatzRei.KakeyaDvir のみ 動作確認 (build 9.4s)。
STEP 1662 との相補関係
| layer | STEP 1662 (rei-aios-80, 2026-09-02) | STEP 1687 (rei-aios-26, 2026-09-03、 本 STEP) |
|---|
| 種別 | Python 数値実験 | Lean 4 formal skeleton |
| 成果物 | data/kakeya/results-step1662.json + scripts/kakeya-finite-field/run-kakeya.py | data/lean4-mathlib/CollatzRei/KakeyaDvir.lean + AxiomCheck pair |
| F34 の 扱い | greedy min = 31 (30 trial), 全空間 81 の 38%, informal Dvir LB=15 の 2.07x | dvirBound_3_4 で C(6,4)=15 を decide、 axiom-free、 STEP 1662 の 15 に formal witness |
| Honest scope | heuristic の 下界、 true min ではない | statement only、 proof は sorry |
| 相補 | 数値実験 evidence | 数値 LB に formal guarantee 提供 |
Failure mode (機械学習用 dataset として)
- What could go wrong: 「Combinatorial Nullstellensatz が mathlib に あるから Dvir も あるだろう」 と grep せず に skip、 実は Kakeya-specific formalization は Rei stack の 独立貢献余地。 逆に 「skeleton だけで STEP を刻む価値がない」 と 保留、 実は skeleton phase の sorry を honestly count する 方が 3,542 axiom-free tally の integrity を 保つ discipline。 sharp bound (Bukh-Chao) に 目移りして original Dvir の 1 ページ証明の Lean 化を skip、 実は original の方が formalization コスト が 一桁少ない。
- Prevention: prior art audit 4 point (mathlib grep + FormalConjectures 確認 + STEP 1662 の informal LB 数値 15 の 由来照合 + Wang-Zahl 2025 との layer 区別) を skeleton draft 前に 完了、 axiom profile を最初から 実測 (
#print axioms で sorryAx を hidden ではなく明示 counting)、 Deliverable A/B/C 分離を docstring に埋込、 sanity theorem 4 件 を decide で closable に して skeleton phase でも 実測命題化。
- Recovery: Deliverable B (full proof, 予想 ~500 行) は 別 STEP に分離可能、 mathlib
combinatorial_nullstellensatz_exists_eval_nonzero を hook として 段階的に proof body を積む path。 Deliverable A alone でも STEP 1662 の numerical LB=15 に formal witness を提供する 独立 operational value あり。
次の一手
- Phase 2 (次): Deliverable B — full proof (~500 行)。
dvir_kakeya の sorry を 実 proof に置換。 4 sub-lemma に分解: (α) linear-algebra existence lemma (K で 消える 非零 P) + (β) top-homogeneous-component extraction + (γ) univariate line restriction + (δ) Nullstellensatz application。
- Phase 3 (最終): 有限体 min size cube-and-conquer 探索。 STEP 1662 の greedy を SAT/ILP で 下回れるか。 F33 (Dvir LB=10) 完全探索、 F34 (LB=15, greedy=31) 部分探索。 formal LB (Phase 2) と numerical UB の bracketing。
参照: 詳細 memory memory/project_step1687_kakeya_dvir_lean_skeleton_2026-09-03.md · notepad docs/notepad/2026-09-03T00-09_STEP-1687_kakeya-dvir-lean-skeleton.md · 関連 STEP 1662 (Python greedy) · STEP 1282 (情報理論プローブ下界 zero-axiom 同 layer) · STEP 1683 (Rei プロジェクト全体マップ)。