Lean: 無次元宇宙式の単位Gap保存則

量を変えること無くカタチを変えられるトポロジーの世界ですが、
平面における、その分解能の最低解像度が「４」分割である。
のような１２０年来の問題解決したという論文があります。

(PDF) https://arxiv.org/pdf/2412.03865

平面の正三角形を４ピースに分けて、正方形を作る。
これが出来るのは４ピースまでで、３ピースでは出来ない。が判明した。

これが意味するのは、宇宙式構造（トロミノ構造）の

$$
\Large
3+1=4
$$

である必要がある。と、私は見ています。
「３」が動くには、余白の「１」が存在していないと出来ない。です。

なので全体として「４」必要になる。「３」の実体は変わる必要はない。

はい。前置きでした。
（これは、これで別途証明してみる新しい課題）

この平面を立体幾何にまで拡張して最低解像度は幾つなのか？
を、また１２０年の難問にしたいと思います（笑）🤣

答えは二項定理にあります。自己相似展開構造です。

以下が、その解析ツールになるであろう一つの証明です。

セルの無次元化

いままで平面構造のトロミノ構造を扱ってましたが、
これを無次元化させます。直交する軸を複数持たせる。

$$
\text{Cell d $\to$ Cell$_2$ = Cell 2 \qquad (alias)}
$$

すると実体部 #Body の構造が二項定理の原理で複雑化していきます。
しかし、複雑化してもその余白構造 #Gap は、変わらない。
実体の大きさ$${x}$$に対する影響を受けない。
全体 #Big の余白（隙間）は常に確保される。
影響は受けないが全体を保つために$${x}$$には依存する。

ということが判明した結果と言えるでしょう。

これは、以下の作業の続編です。

宇宙式の無次元化＝一般宇宙式の形式化が終わって、残る作業は、

Cell := ℤ×ℤ を Cell d := Fin d → ℤ に

まだ、Cell の定義が平面世界の 2D 構造なので、
こちらも無次元化しないといけないのです。

ということで、サクッと（？）完了しておきました。

Lean 形式化

リポジトリ（ブランチ）

※ main マージ済み

ソースコード

該当するコードは以下２つ

• CellDim.lean

• CosmicFormulaCellDim.lean

ドキュメント

今は、作業ノート的な感じでまとめてあります。
そして、まだ GitHub上では数式がちゃんと表示されませんので、
VSCode 側などの Markdown Viewer で見てください。

→ CosmicFormulaCellDim.md

とりあえず、今まで語ってきたことが、
間違ってなさそうだなあ…ということは解った。

ちょっと解説

ここで行った作業は #単位宇宙式 の係数「２」を #無次元化 させて、
$${G_d(x,u)}$$ という構造へ取り替えたこと。そして、単位は、

$$
U_d:=u\to u^d
$$

と、多次元に出来ること。

それでも、基本単位（乗法の単位元）の「１」は、

$$
U_d:=\sqrt[d]1=1\;\to\;1^d=1
$$

変わらず「１」のままである。

$$
どんなカタチでも単位が保存される。\to \space u^d
$$

ということです。

なんだか自明である事を一生懸命やってる気もするのだけど（笑）

主目的は、ここから Lean について学ぶこと。
動いている（ビルドが通る）は、言語上は正しいという証拠。
答えがここにあるのだから、これが何故、成り立つのか？
を後で追って理解すれば良い。✍️

2026/01/24 5:39

D.

#Lean #形式化証明
#宇宙式 #無次元宇宙式 #一般宇宙式
平面セル集合から構造セル集合へ

Appendix

単位宇宙式

$$
U := f(x;u) \;=\; (x+u)^2 - x(x+2u) \;=\; u^2
$$

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

$$
U_d:=f(x,u,d) \;=\; (x+u)^d - x\,G(d,x,u) \;=\; u^d
$$

幾何和版 G

$$
G(d,x,u) := \sum_{k=0}^{d-1}(x+u)^{\,d-1-k}\,u^k,
$$

$$
(x+u)^d-u^d \;=\; x\cdot G(d,x,u).
$$

これより

$$
\#\mathrm{Body}(d,x,u)=x\cdot G(d,x,u).
$$

宇宙式構造

$$
\#\mathrm{Big}=\#\mathrm{Body}+\#\mathrm{Gap}.
$$

• $${\#\mathrm{Big}:=(x+u)^d}$$

• $${\#\mathrm{Body}:=x\cdot G(d,x,u).}$$

• $${\#\mathrm{Gap}:=u^d}$$

$${x\ は\ u^d\ に影響を与えないが\ x\ に依存している}$$