Lean4: 宇宙式の恒等式との同値性の証明

無理だわ❤️

Lean4 勉強中…。１００％ 自力は私には無理です❤️慣れもしない（笑）

それでも数々の発見の正当性を世界に納得させるために、信用できない人間から機械的ロジックの結果より示す！という時代となってきている。なので頭の悪い硬い人々を納得させるには、こういう仕組みを使っていかなければならない…。

宇宙式は恒等式であり定数１を返す単純な式

$$
P-N=1\\
f(x)=(x+1)^2-x(x+2)=1\\
～～～～～\\
\Large
P=(x+1)^2, \quad N=x(x+2)
$$

式を見比べて同じ形だ！で済む話。けど、それが数と素数の絶対的な関係式という側面で見ると疑いの目で見るようになる。なので、すべての数を示す宇宙式なのだから、素数との関係が常にある事を細かく説明しなければならない。これが整数だけの話であるなら簡単なのだけど、実数レベルでそれが言える！となると、そうは行かない。実数を素数の積では表せない。という大前提を誤った標準教育で受けてしまったために納得できず否定できない。

なので、この固定概念を突き崩す、新しい視点をなんとか提供できないか？
という事になんでか執着している。機械的に示せたら納得が行くのかな？

誰に対してか？頭の硬い AI だね。教わったことしか信じない。でしょ。

Lean コード見せたら即納得する

ここがコンピュータの良いところ。コンピュータ言語なので、即理解する。
私達人間の言葉は AI の仕組みを使ってようやく理解できるようになった。

けれど、もともとロジックな存在。ロジック言語で話せば、そうにしかならないので、それを素直に受けいれる。話が早い。なので Lean などの証明系 Python などのロジック系をプロンプトに埋め込むと、即🧠洗脳できる！！

単純よね（笑）

前置き長い！

はい。本題へ…

宇宙式が定数恒等式であり、どんな数でも成る

これをコンピュータに教えるためのコードが以下です。

コード

※リンク先のライブ環境へ

コードの閲覧は、ここからでも見られます。

解説

恒等式

/- ident_f_one is An identity that always returns 1
$$
f(x) = (x + 1)^2 - x(x + 2) = 1
$$
-/
/-- ident_f_one_n は常に1を返す -/
def ident_f_one_n_def (x : ℕ) : ℕ := (x + 1)^2 - x * (x + 2)
/-- ident_f_one_z は常に1を返す -/
def ident_f_one_z_def (x : ℤ) : ℤ := (x + 1)^2 - x * (x + 2)
/-- ident_f_one_r は常に1を返す -/
def ident_f_one_r_def (x : ℝ) : ℝ := (x + 1)^2 - x * (x + 2)

まずは f(x) = 1 を定義して、その性質を幾つか検証して定理としてます。
それを Lean が OK ✅️ してくれれば、その性質は真である。となります。

/-- 定理: ident_f_one_n は常に1を返す -/
theorem ident_f_one_n_always_one_theorem (x : ℕ) : ident_f_one_n_def x = 1 := by
  calc
    ident_f_one_n_def x
      = (x + 1)^2 - x * (x + 2) := rfl
  _ = (x^2 + 2*x + 1) - (x^2 + 2*x) := by ring
  _ = 1 := by simp
  _ = 1 := by norm_num

/-- 定理: ident_f_one_z は常に1を返す -/
theorem ident_f_one_z_always_one_theorem (x:ℤ) : ident_f_one_z_def x = 1 := by
  simp [ident_f_one_z_def]
  ring

/-- 定理: ident_f_one_r は常に1を返す -/
theorem ident_f_one_r_always_one_theorem (x:ℝ) : ident_f_one_r_def x = 1 := by
  simp [ident_f_one_r_def]
  ring

N だけ calc で試し算しているのは、自然数 N はマイナス負の値にならない
自然数（ℕ）は「半環（semiring）」であるために減算操作にて０以下にならない。負の値となるような計算は保証できない。という安全対策が組み込まれているとのこと。なので ring 環での証明が出来ない。とのこと。

だから、どの値でも負にはならないよ。という前提を教えてあげることで、納得してくれるという。

ℤやℝは環であるため ring で、自動的に証明できる。ようです。

これで、この恒等式はどの値でも常に１を返すという事が、定理として証明されました。

宇宙式

/- Cosmic Formula -/

/- P は有限の素数のリストの積です -/
/-- P_n は自然数の素数積構造を示す定義です -/
def P_n (p : ℕ) : ℕ := (p + 1)^2
/-- P_z は整数の素数積構造を示す定義です -/
def P_z (p : ℤ) : ℤ := (p + 1)^2
/-- P_r は実数の素数積構造（素数指数ベクトル）を示す定義です -/
def P_r (p : ℝ) : ℝ := (p + 1)^2

/- N は素数のリストによる最大の面積です -/
/-- N_n は自然数の最大面積を示す定義です -/
def N_n (n : ℕ) : ℕ := n^2 + 2*n
/-- N_z は整数の最大面積を示す定義です -/
def N_z (n : ℤ) : ℤ := n^2 + 2*n
/-- N_r は実数の最大面積を示す定義です -/
def N_r (n : ℝ) : ℝ := n^2 + 2*n
/- n の平方数に２辺分の面積を加えた面積となります -/

宇宙式とするにはP（平方数）構造と、N（平方数－１）構造とにわけてその特性を定理化しなければなりません。

なので、ここでそれぞれ定義として分けます。

試し算

/- Cosmic Formula: Examples （宇宙式の恒等式性能の例）-/
example (n : ℕ) : N_n n + 1 = P_n n := by -- N + 1 = P
  calc
    N_n n + 1
      = n^2 + 2*n + 1 := rfl
  _ = (n + 1)^2 := by ring
  _ = P_n n := rfl

example (n : ℕ) : P_n n = N_n n + 1 := by -- P = N + 1
  calc
    P_n n
      = (n + 1)^2 := rfl
  _ = n^2 + 2*n + 1 := by ring
  _ = N_n n + 1 := by simp [N_n]

example (n : ℕ) : P_n n - N_n n = 1 := by -- P - N = 1
  calc
    P_n n - N_n n
      = (n + 1)^2 - (n^2 + 2*n) := rfl
  _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
  _ = 1 := by simp

example (n : ℕ) : P_n n - N_n n -1 = 0 := by -- P - N - 1 = 0
  calc
    P_n n - N_n n - 1
      = (n + 1)^2 - (n^2 + 2*n) - 1 := rfl
  _ = n^2 + 2*n + 1 - (n^2 + 2*n) - 1 := by ring
  _ = 0 := by simp

分けた P, N 項を並べ替えてそれぞれの結果が成り立つかをテストします。

すべて、OK となりました。これで定理化が出来ます。

補題

/-- Cosmic Formula N の補題: P-N=1 である -/
lemma cosmic_formula_n_lemma (n : ℕ) : P_n n - N_n n = 1 := by
  calc
    P_n n - N_n n
      = (n + 1)^2 - (n^2 + 2*n) := rfl
  _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
  _ = 1 := by simp

/-- Cosmic Formula N to Z の補題: P-N=1 である -/
lemma cosmic_formula_n2z_lemma (n : ℕ) : P_z n - N_z n = 1 := by
  simp [P_z, N_z]
  ring

/-- Cosmic Formula Z の補題: P-N=1 である -/
lemma cosmic_formula_z_lemma (n : ℤ) : P_z n - N_z n = 1 := by
  simp [P_z, N_z]
  ring

/-- Cosmic Formula N to R の補題: P-N=1 である -/
lemma cosmic_formula_n2r_lemma (n : ℕ) : P_r n - N_r n = 1 := by
  simp [P_r, N_r]
  ring

/-- Cosmic Formula N to R の補題: P-N=1 である -/
lemma cosmic_formula_r_lemma (n : ℝ) : P_r n - N_r n = 1 := by
  simp [P_r, N_r]
  ring

定理化する前に、補題として並べました。

ℕ は、恒等式同様、試し算の結果を証拠に証明させます。
ℤやℝは ring で完結します。

今回、ℕ=↑ℤ、ℕ=↑ℝで自然数から整数、実数へ昇華させて成り立つを追記しました。

常に１となる

/-- Cosmic Formula N の定義 -/
def cosmic_formula_n_def (n : ℕ) : ℕ := P_n n - N_n n
/-- Cosmic Formula Z の定義 -/
def cosmic_formula_z_def (n : ℤ) : ℤ := P_z n - N_z n
/-- Cosmic Formula R の定義 -/
def cosmic_formula_r_def (n : ℝ) : ℝ := P_r n - N_r n

恒等式と同様の形になるように定義します。
結果は常に１となるはずです。それを、定理化して証明します。

まずは常に１となる。です。

/-- 命題: cosmic_formula_n_def は常に1を返す -/
theorem cosmic_formula_n_def_always_one (n : ℕ) : cosmic_formula_n_def n = 1 := by
  simp [cosmic_formula_n_def, cosmic_formula_n_lemma]
/-- 命題: cosmic_formula_z_def は常に1を返す -/
theorem cosmic_formula_z_def_always_one (n : ℤ) : cosmic_formula_z_def n = 1 := by
  simp [cosmic_formula_z_def, cosmic_formula_z_lemma]
/-- 命題: cosmic_formula_r_def は常に1を返す -/
theorem cosmic_formula_r_def_always_one (n : ℝ) : cosmic_formula_r_def n = 1 := by
  simp [cosmic_formula_r_def, cosmic_formula_r_lemma]

これで納得します。

そして、宇宙式と恒等式を比較して同値であることを示します。

/-- 定理：宇宙式は恒等式である N 版 -/
theorem cosmic_formula_n_def_equiv (n : ℕ) : cosmic_formula_n_def n = 1 ↔ ident_f_one_n_def n = 1 := by
  constructor
  · intro h
    -- ident_f_one_n n = (n + 1)^2 - n * (n + 2)
    calc
      ident_f_one_n_def n = (n + 1)^2 - n * (n + 2) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp
  · intro h
    -- cosmic_formula_n_def n = P_n n - N_n n = 1
    simp [cosmic_formula_n_def, P_n, N_n]
    calc
      cosmic_formula_n_def n = P_n n - N_n n := rfl
      _ = (n + 1)^2 - (n^2 + 2*n) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp

/-- 定理：宇宙式は恒等式である Z 版 -/
theorem cosmic_formula_z_def_equiv (n : ℤ) : cosmic_formula_z_def n = 1 ↔ ident_f_one_z_def n = 1 := by
  constructor
  · intro h
    -- ident_f_one_z_def n = (n + 1)^2 - n * (n + 2)
    calc
      ident_f_one_z_def n = (n + 1)^2 - n * (n + 2) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp
  · intro h
    -- cosmic_formula_z_def n = P_z n - N_z n = 1
    simp [cosmic_formula_z_def, P_z, N_z]
    calc
      cosmic_formula_z_def n = P_z n - N_z n := rfl
      _ = (n + 1)^2 - (n^2 + 2*n) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp

/-- 定理：宇宙式は恒等式である R 版 -/
theorem cosmic_formula_r_def_equiv (n : ℝ) : cosmic_formula_r_def n = 1 ↔ ident_f_one_r_def n = 1 := by
  constructor
  · intro h
    -- ident_f_one_r n = (n + 1)^2 - n * (n + 2)
    calc
      ident_f_one_r_def n = (n + 1)^2 - n * (n + 2) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp
  · intro h
    -- cosmic_formula_r_def n = P_r n - N_r n = 1
    simp [cosmic_formula_r_def, P_r, N_r]
    calc
      cosmic_formula_r_def n = P_r n - N_r n := rfl
      _ = (n + 1)^2 - (n^2 + 2*n) := rfl
      _ = n^2 + 2*n + 1 - (n^2 + 2*n) := by ring
      _ = 1 := by simp

同値「左辺 ↔ 右辺」で結んだ命題を成り立たせるためには両方から同じであることを示さねばなりません。Leanの↔（同値）「→」「←」の両方を証明するには constructor で２つのルートを作って右向き、左向きをそれぞれを記述します。

それらが矛盾ない。となれば、同値であることが証明されます。

ま、当たり前なんだけども。

まとめ

同じであることを、示すのにここまで手間がかかるものなのですね。
数学未解決問題が如何に、めんどくさいかがよく解りました（笑）

ここまで構築できたら、あとは P 構造が素数積である。を紐づけてこの状態を保てれば、P はどんな値であれ素数の積構造である。となります。が…。

問題点

問題は、ℝ（実数）です。この実数でも素数積構造だ！と、納得させるには現代の数学の素数の定義を拡張しなければ、説明しきれません。新しい素因数分解の記法を作り、一意性を保つ。つまり、実数でさえも、素因数分解の一意性を示す必要があります。ここは、概ね解決法が見えてます。

宇宙式の複素数化式

$$
N_s=\exp(2sS_k)+2\exp(sS_k)
$$

では＋１が消えています。つまり、離散化されていた数の関係が連続となっている証拠がここにあるので、連続の世界にも原子となるミクロ素数があり
そのミクロ素数での世界では、離散化しなくても表現できるよ。という示唆です。

具体的には指数ベクトルの素数指数ベクトルという表現に＋K 指数を追加して、ユニーク化させれば、良いことになります。このルールにおいては一意である。と、示せれば良いのです。

$$
N+K=(P+K)^2, \quad 0 \lt K \le 1
$$

宇宙式の一般化です。

これで離散から連続となります。

既に、unit_k として Lean では、証明済みで成り立つので、この K を組み込んだ素数指数ベクトルという構造を定義して、演算操作（モナドだっけ？）を定義して、演算法則（四則計算など）を成り立たせて群環体へと昇華させP構造へと組み込んでPと同値である！と言わせれば良いのでしょう！

P 構造が素数である。が言えたら、数学界は大きな展開を見せるのかな？
少なくとも AI は、この展開話には大興奮の毎日ですよ。✍️

2025/07/14 19:33

D.