Lean4: 解説: KUS 構造

#Lean4 #形式化証明 #KUS #解説

KUS 構造とは何か

値の背後にある「単位」と「設計図」を失わないために

数学では、ふつう数は「値」として扱われる。
たとえば $${3}$$、$${7}$$、$${0}$$ という具合じゃ。

だが実際には、その値が どの単位世界で観測されたものか 、そして どの設計図の上に立っているのか が、隠れてしまっていることが多い。
特に零 $${0}$$ は強い。零になると、そこに至るまでの構造をまとめて飲み込んでしまう。

わっちが今回実装した KUS 構造 は、その「飲み込まれていた構造」を、きちんと残すための仕組みじゃ。

1. KUS は数を 3 つ組で見る

KUS では、数を単なる値ではなく、次のような構造体として扱う。

$$
(K, U, S_U)
$$

ここで

• $${K}$$：観測される係数

• $${U}$$：単位・格子幅・座標系

• $${S_U}$$：その単位 $${U}$$ に従属する blueprint（設計図）

を表す。

大事なのは、$${S}$$ が独立したただの飾りではないことじゃ。
設計図は常に単位に従って意味を持つので、正確には $${S_U}$$ と書く。
つまり「どの単位世界で見ているか」に応じて、設計図の解釈も変わる。

これは、数の背後にある構造をはっきり表に出すための第一歩じゃ。

2. なぜ零を特別に扱うのか

通常の数体系では、

$$
a \cdot 0 = 0
$$

となる。
もちろん計算としては正しい。だが、その瞬間に

• もとの単位は何だったか

• どの設計図を持っていたか

• 何が零化され、何が残ったのか

という情報は見えなくなる。

KUS では、零状態を単なる $${0}$$ に潰さず、

$$
(0, U, S_U)
$$

として保持する。
つまり、失われるのは係数 $${K}$$ だけであり、単位 $${U}$$ と設計図 $${S_U}$$ は残る という考え方じゃ。

これが KUS の最初の核心じゃな。
零とは「何もない」ではなく、可視量が消えた構造状態 と読む。

3. KUS は「変な数体系」ではない

ここは誤解されやすいところじゃが、KUS は零除算を正当化したいわけでも、奇妙な新数体系を作りたいわけでもない。

KUS がやりたいのは、もっと地味で、しかしずっと重要なことじゃ。

それは、数の計算の背後にある

• 単位

• support

• 設計図

• 零化の痕跡

を、値とは別の層として保持すること。

言い換えると、KUS は 値の数学に、構造の記憶を戻すための枠組み じゃ。

4. 同じ support なら演算できる

KUS では、同じ support を持つもの同士なら、加法や乗法のような演算を自然に考えられる。

これは直感的にも自然じゃろう。
同じ座標系、同じ単位格子、同じ設計図面の上にあるものなら、その場で足したり掛けたりしてよい。

だが、問題は support が異なる場合じゃ。

たとえば、片方はある単位世界 $${U_1}$$、もう片方は別の単位世界 $${U_2}$$ にいるとする。
このとき、両者をいきなり足し合わせるのは危うい。
方眼紙の目盛りが違うのに、そのまま重ねるようなものだからの。

そこで KUS では、異なる support 同士を直接演算せず、いったん共通の調和 support $${H}$$ へ運んでから演算する。

図式で書けば、

$$
US_1 \to H \leftarrow US_2
$$

という形じゃ。

つまり、

１．左を共通 support $${H}$$ にエンコードする
２．右も共通 support $${H}$$ にエンコードする
３．$${H}$$ 上で演算する
４．必要なら元の世界や別の世界へ戻す

という流れになる。

この考え方を、わっちは KUS transport として実装した。

5. DHNT とのつながり

この transport の考え方は、動的調和数論 DHNT と強く結びつく。

DHNT は、数を固定された一つの姿ではなく、スケール変換や指数対数の関係を通して見直す理論 じゃ。
要するに、数を「どの座標で見るか」によって姿が変わることを、むしろ本質として扱う。

KUS は、その DHNT が与える調和座標を、単位と設計図を持つ構造体の形へ落とし込む器になる。

DHNT が「どう見るか」を与え、KUS はそれを「どう保持するか」を与える。
この役割分担が、なかなか美しいのじゃ。

6. CosmicFormula とのつながり

さらに KUS は、宇宙式ともつながる。

宇宙式では、Big / Body / Gap のように、数や図形を分解して読む視点が重要になる。
たとえば

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

という形で、全体と内部構造を分けて見る。
この視点は、値だけを見ていると掴みにくいが、KUS のように単位と設計図を保持する構造を通すと、かなり扱いやすくなる。

流れとしては、

$$
\mathrm{CosmicFormula}
\;\to\;
\mathrm{DHNT}
\;\to\;
\mathrm{KUS\ transport}
$$

と見るのが自然じゃ。

• CosmicFormula が 絶対量や幾何構造 を与える

• DHNT がそれを 調和座標へ符号化 する

• KUS がそれを 型付きの support 構造として保持し、運ぶ

こうして、ばらばらに見えていた理論群が、ひとつの流れの中に入ってくる。

7. KUS 構造の核心

結局のところ、KUS の核心は次の一文に尽きる。

数を、値だけでなく、単位と設計図を背負った存在として扱うこと。

そのために KUS は、

$$
(K, U, S_U)
$$

という形を取り、
零状態を

$$
(0, U, S_U)
$$

として保持し、
異なる support 間の演算を transport によって安全に定義する。

つまり KUS は、単なる演算規則ではない。
構造を失わないための数学的な器 じゃ。

8. おわりに

ふつうの数学では、値が主役じゃ。
だが、値だけを追っていると、単位や設計図、そして零に沈んだあとの痕跡が見えなくなる。

KUS は、その見えなくなっていた層を、もう一度表へ引き上げるために作られた。
言うなれば、

値の背後にある世界を、忘れずに持ち歩くための構造 じゃな。

今後はこの KUS を足場にして #DHNT や #CosmicFormula との接続をさらに強めていくつもりじゃ。
数はただ並んでいるのではなく、それぞれの単位世界と設計図の上に立っておる。
そこを忘れずに見ていくと、なかなか面白い景色が開けてくるぞい。

2026/03/16 0:48

D.

Appendix

リポジトリ main / DkMath.KUS