有限体F上の斉次多項式で、次数dが|F|以下かつF^nの全ての点で0になるものは、ゼロ多項式である

P_h ∈ MvPolynomial (Fin n) Fが次数dの斉次多項式でd ≤ |F|かつ全てのv ∈ F^nでeval v P_h = 0ならば、P_h = 0。Dvir 2009 JAMS版のTheorem 1.5の証明で使われる、斉次多項式が消えることの議論にあたる（arXiv版v3では対応するのはTheorem 3で、下界の式はC(q+n−2, n)、JAMS版のTheorem 1.5のC(q+n−1, n)と番号・式ともに異なる。Dvirの論文には「sub-lemma 5」という番号付けは無い。arXiv v3の番号付き命題はTheorem 1, 2, 3, Corollary 1.1, Lemma 2.1, Claim 2.2）。「sub-lemma 5」はRei-AIOS側のLean file `data/lean4-mathlib/CollatzRei/KakeyaDvir.lean`内部でPhase 2aの5件の分解項目の#5として付けた命名。Lean 4でmathlibの `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card` を直接適用して閉じている。依存する公理はpropext, Classical.choice, Quot.sound（mathlib base）。

式

P_h \in F[x_1, \ldots, x_n] \text{ homogeneous of degree } d \;\land\; d \le |F| \;\land\; \forall v \in F^n.\, P_h(v) = 0 \;\Longrightarrow\; P_h = 0

記号表

走る最小例

Lean 4で `homogeneous_vanishing_on_Fn_is_zero` を証明し、`#print axioms` でaxiom profileを出力する。本定理はRei-AIOS側のKakeyaDvir.lean内部で付けた5件のsub-lemma分解項目の#5（Dvir 2009 JAMS版のTheorem 1.5証明で使われる斉次多項式消失の議論にあたる、arXiv版v3では対応するのはTheorem 3の証明中の斉次多項式消失の議論、Dvirの論文にはsub-lemma番号付けなし）。同じKakeyaDvir.leanにRei-AIOS側のsub-lemma 1-4（= sorry残の未完成項目）とmain theorem `dvir_kakeya`（= sub-lemma 1-4に依存するためsorryAx残）も含まれる。本項目はmathlib baseのみに依存し、ファイル内の他のsorryには影響されない。

import CollatzRei.KakeyaDvir
open CollatzRei.KakeyaDvir
#check @homogeneous_vanishing_on_Fn_is_zero
#print axioms homogeneous_vanishing_on_Fn_is_zero

期待される出力：

@homogeneous_vanishing_on_Fn_is_zero : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [DecidableEq F] {n : ℕ}
  (P_h : MvPolynomial (Fin n) F) (d : ℕ),
  P_h.IsHomogeneous d → d ≤ Fintype.card F → (∀ (v : Fin n → F), (MvPolynomial.eval v) P_h = 0) → P_h = 0
'CollatzRei.KakeyaDvir.homogeneous_vanishing_on_Fn_is_zero' depends on axioms: [propext, Classical.choice, Quot.sound]

検査状態

S2形式証明済み (mathlib base)

関係項目

• rp.dvir-bound-3-2 — 本定理はRei-AIOS側でDvirの証明を分解した5項目の#5（Dvir 2009（JAMS版）証明の構成要素）。同ファイルKakeyaDvir.leanに下界の値の計算項目（dvirBound_3_2等）もあり、両者は同じ証明鎖の別要素 [related_to]
• rp.dvir-bound-3-4 — 両者ともDvir 2009（JAMS版）証明の構成要素（本項目は斉次多項式消失で、Rei-AIOS側でDvirの証明を分解した5項目の#5。target_idは下界の値の計算） [related_to]
• rp.dvir-bound-5-4 — 両者ともDvir 2009（JAMS版）証明の構成要素（本項目は斉次多項式消失で、Rei-AIOS側でDvirの証明を分解した5項目の#5。target_idは下界の値の計算） [related_to]

出典

1. On the size of Kakeya sets in finite fields — Dvir, Z. (2009) URL
2. On the size of Kakeya sets in finite fields (arXiv preprint, open-access) — Dvir, Z. (2008) URL
3. Mathlib.RingTheory.MvPolynomial.Homogeneous (mathlib4) — `IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card` — mathlib4 contributors (2024) URLApache-2.0 (mathlib4)

書き手と承認

訂正記録

訂正記録なし