Lean4: 日記: CFBRC - Cosmic Formula Binomial Real Complex の形式化に着手

#FLT 形式化に疲れたので、別のことをする。
と言っても FLT などで使うことになろう定理群なので全く異なるものでもない。

これの形式化を行う。

$$
\frac{(x+u)^p-u^p}
{x}
$$

これを利用して #複素演算 を実装し、通常の複素数演算と等価であることを示すのが狙い。すると複素演算中の多項式の状態を得ることが出来、位相、偏角の変化により、多項式がどのように変化するのかが見えるようになると見ている。

そして、これが #円分多項式 の構造原理を説明するツールとなるであろう。

たぶん。

現在実装中。至極当然のごとくと言わんばかりに、素直に宇宙式 GN との接続を可能とし、円分多項式との繋がりを形成する補題が立ち上がっている。

#Zsigmondy だけでは不足していた FLT 形式化証明において、この補題が加わることで、FLT n > 3 より高次の具体的証明に繋がることを願って…。

2026/03/12 15:08

D.

#Lean4 #形式化 #CFBRC

Appendix

早速公開 nightly snapshot