Lean4: DkMath.KUS と リーマン予想

リーマン予想の形式化作業中…

ゼロ点座標とゼロ点を扱う事柄なので、なんでも情報をゼロに潰して、
もとの情報が何だったのかが得られない。そんな問題を抱え続ける。

そこで昔、作っておいた Framework が役に立つ（証明済み）

DkMath.KUS

それを解決するのが DkMath.KUS Framework この定理のおかげで、
型を壊さず構造を保持し値は$${K=0}$$に。それが何だったのか？は、

$$
S(U)
$$

が覚えている。

$$
N=K\cdot S(U)
$$

KUS という名前だが、式構造はこうなる（なってしまった）

• $${K:=\mathrm{Scale}}$$

• $${U:=\mathrm{Unit}}$$

• $${S:=\mathrm{Structure}}$$

である。

S という設計図（元の術式）その尺度となる基準単位は U 単位（最小）
それを目的の数になるように K でスケーリングする。

e.g.

$$
5 = 9*(1/3)*(5/3)=5
$$

$$
10=16*(1/4)*(10/4)=10
$$

$$
N=K*(1/u)*(n/u)
$$

数値計算だと、みたいな感じです。
この例だと $${K=u^2}$$ ですかね。

これを汎用的に型代数的に扱えるようにしたもの。

演算は K ですべて行う。US 成分は演算には触れない。
結果 K=0 となっても US 成分は残る。型検証に使える。というわけです✍️

2026/08/03 2:25 草稿
2026/08/17 0:03 投稿

D.

#DkMath #KUS #Lossless

（公式リリース時には KSU に改名して公開するかな…🤔
　いやエイリアスにしておこう…🐺賢狼と話が合わなくなる…）

🧠 note AI れびゅー補足解説

ご提示いただいた内容は、数学的あるいはプログラミング的な概念（特にゼロによる情報喪失の回避）を独自のフレームワークとして定義しようとする興味深い試みだと感じました。

内容についてのレビューをいくつかまとめます。

1. コンセプトの独創性

「値が0になっても構造（型）を保持する」という目的は、計算機科学における「型システム」や、物理演算における「次元解析」に通じる実用的な視点です。特に「ゼロに潰れて元の情報が失われる」という問題へのアプローチとして、$S(U)$ という項に情報を退避させる考え方は明確です。

2. 数式の構成と整合性

例示されている数式について、いくつか確認・整理が必要な点があります。

• 例の整合性:

  • $5 = 9 \times (1/3) \times (5/3)$ は計算すると確かに $5$ になります。

  • このとき、$u=3$ とすると $K=9$ なので、ご自身で書かれている通り $K=u^2$ の関係が成り立っています。

• 変数の役割:

  • $N = K \cdot (1/u) \cdot (n/u)$ という式において、$n$ が「元の値」だとすると、$K=u^2$ の時に $N=n$ となり、恒等式として機能しています。

  • 「演算は $K$ ですべて行う」というルールにおいて、$K=0$ になった際、数式全体としては $0$ になりますが、背後に $S(U)$ という「構造の記録」が残るというロジックは一貫しています。

3. ブラッシュアップのための提案

• $S(U)$ の定義の具体化: 「$S$ は設計図（元の術式）」とありますが、これが具体的にどのようなデータ形式（あるいは代数的性質）を持つのかを少し掘り下げると、より説得力が増します。例えば「単位の次元（$L, M, T$ など）」なのか、「演算の履歴」なのか、といった点です。

• 「型検証」への応用:
  「結果 $K=0$ となっても US 成分は残る」という点は、例えば「0メートル」と「0秒」を区別できるというメリットとして強調すると、読者に利点が伝わりやすくなります。

4. 文章のトーン

開発日誌や技術メモとしては、現在の「✍️」を用いた少し砕けたスタイルで問題ないと思います。もし論文や公式ドキュメント風にするのであれば、冒頭の「なんでも情報をゼロに潰して」を「情報の消失（Information Loss）」といった用語に置き換えると、より専門的な印象になります。

全体として、独自の理論体系（KUS Framework）としての骨組みはしっかりしていると感じました。