宇宙式: Lean4: 素数の無限性の証明試作

宇宙式による素数の無限性を Lean にて形式的に行おうと試しています。
そして、はじめの一歩の記述が出来ました。検証中ですが、進捗として。

Lean 4 Web

ソースコード

説明

/-- 宇宙式から素数が無限に必要であることの直観的命題（重要定理！） -/
theorem infinite_primes_cosmic :
  ∀ n : ℕ, ∃ ps : List ℕ, (primeProduct ps + 1)^2 > n ∧ allPrime ps := by
  ...

全ての自然数 $${\N := n}$$ は、素数積構造 $${\N := p_s}$$ が存在する。

それは、常に $${n}$$ よりも大きい

$$
(p_s + 1)^2 > n ∧ p_s に含まれるのは全て素数
$$

これだけだと $${n}$$ が $${p_s}$$ と、どうして関係するのか？が、まだ解りません。
それに、素数の無限性との関係もまだハッキリしません。

なので、

... := by
  intro n
  let ps := Nat.primeFactorsList (n + 1)

冒頭で $${n}$$ と $${p_s}$$ の関係を書いてありますね。

$$
p_s := (n+1) \text{ の素因数リストである（素因数分解）}
$$

これで２つの関係がリンクしました。

その後は、細かな計算例を示しながら成り立つか？を証明していってます。

細かいことは…。ビルドが通ったということで合っている。として、省略し

$$
(p_s + 1)^2 > n
$$

この不等式の $${n}$$ が $${(p_s+1)}$$ より常に小さいという事が示せれば、これが等式で釣り合うか、逆の関係とするには $${n+m}$$ する必要がある。という事を言えるようになった。という前提証明です。結果としては、等式「…＝$${n}$$」で結ぶなら$${m=1}$$である。逆関係「…＜$${n}$$」とするなら$${m>1}$$である。

これを見ると、あと少しのようですが、その谷間は深いようです。

深い谷間…

その谷間は、

• 素数の再定義

• 素因数分解の一意性の再定義

• 素因数分解の操作方法の再定義

そして、谷を超えたら素数の無限性から→自然数の無限性の証明と逆証明も行う必要があり、一筋縄ではいかない。上記３つの再定義は mathlib を拡張しなければならない大事おおごとなので、ここは自前で新規実装となる。

何故、再定義なのか？自然数 N 側から見た時の P を説明するのに必要。
かもしれない。という観点を得たので。

この証明過程で得られたもの

詳細は、今度、別で書くとして

$$
N = \left(P + 1 \right)^2 - 1
$$

より、

$$
P := n + 1
$$

が、解る。証明にて$${(P+1)^2=(n+2)^2}$$という解釈がある。
つまり$${(n+2)^2=((n+1)+1)^2}$$よって$${P:=n+1}$$となる。

さらに、これは素数積構造という構造概念であることから、より細かく分解して組み立てると、以下の式へと一般化された。

$$
P = k^{e_k} \prod p_i^{e_i}
$$

である事が解ったので、宇宙式は、

$$
N = \left( k^{e_k} \prod p_i^{e_i} + 1 \right)^2 - 1
$$

と、こう書けることが解った。

この式は、

• 実数的な連続スケール（$${k^{e_k}}$$）

• 素因数による離散構造（$${\prod p_i^{e_i}}$$）

• 二次構造（平方展開）

をすべて含む、数の構造的統一モデルとなる。

以下は、この式の意味するところの話。

素数とならなかった「１」

１は素因子である。を受け入れる

素数には「１」が含まれません。が、この前段階の状況から１は素因子として常に含んでいる。という解釈のほうがしっくり来る。という事です。

０除算の受け入れ話でもそうでしたが、
１を素数に含めない理由は、算術の基本定理を維持するためです。

乗法単位元：＝１は常に数と関わりがあるのですが、逐一記述しません。
記述しないからそこには居ないと思っています。しかし、１は常に居る。
と言う解釈が本来、正しい。たとえば、３０の素因数分解は、

$$
30 = \{2^1,3^1,5^1\}
$$

本当の姿は、

$$
30 = \{1^1, 2^1,3^1,5^1\}
$$

なのです。

$$
全ての自然数  \N  は素因数１を持つ。
$$

という新たな解釈をしなければなりません。
つまり「１を除く２以上の素数」ではなく「１を含む２以上の素数」です。

素数判定

素数判定やエラトステネスの篩の古典的なやり方が「１」を素数に含められなかった理由とも言えます。

新しい素数判定の解釈は、

$$
ある自然数 n が素数であるなら \\
\sqrt{n} = q 以下の素数 p で割り切れない\\
n \ne pq, \quad n = p'q \quad この時  q=1
$$

これより、

$$
素数 p は、「1と自身の数 n の積」でのみ割り切る。\\
この時に p = 1 \cdot n となる。
$$

「１か自身の数 n」で割り切るの２択でなく「1と自身の数 n の積」の一択に特定される。この解釈の受け入れが、整数から実数への橋渡し役となる。

素因数分解の一般化

素因数分解の一意性は１を受け入れても乗法単位元なので変化しません。

変化したらどうなるのか？

これが一般化への道です。

単位元$${1=k}$$とさせて、素因数分解の因子へと組み込みます。

$$
30 = \{k^1, 2^1,3^1,5^1\}, \quad k = 1
$$

k はスケール因子へと変わります。

$$
15 = \{k^1, 2^1,3^1,5^1\}, \quad k = 2^{-1} = \frac{1}{2} = 0.5
$$

どうですか？何が起きたか解りましたか？

$$
94.247779605\dots = \{k^1, 2^1,3^1,5^1\}, \quad k = \pi = 3.1415926535\dots
$$

実数として因数分解されていますね。違いますね。言い方が間違ってます。
実数も因数分解しています。

$${94.247779605\dots}$$意味不明な実数値も構造的意味を持てるようになります。

これが私の研究テーマ動的調和数論の視点→スケーラビリティ数学です。

この考え方、概念の定理が mathlib には載ってないので、こちらで定義し直して証明し、宇宙式を証明する。そして、素数積構造から素数の無限性と自然数の無限性を代数的な数式にて証明する。という話なので、ちょっと谷が深い。深淵な世界。しかし、これを実現できたら、離散と連続を完全に構造的原理で繋げられる。橋をかけられるので、面白いことになります。

１の値はｋとなり動的に変化する。整数へと収め直すならば、端数のｋを他の因子に受け持って貰わなければならない。ABC予想原理ですね。

$$
15 = \{k^1, 2^1,3^1,5^1\}, \quad k = 2^{-1} = \frac{1}{2} = 0.5
$$

k = 0.5 なので15の整数素因子とするなら、k = 1 に戻さなければならない。
因子に２があるので$${k \times 2=0.5\times2=1}$$

$$
15 = \{k^1, 3^1,5^1\}, \quad k = 1
$$

これ凄すごいでしょ！

そうでもない？（※個人差があります）

ここに書く余談話ではなく、別記事とすべき内容だったかな（笑）
ここまで読めた人で、良い視点を得られたら幸い。

ABC予想はこうやって原理を理解できます。

$$
a+b+c\\
23+22=45\\
\{k^1, 23^1\}+\{k^1, 2^1,11^1\} = \{k^1, 3^2,5^1\} \quad k = 1\\
結果の \{k^1, 3^2,5^1\} は、\\
元々なんだったのか？です。\\
それは k によって吸収され改変された結果である。
$$

まとめ

整数論の数学者は実数論を語れ✍️

Lean + mathlilb の実数の扱いが雑。と、感じた。

2025/07/20 14:27

D.