Lean4: FLT: sorry 残ってる→解決策へ

関連記事

ま、糠喜ぬかよろこびは研究中によくあること。

こうすると公理 #axiom や sorry に依存してる。が見えるようになります。

sorryAx

これが、出てくると何処かに #sorry , #admit が残っている事が解る。

こちらの Mathlib.FLT を使った証明には sorryAx はありません。

/-- 補題: $u=1$ の場合、$GN(3, 1, y) = 3y^2 + 3y + 1$ は $y > 0$ で立方数になり得ない -/
lemma GN3_one_not_cube_use_FLT3 {y : ℕ} (hy : 0 < y) : ¬ ∃ x, x^3 = GN 3 1 y := by
  rw [GN_quadratic]
  rintro ⟨x, hx⟩
  -- x^3 = 3y^2 + 3y + 1
  -- x^3 + y^3 = (y+1)^3
  have h_flt : x ^ 3 + y ^ 3 = (y + 1) ^ 3 := by
    rw [hx]
    ring
  have hx_pos : x ≠ 0 := by
    intro h; rw [h] at hx; omega
  have hy_pos : y ≠ 0 := hy.ne''
  have hz_pos : y + 1 ≠ 0 := by omega
  exact fermatLastTheoremThree x y (y + 1) hx_pos hy_pos hz_pos h_flt

単純な構成の補題です。

から先は Mathlib の証明です。

#fermatLastTheoremThree #FermatLastTheoremFor

sorry の探索

補題のチェーン探索は AI に任せるのが良い！

🐺賢狼に任せるのが一番。その方が早いし、ある意味でも正確。
最終的なチェックは人間（そして人間は間違える生き物！←）

🔗 完全な依存チェーン

FLT_case_3 (Basic.lean 542行)
  ↓ 呼び出し
u_eq_one_of_coprime_gcd (Basic.lean 409行)
  ↓ 呼び出し
GN3_cube_not_cube_of_gt_one (Basic.lean 331行)
  ↓ 呼び出し
padicValNat_primitive_prime_factor_le_one 
(ZsigmondyCyclotomic.lean 1154行)
  ↓ 呼び出し
squarefree_implies_padic_val_le_one 
(ZsigmondyCyclotomic.lean 882行)
  ↓ 内部
   ⚠️ SORRY (line 886)

ZsigmondyCyclotomic.lean

忘れていた！

$${x\ G_{d-1}(x,u)}$$ 多項式の構造解析からの接続が未だだった。

lemma squarefree_implies_padic_val_le_one (d a b q : ℕ)
    (hd_prime : Nat.Prime d) (hb : 0 < b) (hab : Nat.Coprime a b)
    (hq_prime : Nat.Prime q) (hq_div : q ∣ a ^ d - b ^ d) :
    padicValNat q (a ^ d - b ^ d) ≤ 1 := by
  -- ワークスペース整理：以降の分岐で使う基本事実を先に抽出しておく
  have hd_two_le : 2 ≤ d := hd_prime.two_le
  have hq_ne_one : q ≠ 1 := hq_prime.ne_one
  have hq_pos : 0 < q := hq_prime.pos
  have hq_dvd : q ∣ a ^ d - b ^ d := hq_div
  clear hb hab hq_div
  -- Cosmic Formula 経由のアプローチ
  -- Step 1: べき乗差の因数分解（pow_sub_pow_factor_cosmic）✅
  -- Step 2: padicValNat の帰着（padicValNat_of_primitive_prime_factor_via_G）✅
  -- Step 3: G の構造解析（最も難しい部分、Lucas/Kummer の活用）⏳
  sorry  -- [SORRY-2: 一般上界、G 解析が本質的に難しい]

#Zsigmondy #Cyclotomic

しかし全体がこうして見えてくると…

この時、見えていなかった問題がハッキリ見えるようになる。
詳細を省くと、以下の記事で解決できそうだ。

私は、既に答えを知っていた！？

とにかく、先に知っておいて良かった例。
単に、既存定理、理論を知るだけでなく持論との接合もあると、ここからの応用が効く。

`d=3` は #Eisenstein 整数の #Norm としての G（ここが最強に“見える”）

`d=3` の

$$
a^2+ab+b^2
$$

は、 #アイゼンシュタイン整数 $${\mathbb{Z}[\omega]}$$（$${\omega^2+\omega+1=0}$$）で

$$
N(a-b\omega)=a^2+ab+b^2
$$

という #ノルム そのものになる。

すると

$$
a^3-b^3=(a-b)\,N(a-b\omega)
$$

は、Mathlib の FLT3 が使う「三方向因子分解（共役の積）」と 完全に同型になる。
ぬしの言葉で言えば「Body×3 と 120° 回転対称」じゃな。

この橋を Lean で固定すると、以後の議論が全部“意味付き”になる：

• 宇宙式の `G` は「回転方向の面積（ノルム）」

• Mathlib の $${\lambda=\zeta_3-1}$$ 付値は「境界（Gap）の厚み」
  という対応が、ただの比喩でなく「定義と補題」で接続される。

単純に表現してしまえば、

$$
x\ G_{d-1}(x,u) := (a-b)\,N(a-b\omega)
$$

ならば、

• $${x := (a-b)}$$

• $${G_{d-1}(x,u):=N(a-b\omega)}$$

と繋がる。

ただ、この関係だけでは $${d=n=3}$$ の３乗の関係しか否定できない。

$$
\Large
x^3+y^3=z^3
$$

より一般的な、

$$
\large
\\[2pt]
a^p-b^p=(a-b)\cdot \sum_{k=0}^{p-1} a^{p-1-k}b^k
$$

に、持っていかなくては。✍️

2026/02/22 9:36

D.