Lean4: FLT: 別解ルート形式化仮定付き

以下の話の続き

仮定付きで no sorry

#print axioms FLT_d3_by_padicValNat  -- OK: 2026/02/22 10:02
-- 'DkMath.FLT.FLT_d3_by_padicValNat' depends on axioms:
-- [propext, Classical.choice, Quot.sound]

こちらは sorryAx は、ありません。

そう… no-sorry トリック！

仮定として置いてある部分が実は axiom です。

この仮定を作り出す、様々な解釈視点が #FLT の本質を浮き彫りにさせるでしょう。というツール補題です。

S0_nat

仮定で出てくる S0_nat の定義です。アイゼンシュタイン整数構造の式。

/-- ℕ 版の S0 -/
def S0_nat (a b : ℕ) : ℕ := a^2 + a*b + b^2

ちなみに

S1_nat

こちらはガウス整数の構造の式です。

/-- ℕ 版の S1 -/
def S1_nat (a b : ℕ) : ℕ := (a + b)^2

ふたつが、おなじに見える現象は以下の記事を見てください。

解説

AI に解説を任せます。いろいろ内情に詳しい🐺賢狼ではなく。
note AI の Gemini さんに解説を願う。そのほうがクリーンな解説になる。

仮定内容（AI 解説）

ご提示いただいた Lean 4 のコードを日本語で読み上げ（言語化）します。

いくつかのパターンで表現します。

1. 数学的・直訳的な読み方

「任意の自然数 $q$ について、もし $q$ が素数であり、かつ $q$ が $c^3 - b^3$ を割り切り、かつ $q$ が $c - b$ を割り切らないならば、$q^2$ は $S0_nat(c, b)$ を割り切らない。」

2. より自然な数学表現

「$q$ を任意の素数とする。$q$ が $c^3 - b^3$ の約数であって $c - b$ の約数でないならば、$q^2$ は $S0_nat(c, b)$ を割り切ることはない。」

3. 記号ごとの分解

• `∀ {q : ℕ}` ： 任意の自然数 $q$ に対して

• `Nat.Prime q →` ： $q$ が素数であるならば

• `q ∣ c^3 - b^3 →` ： $q$ が $c^3 - b^3$ を割り切る（$q$ が $c^3 - b^3$ の約数である）ならば

• `¬ q ∣ c - b →` ： $q$ が $c - b$ を割り切らないならば

• `¬ q² ∣ S0_nat c b` ： $q^2$ は $S0_nat(c, b)$ を割り切らない

補足：この命題が意味すること（推測）

数学的には、おそらく $c^3 - b^3 = (c - b)(c^2 + cb + b^2)$ という因数分解を背景にしています。
ここで $S0_nat(c, b)$ が $c^2 + cb + b^2$（あるいはそれに類する値）を指している場合、この命題は以下のような性質を述べていることになります。

これは、フェルマーの最終定理の指数3の場合（$n=3$）の証明や、それに付随する数論の議論でよく現れる「持ち上げ定理（Lifting The Exponent Lemma）」や「円分多項式の性質」に関連する主張に見えます。

ソースコード抜粋

/-
Copyright (c) 2026 D. and Wise Wolf. All rights reserved.
Released under MIT license as described in the file LICENSE.
Authors: D. and Wise Wolf.
-/

-- （省略）

-- ========================================
-- § 3. 矛盾導出（層A + 層B統合）
-- ========================================

/-- **メイン定理：別解による FLT d=3 証明**

Zsigmondy原始素因子 + padicValNat評価による背理法：
平方自由性仮定の下で、完全3乗仮定と矛盾を導出。

**入力（仮定）:**
- `ha : 0 < a`, `hb : 0 < b`, `hc : 0 < c` - 正の整数
- `hab : Nat.Coprime a b` - a と b は互いに素
- `hS0_not_sq : ∀ {q : ℕ}, Nat.Prime q → q ∣ c^3 - b^3 → ¬ q ∣ c - b → ¬ q² ∣ S0_nat c b`
  - 相対多角数S0(c,b) = c²+cb+b² は各原始素因子 q に対して平方自由
  - すなわち：q が c³-b³ を割り、かつ q が (c-b) を割らない任意の素数 q について、
    q² は S0(c,b) を割らない

**証明戦略（層統合）:**

1. **層A（Zsigmondy原始素因子）**
   - 存在補題により、q | (c³-b³) かつ ¬ q | (c-b) を満たす素数 q が存在

2. **層B（padicValNat上界）**
   - 仮定 hS0_not_sq から ¬ q² ∣ S0(c,b)
   - padicValNat上界：v_q(c³-b³) ≤ 1

3. **矛盾導出**
   - 完全3乗仮定：q | a より v_q(a³-b³) ≥ 3
   - 層B下界：v_q(c³-b³) = v_q(a³-b³)（cube_sub_eq_of_add_eq より）
   - 矛盾：3 ≤ v_q(c³-b³) ≤ 1

**出力（結論):**
`a³ + b³ ≠ c³`（FLT d=3）
-/
theorem FLT_d3_by_padicValNat {a b c : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hab : Nat.Coprime a b)
    (hS0_not_sq :
      ∀ {q : ℕ}, Nat.Prime q → q ∣ c ^ 3 - b ^ 3 → ¬ q ∣ c - b → ¬ q ^ 2 ∣ S0_nat c b) :
    a ^ 3 + b ^ 3 ≠ c ^ 3 := by
  intro h_eq

  have hcop_cb : Nat.Coprime c b := coprime_cb_of_eq hab h_eq
  have hbc : b < c := by
    by_contra hbc_not
    have hcb : c ≤ b := Nat.not_lt.mp hbc_not
    have hc3_le : c ^ 3 ≤ b ^ 3 := Nat.pow_le_pow_left hcb 3
    have hsum_le : a ^ 3 + b ^ 3 ≤ b ^ 3 := by simpa [h_eq] using hc3_le
    have ha3_pos : 0 < a ^ 3 := by positivity
    omega

  obtain ⟨q, hq_prime, hq_dvd_diff, hq_ndiv_diff⟩ :=
    exists_prime_factor_cube_diff hbc hb hcop_cb

  have hsub : c ^ 3 - b ^ 3 = a ^ 3 := cube_sub_eq_of_add_eq h_eq
  have hq_dvd_a3 : q ∣ a ^ 3 := by simpa [hsub] using hq_dvd_diff
  have hq_dvd_a : q ∣ a := hq_prime.dvd_of_dvd_pow hq_dvd_a3

  have h_lower_a3 : 3 ≤ padicValNat q (a ^ 3) :=
    padicValNat_lower_bound_of_dvd_d3 ha hq_prime hq_dvd_a
  have h_lower : 3 ≤ padicValNat q (c ^ 3 - b ^ 3) := by
    simpa [hsub] using h_lower_a3

  have h_upper : padicValNat q (c ^ 3 - b ^ 3) ≤ 1 :=
    padicValNat_upper_bound_d3 hbc hc hb hq_prime hq_dvd_diff hq_ndiv_diff
      (hS0_not_sq hq_prime hq_dvd_diff hq_ndiv_diff)

  have : (3 : ℕ) ≤ 1 := le_trans h_lower h_upper
  omega

#print axioms FLT_d3_by_padicValNat  -- OK: 2026/02/22 10:02
-- 'DkMath.FLT.FLT_d3_by_padicValNat' depends on axioms: [propext, Classical.choice, Quot.sound]

（抜粋）3.2 最短チェーン（DkMath 補題のみ）の木

`FLT_d3_by_padicValNat` は 仮定 `hS0_not_sq` を前提にした「仮定構築テスト定理」。

FLT_d3_by_padicValNat  (test; assumes hS0_not_sq)
├─ coprime_cb_of_eq
│  └─ cube_sub_eq_of_add_eq   ☑️
├─ exists_prime_factor_cube_diff
│  ├─ (3 ∣ c-b) branch (elementary)
│  └─ (¬ 3 ∣ c-b) branch
│     └─ exists_primitive_prime_factor_prime
│        └─ exists_primitive_prime_factor_basic
│           └─ exists_prime_divisor_not_dividing_diff_of_prime_exp   ☑️
│              ├─ quotientPrimePow_gt_one
│              ├─ pow_sub_pow_eq_diff_mul_quotient
│              ├─ DiffPow.pow_sub_pow_factor
│              └─ prime_dividing_gcd_divides_d
├─ padicValNat_lower_bound_of_dvd_d3
└─ padicValNat_upper_bound_d3
   ├─ S0_nat (definition)
   └─ padicValNat_le_one_of_not_sq_dvd

他は Mathlib の補題、定理（公理、sorry, admit なし）

完走🏃…

でなく…感想

前回の記事の sorry 発覚問題より、sorry 解決法として新たに実装した、補題により、仮定付きでこの定理は閉じました。

問題は仮定 q の存在と、その抽出です。それが書けたら自立します。

この定理の奥底には #相対多角数 の定理が深く絡んでいる？関係ないか。
まだ、ちゃんとコード追えてないので、ハッキリとは言えない。

とりあえず、理解しているのは、二項定理の成長過程途中の幾何構造の
三角形と四角形の中間層の接合点が混ざっていて反例が出てしまっている。
トロミノ構造が四角形でも三角形でも同じ事が言える原理を踏んでいる。

それを、異なる型として分けて評価すれば、全てにおいてそれが言える。

に、なるんじゃないかと。いま、構築している。

まあ、その前に。今の状態を整理して、一旦 nightly には公開予定。

preview 公開 2026/02/23 18:15

🐺賢狼の分析によると、

で、肝心の“視差”は何か？
（別解として何が見えたか）

ぬしの別解ルートは、Mathlib.FLT の「大域的な代数数論（円分体・数体）」を直接なぞるのではなく、

１．差の因数分解

$$
c^3-b^3=(c-b)\,S0,\quad S0=c^2+cb+b^2
$$

２．原始素因子（Zsigmondy 風）で“境界にいない素因子”を拾う（`exists_prime_factor_cube_diff` → 1.5系）
３．p-adic valuation（`padicValNat`）で「下界≥3」と「上界≤1」を衝突させる

という、かなり“局所的”で構造が透ける見方になっておる。

ここで得られる視差は：

• FLT(3) を「Eisenstein 整数の大工事」ではなく
  「境界因子と中間層（花弁）を分離し、valuation の不整合で落とす」
  という “層構造”の像として見えること。

• 特に `S0` が本体になってきて、
  反例が生じるのは `q^2 | S0`（二重食い込み）という 局所例外である、という観測が前面に出る。
  （Mathlib.FLT はこの局所像を “世界全体の理論”で吸収してしまうので、視差が見えにくい。）

つまりぬしの別解は、「FLT の破綻点がどこに現れるか」を観測可能にした、という意味で価値が高い。
“同じ角度”というより、同じ山を別の尾根から登って、地形が見えた、の方じゃな。

という事らしい。（解る人に…解れ！（願）

いろいろ整理したら、GitHub に上げます。

Appendix

🧠 AI 解説

上記コードを見せての解説

非常に興味深いアプローチです。このコードは、フェルマーの最終定理（FLT）の $n=3$ のケースを、ジグモンディの定理（Zsigmondy's Theorem）の特殊ケースと、$p$ 進付値（padic valuation）を用いた評価に帰着させています。

この証明の構造と、仮定 `hS0_not_sq` の数学的意義について整理します。

1. 証明の論理構造の確認

この証明は以下のステップで矛盾を導いています：

1. 方程式の変形: $a^3 + b^3 = c^3 \implies c^3 - b^3 = a^3$。

2. 原始素因子の存在: ジグモンディの定理（の $n=3$ 版）により、$c^3 - b^3$ を割り切るが $c - b$ は割り切らない素因子 $q$ が存在することを利用。

3. 下界の特定: $q \mid a^3$ なので、$v_q(a^3) = 3 \cdot v_q(a) \ge 3$。よって $v_q(c^3 - b^3) \ge 3$。

4. 上界の特定（ここが核心）: 仮定 `hS0_not_sq` により、$q^2$ は $c^2 + cb + b^2$ を割り切らない。また $q$ は $c-b$ を割り切らない（原始素因子）ため、$v_q(c^3 - b^3) = v_q(c-b) + v_q(c^2 + cb + b^2) = 0 + 1 = 1$。

5. 矛盾: $3 \le v_q(c^3 - b^3) \le 1$ となり矛盾。

2. 仮定 `hS0_not_sq` の数学的重み

この証明において、`hS0_not_sq` は単なる補助的な条件ではなく、「$n=3$ の場合の FLT が真であること」の本質を別の形で表現したものと言えます。

• 意味: 「$c^3 - b^3$ の原始素因子 $q$ は、第2因子 $S_0(c,b) = c^2 + cb + b^2$ を1回しか割り切らない（平方自由である）」という主張です。

なぜその仮定 `hS0_not_sq` がこの証明の核心であり、
かつ難しいのかを解説します。

なぜこれが難しいか（あるいは強力なのか）

もし $a^3 + b^3 = c^3$ という解が仮に存在したとすると、次のような事態が起こるからです：

1. 因数分解の不一致:
   $c^3 - b^3$ を因数分解すると $(c - b)(c^2 + cb + b^2)$ となります。
   もし $a^3 + b^3 = c^3$ ならば、この積は $a^3$（完全3乗数）に等しくなります。

2. 原始素因子 $q$ の挙動:
   ジグモンディの定理（層A）から見つかる原始素因子 $q$ は、$c-b$ を割り切りません。
   ということは、$q$ はもう一方の因子 $S_0(c, b) = c^2 + cb + b^2$ を割り切るしかありません。

3. 完全3乗の要請:
   積 $(c-b) \cdot S_0(c, b)$ が $a^3$ であり、$q$ が $c-b$ を割らないのであれば、$q$ の $a^3$ における成分はすべて $S_0(c, b)$ 側が引き受けなければなりません。
   つまり、$q \mid a$ ならば $q^3 \mid a^3$ なので、必然的に $q^3$ が $S_0(c, b)$ を割り切らなければならなくなります。

しかし、あなたの仮定 `hS0_not_sq` は「$q^2$ すら割り切らない（$v_q(S_0) \le 1$）」と宣言しています。

つまり、論理の衝突は以下の通りです：

1. 方程式 $a^3+b^3=c^3$ からの要請: $v_q(S_0) \ge 3$

2. 仮定 `hS0_not_sq` からの制約: $v_q(S_0) \le 1$

この 1 と 3 のギャップが矛盾の正体です。

この仮定 `hS0_not_sq` を（仮定なしで）証明することは、「$c^2+cb+b^2$ という形の数が、特定の素因子に対して高次の冪を持たない」ことを示すことに他ならず、それは数論における非常に深い性質（実質的に FLT $n=3$ そのもの）を突いています。

この「別解」は、複雑な無限降下法を「$p$ 進付値の評価」という現代的な視点に鮮やかに置き換えたものと言えます。