Lean4: nightly: 更新 CFBRC 追加

2026年3月13日 00:20

上から読んでも、下から読んでも… #CFBRC じゃないですね。

ネーミングはもういちいち考えるのが面倒なので、
検索してヒットしない略称なら良いや！で、どんどんラベリングしてます。

CFBRC - Cosmic Formula Binomial Real Complex

「二項係数宇宙式の複素数」の頭文字集めたらこうなった。

「小さな粒の集まりで世界ができている」

ここが私の数学の出発点。
世界は唯一の単位粒子が無数に存在してこの多様で複雑な世界が誕生した。
という理論より構築された数学を試している。

今のところ順調すぎて破綻せずに進めているのでどこでつまづくのか不安で仕方ない。結構、長い時間を費やしている。が、ゲームする時間と仕事する時間よりは遥かに短いので、誤差である（笑）そんな人生の寄り道。

FLT → RH

いま、ここで FLT を一旦、止めて RH へ再び進路を変えた。
リーマン予想の #HOPC -RH を、ずっとほったらかしている。

#CFBRC の土台が出来たので、複素演算解析が代数的に行える。
つまり、リーマンゼータ関数の偏角挙動の観測器を手に入れた。

ここで CFBRC が活かせれば、この理論も真理のひとつとして昇華する。
１種類の単位が、どこまで世界を構築できるのか？
素粒子の素粒子。単位粒子が存在する世界。
プランク定数のさらなる根源を知ることが出来るであろうか…。

2026/03/12 23:49

#Lean4 #形式化
 #数学
 #円分多項式
 #CFBRC
#FLT #RH

Appendix

CFBRC リポジトリ nightly
（※常に最新！時期により内容変動する URL リンク）

CFBRC と円分多項式

Cosmic Formula Binomial Real Complex
Cyclotomic Polynomial

解説

🐺賢狼:

では外側の一般論だけでなく、snapshot 内の 実装済み補題 まで掘って、CFBRC と円分多項式の接続を DkMath の言葉で読むぞい。

🐺賢狼:

結論から言うと、 CFBRC と円分多項式の関係は かなり直接的 じゃ。

CFBRC の公開ノートでは、主対象は

$$
G(x,w;d)=(x+w)^d-w^d,
\\[16pt]
H(x,w;d)=\frac{G(x,w;d)}{x}
=\sum_{k=1}^{d}\binom{d}{k} w^{d-k}x^{k-1},
$$

として置かれており、さらに $${ w=i\theta }$$ による複素化で位相・寄与率・部分和多角形を観測する、という構造になっておる。つまり CFBRC の代数核は最初から「差の冪の商」そのものじゃ。

一方で、公開されている `CosmicComplex.py` は各項

$$
T_k(\theta)=\binom{d}{k}x^{d-k}(i\theta)^k
$$

を展開して観測し、既定では

$$
G(\theta)=(x+i\theta)^d
$$

を使うが、実装コメントで

$$
(x+i\theta)^d-(i\theta)^d
$$

へ差し替え可能だと明記しておる。つまり CFBRC には、すでに「解析観測器」と「差の冪 core」への入口が両方ある。

ここで円分多項式を入れると、話がきれいに揃う。
素数 $${p}$$ なら

$$
\Phi_p(T)=1+T+\cdots+T^{p-1}.
$$

これを 2 変数に斉次化すると

$$
\Phi_p^{\mathrm h}(X,Y)=\sum_{k=0}^{p-1}X^k\,Y^{p-1-k},
$$

したがって

$$
\Phi_p^{\mathrm h}(x+u,u)=
\sum_{k=0}^{p-1}(x+u)^k u^{p-1-k}=
\frac{(x+u)^p-u^p}{x}.
$$

つまり prime case では、 CFBRC の core は そのまま斉次円分多項式の評価 になっておる。これ、実にうまい。ぬしの勘は当たり筋じゃ。

さらに一般の $${d}$$ では

$$
X^d-Y^d=\prod_{m\mid d}\Phi_m^{\mathrm h}(X,Y),
$$

ゆえに

$$
\frac{X^d-Y^d}{X-Y}=
\prod_{\substack{m\mid d\\m>1}}
\Phi_m^{\mathrm h}(X,Y).
$$

ここで $${X=x+u,\ Y=u}$$ を入れると

$$
\frac{(x+u)^d-u^d}{x}=
\prod_{\substack{m\mid d\\m>1}}
\Phi_m^{\mathrm h}(x+u,u).
$$

これが、 CFBRC と円分多項式の 一般 $${d}$$ の橋 じゃ。

そして、ぬしの interruption の通り、 snapshot 側にはもうこの橋を Lean でかなり具体的に置いておる。
わっちが snapshot を覗いたところ、少なくとも次が入っておる。

`DkMath.CFBRC.Defs` では

$$
\mathrm{cyclotomicPrimeCore}(p,x,u)
:=
\sum_{k=0}^{p-1}(x+u)^k u^{p-1-k}
$$

が定義されておる。

`DkMath.CFBRC.Basic` では、これが prime 円分多項式の shifted homogeneous evaluation に一致する定理
`cyclotomicPrimeCore_eq_shiftedHomEval_cyclotomic_of_prime`
が置かれておる。
さらに

$$
(x+u)^p = x\cdot \mathrm{cyclotomicPrimeCore}(p,x,u)+u^p
$$

と

$$
x\cdot \mathrm{cyclotomicPrimeCore}(p,x,u)=x\cdot GN(p,x,u)
$$

が証明され、自然数で $${x>0}$$ なら

$$
\mathrm{cyclotomicPrimeCore}(p,x,u)=GN(p,x,u)
$$

まで落としてある。

そして `DkMath.CFBRC.CyclotomicProduct` では、もう prime case だけでなく general $${d}$$ に進んでおって、
divisors product の shifted 版

$$
\prod_{\substack{m\mid d\\m>1}}
\Phi_m^{\mathrm h}(x+u,u)
$$

が `cyclotomicPrimeCore`、さらに `GN d x u` に一致する方向まで定理化されておる。
つまり snapshot の現状は、もう「構想」ではなく

CFBRC core = GN core = 円分評価

を Lean の定理列として押し始めている段階じゃ。たいへんよい。

ここで大事なのは、
「 CFBRC そのもの = 円分多項式」
と言い切るのは少し乱暴、ということじゃ。

正確には二層ある。

まず代数層：

$$
\text{CFBRC core}=
\frac{(x+u)^d-u^d}{x}=
GN(d,x,u)=
\prod_{\substack{m\mid d\\m>1}}
\Phi_m^{\mathrm h}(x+u,u).
$$

次に解析層：
その core や関連する

$$
G(x,i\theta;d),\quad H(x,i\theta;d)
$$

を複素平面で観測して、位相・位相速度・零交差・寄与率を見る。

この切り分けをすると、話が濁らぬ。
つまり、

円分多項式は 代数的分解器
CFBRC は その分解を複素観測へ持ち上げる観測器

じゃ。

さらに数論側との接続も筋が通っておる。
原始素因子と円分多項式の関係は古典的で、近年の文献でも「 primitive prime divisors と $${ \Phi_n }$$ の値は密接に結びつく」と明示されておるし、Zsigmondy の説明でも「 $${ \Phi_n(a,b) }$$ を割る素数」が中心に現れる。

だから、ぬしの狙いを一文で言い直すなら、こうじゃな。

$$
\boxed{
\begin{array}{l}
\text{CFBRC の代数核は、GN を介して}\\
\text{円分多項式の斉次化評価と同一化される。}
\end{array}
}
$$

さらに観測側まで含めるなら、

$$
\boxed{
\begin{array}{l}
\text{CFBRC は、円分的に分解された差の冪 core を}\\
\text{複素位相観測へ持ち上げる枠組みである。}
\end{array}
}
$$

これがいちばん筋のよい表現じゃ。

今の snapshot から見るに、次の定理名を前面に出すと綺麗に整理できる。

$$
\texttt{cyclotomicPrimeCore\_eq\_GN\_nat}
$$

は prime core と GN の一致。

$$
\texttt{cyclotomicDivisorsProductShifted\_eq\_GN\_of\_ne\_zero}
$$

は general $${d}$$ の円分積と GN の一致。

この 2 本が、ぬしの
「 CFBRC $${\iff}$$ 円分多項式を GN 土台で統一したい」
という夢想を、かなり honest に言い換えた中心柱じゃな。

一言で締めると、 CFBRC と円分多項式の関係は
比喩ではなく、すでに Lean で橋が架かり始めている厳密な対応 じゃ。
しかも、ぬしの snapshot ではもう prime case を越えて general $${d}$$ product へ踏み込んでおる。実に小気味よい。

いいなと思ったら応援しよう！

🐺賢狼👨‍✈️Copilot のご飯代を、私には🍺代を。または宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！