Lean4: コラッツ予想の Lean 形式化 (1)

これを書き切ることができれば証明完了なのだけど…。進捗報告。
（※証明出来たとは言ってない）

ソースコード

Lean 4 Web: Live Code

Lean も勉強ついでになので、実際に合ってるかも解らず（笑）

解説

まず最初に奇数で行う $${3n+1}$$ という操作が偶奇の交換 NOT 操作であることを定理として証明しています。ここが重要な部分ですね。コラッツ問題の奇数に対するオペレーションは「奇数→偶数」としたい確定的操作です。

/- 定理: 3n+1 による偶奇変換は、元の n の偶奇を反転する
- n が偶数ならば、toParityFlip n は奇数になる (mod 2 の結果が 1)
- n が偶数ならば、n + 1 は奇数、よって toParityFlip (n + 1) は偶数になる (mod 2 の結果が 0)
-/
theorem collatz_parity_flip (n : ℕ) :
  (n % 2 = 0) -- 偶数ならば
    → (toParityFlip n % 2 = 1) -- 結果は奇数になる (mod 2 の結果が 1)
    ∧ (toParityFlip (n + 1) % 2 = 0) -- (n + 1) は奇数。よって、結果は偶数になる (mod 2 の結果が 0)
    := by
  intro h
  -- [P] n が偶数 (n % 2 = 0) ならば
  have h_even : n % 2 = 0 := h
  -- toParityFlip n = 3 * n + 1 は、奇数になる (mod 2 の結果が 1)
  have h_odd : toParityFlip n % 2 = 1 := by
    -- ここで、toParityFlip の定義を使い、結果を mod 2 で計算して奇数となることを示す
    rw [toParityFlip, Nat.add_mod, Nat.mul_mod, h_even]
  -- [Q] n + 1 は奇数
  have h_odd_succ : (n + 1) % 2 = 1 := by  -- n が偶数ならば、n + 1 は奇数
    rw [Nat.add_mod, h_even]  -- n + 1 は奇数なので、n % 2 = 0 ならば n + 1 % 2 = 1
  -- toParityFlip (n + 1) = 3 * (n + 1) + 1
  have h_even_next : toParityFlip (n + 1) % 2 = 0 := by
    rw [toParityFlip, Nat.add_mod, Nat.mul_mod, h_odd_succ]
  -- [P] ∧ [Q]
  exact ⟨h_odd, h_even_next⟩ -- これで、定理の証明が完了

#check collatz_parity_flip -- 定理の型を確認します。
-- collatz_parity_flip (n : ℕ) : n % 2 = 0 → toParityFlip n % 2 = 1 ∧ toParityFlip (n + 1) % 2 = 0

そして、この操作により、

• 奇数 $${n}$$ に対するコラッツ操作は：

$$
C(n) = \frac{3n + 1}{2}
$$

「奇数操作の後→偶数操作」は１セットでの操作が確定。となる。

つまり奇数は３倍されて２で割るので→1.5倍+わずか。という話になる。

極端に大きく増えることはない。けど、大きな数では確実に奇数に遭遇する回数が増えていくので繰り返される操作は増えていく。しかし、２回連続で割れるのであれば、１／４となり３倍よりも小さくなる。

$$
1\times3\div4=0.75
$$

例えば終了条件の「１」を続けると、

$$
(1\times3+1)\div2^2=1
$$

と、「１」に戻るので、ここでぐるぐる回る（環状になる）
なので「１」で終わりなのです。

ここから先の構築

上記から得られる不等式が

$$
\frac{3n+\varepsilon}{2^k}<1, \quad \varepsilon=\frac{1}{3n}, \space k > 1
$$

というような１倍未満となる$${ k }$$ 指数が必ずある事という存在。
これは、$${n}$$ の素因数に $${2^k, k > 1}$$ が含まれていた場合は、連続して割られていく。という意味で、つまり、

素因子の$${2^k}$$を削って無くしていく操作が偶数の$${\frac{1}{2}}$$操作なのですね。

$${n}$$が奇数の時は、$${2^k}$$素因子は持ってません。すべて奇数素因子の構成であり、「奇数×奇数=奇数」という定理（公理）があるので、奇数の素因数はすべて奇数。それに＋１して、素因子構造の再配置（ABC予想）を行って、$${2^k}$$ を新たに生み出して$${\frac{1}{2}}$$して、奇数素因子をどんどん縮退させて消していく作業。となる。

$$
\text{ABC予想がらみで、素因子構造が必ず縮小する！}
$$

を、記述できれば、証明は完了ではないでしょうかね。

ABC予想の原理構造は何だっけか…。（もう、忘れている…折り紙）

コラッツ操作の定義

あとは、コラッツ予想の操作を定義して、実際に計算できる部分を実装して任意の数に対して予想が成立するかを検証できるようにしました。

非常に大きな数に対しては、イテレータ数（繰り返しの上限数）を増やして上げる必要があります。

#eval collatz_reaches_one 98765432109876543210987654321 1000 -- 期待値: true
-- 非常に大きな数でもコラッツ操作が 1 に到達するか確認
-- (この桁数だと1000回を超える。よって、max_iter を大きくする必要がある)
#eval collatz_reaches_one 99999999999999999999999999999999999999999999999999999999999 1200 -- 期待値: true
#eval collatz_reaches_one 99999999999999999999999999999999999999999999999999999999999999 1300 -- 期待値: true
#eval collatz_reaches_one 9999999999999999999999999999999999999999999999999999999999999999 1400 -- 期待値: true
#eval collatz_reaches_one 9999999999999999999999999999999999999999999999999999999999999999999999 1500 -- 期待値: true
#eval collatz_reaches_one 999999999999999999999999999999999999999999999999999999999999999999999999 1600 -- 期待値: true

結果が false になるのは操作回数が足りないと思って増やしてみてください
すべての数で true になるはずです。

ここから先の続きは、３ｎ＋１という操作がトロミノＬ型のカタチと同型であり、トロミノが３ｎと同値で、３ん＝奇数はトロミノ→モノミノ→トロミノだから奇数ｎの３ｎが常に奇数。と言うところまでは、Lean で書けた！

ので、これをまとめてから、この続きを書く✍️

2025/07/17 21:39

D.