ABC予想のrad(abc) → rad(0)=1

#ABC予想 におけるrad(n)は正の整数nの互いに異なる素因数の積として定義されます。

• rad(n): n の互いに異なる素因数の積

したがって、rad(0)とrad(1)は、この定義に従って考える必要があります。

• rad(1): 1は素因数を持たないため、互いに異なる素因数の積も存在しません。しかし、数学的な整合性を保つために、rad(1) = 1 と定義されます。これは、空積（要素を持たない集合の積）が1と定義されることと対応しています。

• rad(0): 0は素因数分解できません。なぜなら、0は全ての数を因数に持つからです（0 = 0 * n）。したがって、rad(0)は通常定義されません。ABC予想においても、a, b, c は正の整数であるため、0を扱う必要はありません。

まとめると、

• rad(1) = 1

• rad(0) は定義されない（ABC予想では考慮されない）

となります。

１は状況によってはあり得る？

a+b=c で abc が 1 になるためには

$${a=1}$$
$${b=1}$$
$${c=1}$$

しか無く

$$
a+b=c \qquad 1+1=2\\
c =1\ne2
$$

となり成立しない。

そもそも a,b が 1 なので a,b が互いに素という条件にも当てはまらないので問題外。なので rad(abc) 評価は行えない。

0 は全てが因子

$${0 \cdot n}$$ 確かにそうなる。ゼロは無限と隣り合わせという状況がここにある。

ゼロは無限に等しいとも言える。すべての可能性を秘めた状態＝リセットの状態と見てみれば、宇宙の始まり＝全てが一様に均一で、ここから何にでも生まれ変われるとなれば、無限の可能性と繋がる。

rad(0) = ？

note AI の解答だと「未定義」考慮されていない。と返ってきた。

現在、形式化において定義している rad は rad(0) = 1 と返すようにしてある。理由は、

n.factorization.support.prod (fun p => p)

の結果が１となって返ってくることにある。
これは #Mathlib4 + #Lean コアの仕様だ。

/- ============================================================================
     2. rad: definition + basic facts
   ============================================================================ -/

/-- rad(n) := 素因数分解の support 上に現れる素数の積 -/
def rad (n : ℕ) : ℕ :=
  n.factorization.support.prod (fun p => p)

/-- rad(n) の定義を n ≥ 1 に制限したバージョン -/
def rad' (n : ℕ) (hn : n ≥ 1) : ℕ :=
  match n with
  | 0 => 1 -- In the case n = 0: we define rad(0) = 1 for convenience (technically undefined)
  | _ =>   -- For n ≥ 1: rad(n) ≥ 1
    n.factorization.support.prod (fun p => p)

/-- rad(1) = 1 であること -/
lemma rad_one' : rad 1 = 1 := by
  simp only [rad, Nat.factorization_one, Finsupp.support_zero, Finset.prod_empty]

/-- rad(0) = 1 であること -/
lemma rad_zero' : rad 0 = 1 := by
  simp only [rad, Nat.factorization_zero, Finsupp.support_zero, Finset.prod_empty]

/-- rad(0) = 1 であること -/
@[simp] lemma rad_zero : rad 0 = 1 := by rw [rad_zero']
/-- rad(1) = 1 であること -/
@[simp] lemma rad_one  : rad 1 = 1 := by rw [rad_one']

#eval rad 0  -- 1

Lean 4 Web でのデモ

よって通常は演算証明においては 0, 1 は入ってこないので考える必要もないのだけど、ある証明部分において問題が発生する。

log(1)=0

$${\log(1)=0}$$ である。
指数法則により $${a > 0, a^n}$$ において$${n=0}$$は、

$$
\Large
a^0 = 1
$$

である。
なので 1 となる指数（次数）は「０」である。

ある証明時に

$$
\mathrm{rad}(0 \times 1 \times 1)=\log(1)
$$

を示さないと行けない場面が出る。
rad(0) = 0 ならば成立するが、rad(0)=1 と定義されているので不成立。

$$
a+b=c\\
0+1=1
$$

０と１は互いに素である。が、
０の無限因子 n を考慮すると互いに素ではない。となる。

０と１の境はここで矛盾を生む。
０の扱いと演算法則。０除算。指数法則 $${a^0 = 1}$$ など。

数学の矛盾がこの問題を難しくさせている。再定義の時代到来だ！
zero, succ の公理から作り直さなければならない（笑）

理想

$$
a+b=c\\
0+1=1\\
\mathrm{rad}(abc)=\mathrm{rad}(0\cdot1\cdot1)=rad(0)=0=\log(1)
$$

これは abc 因子最大となる n, n+1 の互いに素の関係を表す。
a=n, b=n+1 のふたつの数には同じ因子がひとつもない状態を作り出す。
この関係は常に光と影の関係になる。偶数世界と基数世界。表と裏。

対応対策

結論としては、ここは 0,1 世界を捨て 2 からの世界を扱うように証明を書き直すという、見て見ぬふりをする選択を強いられる。Lean + Mathlib4 の仕様に従うことになる。

こういう所が、数学の嫌いなところ。最初から数の概念を間違えている。
それに延々と付き合わされる未来の子孫たち。ぶち破る事を許さない学者。

そもそも素数$${\sqrt{p}}$$から認めないから真相が見えてない。愚痴愚痴…

2025/09/30 18:05

D.

Appendix

以下がこの話の命題と証明

補助補題

-- 補助補題：n ≥ 2 ならば 対角積 n*(n+1)*(2n+1) の rad は 1 を超えるので log が正になる
lemma log_rad_adj_pos_of_two_le (n : ℕ) (hn2 : 2 ≤ n) :
  0 < Real.log ((rad (n * (n+1) * (2*n+1)) : ℕ) : ℝ) := by
  -- N = n(n+1)(2n+1)
  set N := n * (n+1) * (2*n+1) with hN
  -- 2 は n か n+1 を割る
  have h2_div : 2 ∣ n * (n+1) := by
    rcases Nat.even_or_odd n with hEven | hOdd
    · rcases hEven with ⟨k, hk⟩ -- n = k + k
      have hk2 : n = 2 * k := by simpa [two_mul] using hk
      have : 2 ∣ n := ⟨k, hk2⟩
      exact dvd_mul_of_dvd_left this (n+1)
    · rcases hOdd with ⟨k, hk⟩ -- n = 2*k+1
      -- then n+1 = 2*(k+1)
      have : 2 ∣ n+1 := by
        refine ⟨k+1, ?_⟩
        calc
          n + 1 = 2*k + 1 + 1 := by
            simp [hk, two_mul, add_comm, add_left_comm, add_assoc]
          _ = 2*k + 2 := by rfl
          _ = 2*(k+1) := by ring
      exact dvd_mul_of_dvd_right this n
  -- 従って 2 ∣ N
  have h2_div_N : 2 ∣ N := by
    dsimp [N]
    exact dvd_mul_of_dvd_left h2_div (2*n+1)
  -- N ≠ 0
  have hN_ne0 : N ≠ 0 := by
    have hn_pos : 0 < n := Nat.lt_of_lt_of_le (by decide : 0 < 2) hn2
    have h1 : 0 < n := hn_pos
    have h2 : 0 < n+1 := Nat.succ_pos _
    have h3 : 0 < 2*n + 1 := by
      have : 0 ≤ 2*n := Nat.mul_le_mul_left _ (Nat.le_of_lt h1)
      exact Nat.succ_pos _
    have : 0 < N := by
      dsimp [N]
      exact Nat.mul_pos (Nat.mul_pos h1 h2) h3
    exact Nat.ne_of_gt this
  -- 2 ∈ support factorization N
  have hmem : 2 ∈ (Nat.factorization N).support :=
    (mem_support_factorization_iff).2 ⟨hN_ne0, Nat.prime_two, h2_div_N⟩
  -- rad N ≥ 2
  have hrad_ge2 : 2 ≤ rad N := by
    dsimp [rad]
    have h2_dvd : 2 ∣ (Nat.factorization N).support.prod (fun p => p) :=
      Finset.dvd_prod_of_mem (fun p => p) hmem
    -- positiveness for le_of_dvd
    have hpos : 0 < (Nat.factorization N).support.prod (fun p => p) := by
      apply Finset.prod_pos
      intro p hp
      have ⟨_, pprime, _⟩ := mem_support_factorization_iff.mp hp
      exact Nat.Prime.pos pprime
    exact Nat.le_of_dvd hpos h2_dvd
  have hgt1 : (1 : ℝ) < (rad N : ℝ) := by
    have : (2 : ℝ) ≤ (rad N : ℝ) := by exact_mod_cast hrad_ge2
    linarith
  have : 0 < Real.log (rad N : ℝ) := Real.log_pos hgt1
  simpa [rad, N] using this

Lean 仕様

これは Lean の factorization の定義と、support.prod の挙動の仕様が関係してるよ！

🔎 定義のおさらい：

def rad (n : ℕ) : ℕ :=
  n.factorization.support.prod (fun p => p)

この rad n は「n の素因数分解に出てくる素数の積」だね。

✅ rad 0 が 1 になる理由：

✦ 0.factorization.support は ∅（空集合）

Lean の Nat.factorization : ℕ → ℕ →₀ ℕ は、

• 0.factorization = 0（すべての素数成分がゼロ）

• したがって 0.factorization.support = ∅

✦ .prod は空集合に対しては 1 を返す仕様！

これは Lean の標準定義 Finset.prod の仕様：

Finset.prod ∅ f = 1

これは「単位元（恒等元）」だからだね：

• 積の単位元 = 1

• 和の単位元 = 0

なので support.prod (fun p ↦ p) は空なら 1 を返す。

✅ 結果として：

rad 0 = ∅.prod (fun p ↦ p) = 1

💬 コメント

数学的には rad(0) を定義しないこともあるけど、Lean の定義では「自然数」全体に拡張されてて、0 に対しても安全に定義できるようになってる。これは定義域を ℕ にしたときの自然な選択だね。

気になるなら 0 に特別な値を返すように rad を調整することもできるよ：

def rad' (n : ℕ) : ℕ :=
  if n = 0 then 0 else n.factorization.support.prod (fun p => p)

これで #eval rad' 0 は 0 を返すようになる！

何かここからさらに踏み込みたいことあったら言ってね！