Lean: 宇宙式: 無次元化版の形式化

$$
\Large
x\,G_{d-1}(x,u)
$$

これを形式化したかったのでやってみた系

無次元化版宇宙式（一般化宇宙式）

$$
\Large
U_d(x;u)=\\[6pt]
f(x;u,d) =(x+u)^d - x\,G_{d-1}(x,u)=u^d
$$

$$
\large
G_{d-1}(x,u)=\frac{(x+u)^d-u^d}{x}=\sum_{k=0}^{d-1}\binom{d}{k+1}u^{\,d-1-k}\,x^{k}.
$$

これは正しかったという話です。Lean は認めた。

x\,G_{d-1}(x,u)

U_d(x;u) = f(x;u,d) = (x+u)^d - x\,G_{d-1}(x,u)=u^d

G_{d-1}(x,u)=\frac{(x+u)^d-u^d}{x}=\sum_{k=0}^{d-1}\binom{d}{k+1}u^{\,d-1-k}\,x^{k}.

$$
U_d(x;u) = (x+u)^d - \left(x\,\sum_{k=0}^{d-1}\binom{d}{k+1}u^{\,d-1-k}\,x^{k}\right)=u^d
$$

U_d(x;u) = (x+u)^d - \left(x\,\sum_{k=0}^{d-1}\binom{d}{k+1}u^{\,d-1-k}\,x^{k}\right)=u^d

$${\tiny\text{Gemini に清書させたもの}}$$

$$
U_d(x;u) = (x+u)^d - \left( x \sum_{k=0}^{d-1} \binom{d}{k+1} u^{d-1-k} x^k \right) = u^d
$$

$${\tiny\text{合ってる！}}$$

二項定理

$$
\large
(a+b)^n=\sum_{r=0}^n\ _nC_r\,a^{n-r}\,b^r
$$

$${\ _nC_r := \binom nr = \frac{n!}{k!(n-k)!}\quad 組み合わせの数}$$

(a+b)^n=\sum_{r=0}^n\ _nC_r\,a^{n-r}\,b^r

\ _nC_r := \binom nr = \frac{n!}{k!(n-k)!}

により、

$$
G_{d-1}:=\sum_{k=0}^{d-1}\ _dC_{k+1} = \sum_{k=0}^{d-1}\binom d{k+1} = \sum_{k=0}^{d-1}\frac{d!}{(k+1)!\big(d-(k+1)\big)!}
$$

関数電卓で計算可能なレベルの式表現

$$
U_d(x;u) = (x+u)^d - \left( x \sum_{k=0}^{d-1} \frac{d!}{(k+1)!(d-(k+1))!} u^{d-1-k} x^k \right) = u^d
$$

G_{d-1}:=\sum_{k=0}^{d-1}\ _dC_{k+1} = \sum_{k=0}^{d-1}\binom d{k+1} = \sum_{k=0}^{d-1}\frac{d!}{(k+1)!\big(d-(k+1)\big)!}

U_d(x;u) = (x+u)^d - \left( x \sum_{k=0}^{d-1} \frac{d!}{(k+1)!(d-(k+1))!} u^{d-1-k} x^k \right) = u^d

関連記事：以下を Lean で示せた！✅️

Lean コード

リポジトリ（ブランチ）

ソースコード

• CellDim.lean

• CosmicFormulaCellDim.lean

ドキュメント

• CosmicFormulaCellDim.md

※数式を見たい場合は、VSCode の Markdown ビュアーで見てください。
　まだ GitHub 用に最適化していません。（自動化ツールを通してない）

この結果より、
二項定理版だけでなく「箱／量」で見ても良いという事が解った。

“箱” Box と “量＝card” の次元一般化

$$
\Large
\#\mathrm{Box}(a)=\prod_{i\in \mathrm{Fin}\ d} a_i
$$

$$
\Large
\prod_{i\in\mathrm{Fin}\ d} n = n^d
$$

\#\mathrm{Box}(a)=\prod_{i\in \mathrm{Fin}\ d} a_i

\prod_{i\in\mathrm{Fin}\ d} n = n^d

ここまで確定事項

以下は、妄想…💭

ちゃんと理解してないけど、直感的には以下の記事の話になるのかな？
＋１して次元空間埋め尽くせば次元昇華する。$${V_d+1 \to V_{d+1}}$$

$$
D = p^d \to D_{\text{base}}^d, \quad V=p\times D \quad (d=\text{Dimension},  p = D_{\text{base}}\in \mathbb{P})
$$

$$
\Large
p^d=D, \quad V = p\times D = p^1\cdot p^d = p^{d+1}\\[6pt]
\normalsize
p\text{-進数}  d  次元:  p^d  が満たされた空間の総量は  p^{d+1}  次元昇華↑
$$

実体 #Body は、満たされる前の１つ手前$${\#\text{Body} = V-1}$$ か？

D = p^d \to D_{\text{base}}^d, \quad V=p\times D \quad
(d=\text{Dimension}, p = D_{\text{base}}\in \mathbb{P})

p^d=D, \quad V = p\times D = p^1\cdot p^d = p^{d+1}

考察

元々は「定数」その構造は、単位を示す。
Lean 形式化で「ある定数」を証明した話になるのだけど、
それを細分化しても、次元変えても、定数は保存される。
が解ったと言うだけのこと。なのだけども…。

物理

エネルギーが、その場所から移動するには、その場にいる自身の状態を保存したまま移動しなければならない。その時、移動に際して余裕が無いと動けないのです。

量子化された１状態から次の状態へ移る時、
エネルギーは、増えたり減ったりは出来ない。

しかし、今の場所から隣へ移る時、手足を伸ばす必要がある。
その時、伸ばした手足は、増えるのではなく、単純移動です。

単純移動＝エネルギー保存状態のままということです。

これが、実は単純ではなくカタチを変えても等価を保ち続ける必要がある。
となると、伸ばす方向、退く場所のエネルギー状態を同時刻で両方行う必要がある。

これは、非常に難しいですよ？
時間差があってはいけない。結果的に同じはダメ。
となると、動けないですよね？

なので、空間を移動するのに「時間がかかる」というタイムラグが発生している。重力はさらに空間自体を常に動かしまくっている。その場に停滞とは移動し続ける空間に逆らう動きです。逆らわないならばそれは「自由落下」運動になります。

時間が移動（加速度）、重力に影響して「遅れる」とは、
このエネルギー空間移動の「タイムラグ」の積み重なりの現象になります。

タイムラグを許しているのは、単位空間の余白です。
これがなければ、世界は動けない。

違うか。✍️

2026/01/23 3:08

D.

#Lean #形式化証明
#宇宙式 #無次元宇宙式 #一般化宇宙式
#数学 #二項定理