Lean4: sorry 仮証明

宿題の話です。書き方解る人、教えて欲しい…。以下記事の最後。

※注意：
私のために、改めて調べないでください。
あなたの貴重な時間を奪いたくはありません。

既に知っている。あなた自身も知りたい。と、思った場合のみ取り組むのは構いません。答えが解って、教えたいな。と思ったらのならば、教えて下さい。その解決法は、ちゃんとここで記事にいたします。

数学は時間泥棒ゲームです！✍️大事なことなので。

$$
\begin{align*}
A\cdots f(n, k) &= \underbrace{T(T(T(\cdots T(n))))}_{k\text{-times}}, \quad T = \lambda x.(3x+1)\\
&\small\text{（ T に与えられた $n$ は、ラムダ式の$x$に渡される）}\\B\cdots f(n, k) &= 3 ^ k \times n + \frac{(3 ^ k - 1)}{2} \\
\end{align*}
$$

この２つの関数は同値です。ですが、簡単に Lean で書けないんですよね…。
未熟者ですので…。AI も書けませんでした！！これが私の宿題です。

一般化式の恒等式は以下となります。

$$
f_k(n) = \underbrace{a (a ( \cdots a n + b ) + b ) + \cdots + b}_{k \text{ 回}} = a^k n + b \cdot \frac{a^k - 1}{a - 1}
$$

仮証明

定義上と演算結果が同値なら…

こまけぇこたぁいいんだよ!!

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring

/- 起点となる定義 -/
def fa (n k : ℕ) : ℕ := Nat.iterate (λ x => 3 * x + 1) k n -- 再帰的な反復
def fb (n k : ℕ) : ℕ := 3 ^ k * n + (3 ^ k - 1) / 2 -- fa の閉形式

#check fa -- fa (n k : ℕ) : ℕ
#check fb -- fb (n k : ℕ) : ℕ


def fa_list (n k : ℕ) : List ℕ := List.range (k) |>.map (λ i => fa n i)
def fb_list (n k : ℕ) : List ℕ := List.range (k) |>.map (λ i => fb n i)

#eval fa_list 1 5 -- [1, 4, 13, 40, 121]
#eval fb_list 1 5 -- [1, 4, 13, 40, 121]

-- fa = 3x+1 の反復、fb = 閉形式
def f_iter (n k : ℕ) := fa n k
def f_closed (n k : ℕ) := fb n k

-- 補題：これらは等しい
lemma L_iter_eq_closed (k n : ℕ) : fa n k = fb n k := by sorry
  -- この証明は後で実装（pending: rw 展開に失敗するので展開用の補題が必要）

-- 主定理
theorem fa_eq_fb (n k : ℕ) : f_iter n k = f_closed n k := L_iter_eq_closed k n

-- OK
example : fa_list 1 5 = fb_list 1 5 := by
  rfl -- rfl succeeds because both sides are definitionally equal

-- rfl succeeds because both sides are definitionally equal
example : fa 1 3 = fb 1 3 := by rfl
example : fa 2 2 = fb 2 2 := by rfl
example (n : ℕ) : fa n 1 = fb n 1 := by rfl
example (n : ℕ) : fa n 0 = n := by rfl

-- NG
-- example (k : ℕ) : fa 1 k = fb 1 k := by rfl
-- tactic 'rfl' failed, the left-hand side f_1 1 k is not definitionally equal to the right-hand side
-- example (n k : ℕ) : fa n k = fb n k := by rfl
-- tactic 'rfl' failed, the left-hand side f_1 n k is not definitionally equal to the right-hand side

-- ここでの rfl は失敗する。なぜなら、fa と fb は定義的に等しいが、引数 n と k が異なるため。
-- つまり、n と k が同じでないと rfl は成功しない。


/- 一般化 -/
def L (x : ℕ) : ℕ → ℕ := λ n => x * n + 1

def L_iter (x n k : ℕ) : ℕ := Nat.iterate (L x) k n

def L_closed_form (x n k : ℕ) : ℕ :=
  x^k * n + (x^k - 1) / (x - 1)

def L_general (a b n k : ℕ) : ℕ :=
  a^k * n + b * ((a^k - 1) / (a - 1))

/- 詳細は未証明、定義的には一致だけで通す（仮証明） -/
lemma L_iter_eq_closed_form (x n k : ℕ) : L_iter x n k = L_closed_form x n k := by sorry
lemma L_iter_eq_general (a b n k : ℕ) :   L_iter a n k = L_general a b n k := by sorry

-- 定理として形式化（仮定理）
theorem test_main_theorem_1 (x n k : ℕ) : L_iter x n k = L_closed_form x n k :=
  L_iter_eq_closed_form x n k
theorem test_main_theorem_2 (a b n k : ℕ) : L_iter a n k = L_general a b n k :=
  L_iter_eq_general a b n k

-- 3 と 1 の場合の例
#eval L 3 1 -- 4
#eval L_iter 3 1 1 -- 4
#eval L_closed_form 3 1 1 -- 4
#eval L_general 3 1 1 1 -- 4

-- 3 と 2 の場合の例
#eval L 3 2 -- 7
#eval L_iter 3 2 1 -- 7
#eval L_closed_form 3 2 1 -- 7
#eval L_general 3 1 2 1 -- 7

-- 5 と 1 の場合の例
#eval L 5 1 -- 6
#eval L_iter 5 1 1 -- 6
#eval L_closed_form 5 1 1 -- 6
#eval L_general 5 1 1 1 -- 6

-- 6 と 5 の場合の例
#eval L 6 5 -- 31
#eval L_iter 6 5 1 -- 31
#eval L_closed_form 6 5 1 -- 31
#eval L_general 6 1 5 1 -- 31

-- 123 と 5 の場合の例
#eval L 123 5 -- 616
#eval L_iter 123 5 1 -- 616
#eval L_closed_form 123 5 1 -- 616
#eval L_general 123 1 5 1 -- 616

-- これは fa と fb の一般化された形であり、L の特定のケースとして考えることができる。
-- ここで、x = 3, n = 123, k = 5 として考える。
-- fa 123 5 と fb 123 5 は同じ値を返す。
-- つまり、L 123 5 は fa 123 5 と同じ値を返す。
-- したがって、L 123 5 は 616 になる。
-- これは、fa と fb が定義的に等しいことを示す一例である。
-- ここで、L は fa と fb の一般化された形であり、L_iter, L_closed_form, L_general はそれぞれ
-- 反復、閉形式、一般化された形である。
-- これらの関数は、fa と fb の定義的な等価性を示すために使用される。

Lean 4 Web: Live Code

ソースコード

解説

恒等式

$$
\begin{align*}
A=f(n, k) &= \underbrace{T(T(T(\cdots T(n))))}_{k\text{-times}}, \quad T = \lambda x.(3x+1)\\
&\small\text{（ T に与えられた $n$ は、ラムダ式の$x$に渡される）}\\
B=f(n, k) &= 3 ^ k \times n + \frac{(3 ^ k - 1)}{2} \\
\end{align*}
$$

$$
A_k(n)=B_k(n)
$$

上式より以下、ふたつの定義が同値であることを証明したい。

/- 起点となる定義 -/
def fa (n k : ℕ) : ℕ := Nat.iterate (λ x => 3 * x + 1) k n -- 再帰的な反復
def fb (n k : ℕ) : ℕ := 3 ^ k * n + (3 ^ k - 1) / 2 -- fa の閉形式

別名式を用意（エイリアス）

-- fa = 3x+1 の反復、fb = 閉形式
def f_iter (n k : ℕ) := fa n k
def f_closed (n k : ℕ) := fb n k

そのまま参照しているので処理は全く一緒。

-- 補題：これらは等しい
lemma L_iter_eq_closed (k n : ℕ) : fa n k = fb n k := by sorry
  -- この証明は後で実装（pending: rw 展開に失敗するので展開用の補題が必要）

補題として等式で結び「等価である」と適当に (by sorry) 言っておく。

-- 主定理
theorem fa_eq_fb (n k : ℕ) : f_iter n k = f_closed n k := L_iter_eq_closed k n

主定理のほうで f_iter = f_closed は「等価である」と述べる。その理由は、補題 L_iter_eq_closed だから。と主張すると…。

補題は sorry 付いているので警告が出る。
あとでちゃんと証明しておくようにと。

主題は、何でかOK✅️✅️となる。補題が未完なのに主題側が通される。
バグではなく、Lean の特徴らしい。

このへんをちゃんと学ぶ必要がある✍️私へ

同一性の比較には幾つかあるっぽい

よく解ってないので、ちゃんと説明できないのですが。
定義的同一性と代数的同一性というふたつの比較があるみたいです。
この前者の「定義的」という点では OK を貰える。

-- rfl succeeds because both sides are definitionally equal
example : fa 1 3 = fb 1 3 := by rfl
example : fa 2 2 = fb 2 2 := by rfl
example (n : ℕ) : fa n 1 = fb n 1 := by rfl
example (n : ℕ) : fa n 0 = n := by rfl

これらの rfl は definitionally で一致している。と判断されて OK となる。

しかし、以下の場合は通らない。

-- NG
-- example (k : ℕ) : fa 1 k = fb 1 k := by rfl
-- tactic 'rfl' failed, the left-hand side f_1 1 k is not definitionally equal to the right-hand side
-- example (n k : ℕ) : fa n k = fb n k := by rfl
-- tactic 'rfl' failed, the left-hand side f_1 n k is not definitionally equal to the right-hand side

-- ここでの rfl は失敗する。なぜなら、fa と fb は定義的に等しいが、引数 n と k が異なるため。
-- つまり、n と k が同じでないと rfl は成功しない。

この違いが、まず私はよく解っていない。

与えるパラメータが同じでないと？の意味が私には通じていないのだろう。
n だけの時は通るのに、k だけのときは通らない。n k 両方も通らない。

謎である。

一般化式

再掲

$$
f_k(n) = \underbrace{a (a ( \cdots a n + b ) + b ) + \cdots + b}_{k \text{ 回}} = a^k n + b \cdot \frac{a^k - 1}{a - 1}
$$

/- 一般化 -/
def L (x : ℕ) : ℕ → ℕ := λ n => x * n + 1

def L_iter (x n k : ℕ) : ℕ := Nat.iterate (L x) k n

def L_closed_form (x n k : ℕ) : ℕ :=
  x^k * n + (x^k - 1) / (x - 1)

def L_general (a b n k : ℕ) : ℕ :=
  a^k * n + b * ((a^k - 1) / (a - 1))

係数３に限らず、この等価性は汎用らしい。

今回、証明に使いたいのは「３」なので、こちらはコラッツ予想一般化においての証明用となろうか。奇数ｎ倍＋１、偶数ｍ分の１でも成り立つのか？です。

こちらも、同様の仮証明で一旦、通してある。

ここで悩んでいても仕方ないので。とにかく #eval テストにて同じ値が返ってくる。という事実は変わらないので、単純に Lean が自動的に式変換して代数解を求められない。AI も、どう書いていいかよく解んない！という状態なんですね。

ここで人類の出番ですが…。
イテレータ式を展開って、どうするのかさっぱりです。連分数みたいな？

式の等価性証明

🤷‍♀️ sorry

なんで反復式と閉形式が、同じになるのか解らないので説明しようがないですね。魔法式だからです！（これでいい👍️（いやよくない❗️（汗😅💧）））

きっとこれを説明できるようになったら書けるようになってるのでしょう…

おわりに

この式が宇宙式とどのように関係してくるのか？とか、この式も宇宙式みたいな神秘を秘めているのか？興味あるのですが。コラッツさんて何を研究してた方なのでしょうかね？そっちから調べるという手もあるか。

うん。さっぱり解らん✨️

私のためではなく、あなたのために。ですよ。

人としての時間は有限。存在は無限。なので人をやめた時に、異なる存在では理解できるようになってるから。人の時に今、知りたいかどうかです。✍️

D.