Lean 4による多次元コラッツ木における構造的複雑度界 K < N の形式検証【プレプリント】
Title: Formal Verification of Structural Complexity Bounds K < N in Multidimensional Collatz Trees via Lean 4
Abstract (150–250 Words)
This study applies the Dynamic Fregean Axioms, previously established to structuralize and elucidate the operational mechanics of the Collatz Conjecture, to the Hyama Conjecture, which extends the original problem into a multidimensional natural number topology. By dismantling the unconscious omission of dynamic causality (the actual execution steps of node generation and bit-shifting) traditionally forgotten and rejected in classical static mathematics, we extend the theoretical framework of Strong Normalization based on multidimensional infinite tree topology to a higher algebraic dimension. Spatial structures expanding across 1D (\(N+1\)), 2D (\(2N+1\)), and 3D (\(4N+1\)) are formulated through a unified bit-shift generator \(2^k N + 1\) (\(k \in \{0, 1, 2\}\)) corresponding to modulo algebra (\(\text{mod } 2, \text{mod } 4\)). Furthermore, using the interactive theorem prover Lean 4 (leveraging Mathlib's omega tactic), we present a fully automated, defect-free formal proof showing that the number of traversals \(K\) along the 3D information compression axis (\(4N+1\)-type steps) for any starting node value \(N\) is strictly bounded by the algebraic absolute ceiling \(K < N\). This formal verification confirms the inherent structural contraction of the dynamic tree, demonstrating that when execution processes are fully recovered without omission, the generative complexity is naturally encapsulated within its own initial boundaries.
概要（Japanese / 512文字）
本研究では、前研究のコラッツ予想の構造的解明において導入した「動的フレーゲ公理」を基礎とし、同予想を自然数の多次元トポロジーへと拡張した「Hyama予想」への応用を展開する。
従来の古典数学が実無限の静的空間を前提とすることで、無意識に排斥・忘却してきた「動的原因（ノード生成やビットシフトの実プロセス）」の省略を打破し、多次元無限木トポロジーおよび動的フレーゲ公理に基づく強正規化の理論枠組みをさらに高次へと拡張する。
1次元（\(N+1\)）、2次元（\(2N+1\)）、3次元（\(4N+1\)）へと展開される空間構造を、モジュロ代数（\(\text{mod } 2, \text{mod } 4\)）に対応する統一的ビットシフト生成子 \(2^k N + 1\) （\(k \in \{0, 1, 2\}\)）として定式化する。
その上で、3次元情報圧縮軸（\(4N+1\) 型ステップ）における通過回数 \(K\) が、出発する任意のノード値 \(N\) に対して常に代数的絶対天井 \(K < N\) を満たし、動的木の固有の構造的収縮の内部に封入されることを、定理証明支援系 Lean 4（Mathlib omega タクティク）を用いて欠陥なく完全自動証明した。
本検証は、実行プロセスを省略せずに復元したとき、生成複雑度が初期境界の内部に必然的にカプセル化されることを示している。
序論
数論および計算機科学における長年の懸案であるコラッツ予想（\(3x+1\) 問題）[Lagarias 1985] に対し、我々は一連の研究を通じて構造的解明を進めてきた。
多次元無限木のトポロジー構造の検証 [Hyama 2026a]：1次元、2次元、3次元空間におけるコラッツ型無限木のトポロジーについて、強正規化の観点から定理証明支援系 Lean 4 [de Moura 2021] を用いた検証を実施し、根の一位性・非循環性・全域性を形式的に確立した。
動的フレーゲ公理による完全形式化 [Hyama 2026b]：コラッツ無限木に特化し、動的フレーゲ公理（Dynamic Fregean Semantics / DFS）の立場から強正規化プロセスの型論的妥当性を Lean 4 [de Moura 2021] コードとして完全検証した。
本研究の目的は、初期予想 [Hyama 2025] に回帰し、多次元無限木構造における任意の自然数 \(N\) の生成複雑度（木における深さ・世代数 \(K\)）に対する絶対上限を厳密に確定させることにある。
ここで、次元指標 \(k \in \mathbb{N}\) を伴う生成子 \(2^k N + 1\) は「多次元フレームワーク」を構築する。1次元（\(\text{mod } 2\)）、2次元（\(\text{mod } 2/4\)）、3次元（\(\text{mod } 4\)）と次元が上がるにつれて幾何学的解像度が拡張され、\(3x+1\) 演算の代数構造は3次元（Modulo 4）において完全に閉じ、完結する。本稿では、この3次元軸における世代数 \(K\) が常に出発値 \(N\) 未満（\(K < N\)）に封入されることを Lean 4 [de Moura 2021] のカーネルレベルで証明する。
【補足】「動的フレーゲ公理」とは何か？ — 数学に実プロセスと因果を取り戻す
従来の静的な古典数学における最大の欺瞞は、実プロセス（動的原因）の記述を単に省略したに過ぎない不完全な体系を、いつの間にか「数学だけは因果律を超越した特別な聖域である」と言い換えて特権化してきた点にあります。これに対し、動的フレーゲ公理はプロセスの特別扱いを排し、以下のように定義されます。
1. 数学に「動的原因」を復活させるための現実の操作・生成ルール
静的な記号の言い換え（外延的抽象）に留まるフレーゲ的ドグマの限界を打破 [Russell 1902, Wright 1983]。
実プロセスを省略して実無限の「結果の器」に逃げ込む古典数学を拒絶。
「可能無限」の上で情報が圧縮され、ノードが実際に生成される構造的因果関係（操作的意味論）として数学を捉え直す [Plotkin 1981]。
2. 「因果律は物理世界だけでなく、数学の世界でも特別扱いされない」という基礎の確立
プロセスを無視・サボる言い訳として「数学だけは特別だ」と主客をすり替える欺瞞を弾劾。
「アキレスと亀」のプロセス衝突（連続性と離散ステップの不一致）を実無限で誤魔化した「ゼノのパラドックス」に真っ向から対置。
実行プロセスの停止・破綻現象（Zeno behavior）の計算論的モデル [Alur 1994, Bournez 2001] や並行計算論の遷移系 [Milner 1989] を導入。
物理世界と同様、数学の1ステップ（ビットシフトやノード生成）そのものに厳密な動的因果性を認め、プロセスの省略を一切許さない。
3. 具体的かつ絶対的な限界（\(K < N\)）を証明可能にする基盤
原因を無視した静止述語の抽象論（神視点）から決別。
現代計算機科学における「無限ストリームの生産性」や共帰納（Coinduction）の理論 [Rutten 2000, Capretta 2005] を採用。
型論的な強正規化（Strong Normalization）の保証 [de Moura 2021] を基礎に据える。
一歩一歩確実に実行される現実のプロセス（インダクティブ型）の上で駆動。
数の組み合わせや構造の限界（\(K < N\)）を、エラーの余地のない必然的な計算現実として証明可能にする。
1. 多次元階層の代数的統一 ($2^k N + 1$) とモジュロ構造
無限木におけるノード生成子は、次元パラメータ $k \in \{0, 1, 2\}$ の上昇に伴い、以下の一般的統一形式 $2^k N + 1$ および対応する代数的モジュロとして記述される [1, 3]。
$$\text{Generator}(k, N) = 2^k N + 1$$
次元空間名称対応モジュロ生成子 (2kN+1)幾何学的・構造的意味1次元 ($k=0$)Peano 空間Modulo 2$2^0 N + 1 = \mathbf{N + 1}$単調増加軸。$K = N - 1$ となり $K < N$ の最悪ケース（限界境界）2次元 ($k=1$)Parity 空間Modulo 2/4$2^1 N + 1 = \mathbf{2N + 1}$偶奇パリティ遷移軸。2D格子上の直交隣接移動3次元 ($k=2$)Modulo 4 空間Modulo 4$2^2 N + 1 = \mathbf{4N + 1}$情報圧縮・世代カウント軸。$3x+1$ と直結する完全構造
Modulo 4 における $3x+1$ の自己同型性
奇数空間を Modulo 4 で分離した際、$4n+1$ 型奇数に対してコラッツ演算 $3x+1$ を適用すると以下の代数展開が得られる。
$$3(4n+1) + 1 = 12n + 4 = 4(3n+1)$$
この関係式は、$\div 4$ （2ビットの強制情報消去）が発動すると同時に、内部から再び同型の演算 $3n+1$ が現れることを示している。すなわち、$3x+1$ という演算そのものが Modulo 4（3次元空間）と一対一で直結しており、この空間において構造が完全自己完結する。
2. トポロジーの不変性と Lean 4 形式証明
空間の次元が上昇しても、インダクティブ型 CollatzTree の持つトポロジー構造（根の一位性・アサイクリック性）は一切不変である [1, 2]。
本章では、3次元軸（$4N+1$ 型奇数ノード）の通過回数をカウントする関数 count_k を定義し、任意のノード $t : \text{CollatzTree } n$ に対して $K < N$ が成立すること（ひゃま予想 [3]）を Lean 4 で完全自動証明する。
Verification Status
環境: Lean 4 (Mathlib.Tactic.Omega)
証明状態: Goals accomplished （エラー・未解決警告ゼロ）
Lean
import Mathlib
set_option autoImplicit false
-- -------------------------------------------------------------------------
-- 1. コラッツ無限木の密閉トポロジー空間 (CompleteCollatzTree)
-- -------------------------------------------------------------------------
namespace CompleteCollatzTree
inductive CollatzTree : Nat → Type
| root : CollatzTree 1
| even_step (n : Nat) (hn : n > 0) : CollatzTree n → CollatzTree (2 * n)
| odd_step_4n1 (n : Nat) (hn : n >= 0) : CollatzTree n → CollatzTree (4 * n + 1)
| odd_step_4n3 (n : Nat) (hn : n >= 0) : CollatzTree n → CollatzTree (4 * n + 3)
end CompleteCollatzTree
-- -------------------------------------------------------------------------
-- 2. ひゃま予想 (K < N) の形式検証 (HyamaConjecture)
-- -------------------------------------------------------------------------
namespace HyamaConjecture
open CompleteCollatzTree
/-!
### 世代数 K (4n+1 型奇数ノード通過回数) の定義
odd_step_4n1 を通過した時のみ「+1」加算する。
-/
def count_k {n : Nat} : CollatzTree n → Nat
| CollatzTree.root => 0
| CollatzTree.even_step _ _ t => count_k t -- 偶数ステップでは加算しない
| CollatzTree.odd_step_4n3 _ _ t => count_k t -- 4n+3 ステップでも加算しない
| CollatzTree.odd_step_4n1 _ _ t => 1 + count_k t -- 4n+1 ステップのみ +1 加算
/-!
### 【核心定理】ひゃま予想の証明: hyama_conjecture_lt
任意の CollatzTree n において count_k t < n を構造帰納法と omega で証明。
-/
theorem hyama_conjecture_lt {n : Nat} (t : CollatzTree n) : count_k t < n := by
induction t with
| root =>
simp [count_k]
| even_step k hk t ih =>
simp [count_k]
omega
| odd_step_4n1 k hk t ih =>
simp [count_k]
omega
| odd_step_4n3 k hk t ih =>
simp [count_k]
omega
end HyamaConjecture3. 構造的解明：$N = 27$ の絶対天井封入
従来の1次元ステップ（$3x+1$ および $x/2$）の評価においては、初期値 $N = 27$ は「111 ステップにおよび、途中で最大値 9232 まで大爆発する複雑なカオス軌道」の代表例として扱われてきた。
しかし、本研究の3次元代数空間（$2^2 N + 1$ 幾何学）においてこの軌道を捉え直すと、その評価は一変する。
図1は、評価軸適用空間N=27 における定量的評価構造的意味従来の演算ステップ1次元数直線111 ステップ（最大値 9232）一見不規則な増大と長い縮小プロセス3次元世代数 $K$3次元多次元木 ($4N+1$)$K < 27$（確実に 27 未満）絶対天井 $N$ の内部に代数的に完全封入
※27以外もこのコラッツ数列ジェネレータで確認できます。
本検証（hyama_conjecture_lt）により、$N=27$ がいかに長く複雑な軌道を描くように見えようとも、$4n+1$ 型情報圧縮エンジンを通過する回数 $K$ は 計算を始める前から $K < 27$ の範囲内に代数的に固定されている ことが確定する [1, 3]。
4. 考察：$3x+1$ (Modulo 4) の収束必然性と $7x+1$ (Modulo 8) の発散
本モデルにおける「なぜ Modulo 4 (3次元) の $3x+1$ なのか」という問いに対し、一般化コラッツ演算 $qx+1$ と高次モジュロ空間との比較分析は極めて示唆に富む。
例えば $7x+1$ 演算を Modulo 8（$8n+1$ 空間）で検討すると、
$$7(8n+1) + 1 = 56n + 8 = 8(7n+1)$$
となり、一見すると $\div 8$ （3ビット消去）の超高速圧縮が発生するように見える。しかし、$7x+1$ システム全体は無限大へ発散する。
演算体系乗数 qログ膨張率 log2q平均消去ビット数ドリフト係数全体挙動$3x+1$ (Modulo 4)$3$$\approx 1.585$ bit$2.0$ bit$-0.415 < 0$絶対収縮（$K < N$ 成立）$7x+1$ (Modulo 8)$7$$\approx 2.807$ bit$2.0$ bit$+0.807 > 0$発散（収束木を形成不能）
Modulo 8 など高次元空間で局所的な大消去（$\div 8$）が起きたとしても、乗数 $q$ による膨張スピードが打ち勝つ場合、システム全体は破綻する。
これに対し、$3x+1$ 演算は Modulo 4（$4N+1$）という最小完結空間において、ログ増大率（$1.585$）が平均消去能力（$2.0$）を下回る唯一絶妙な臨界点 に位置している。したがって、3次元多次元木においてのみ、絶対天井 $K < N$ を持つ安定した密閉不変構造が成立する。
結論（Conclusion）
本研究により、多次元無限木におけるノード生成ルールが \(2^k N + 1\) という統一形式で記述できること、および Modulo 4 に対応する3次元情報圧縮空間における代数的複雑度（世代数 \(K\)）が常に出発値 \(N\) 未満（\(K < N\)）に封入されることが Lean 4 によって形式的に検証された [1, 2, 3]。1次元での最悪ケース \(K = N - 1\) から、2次元・3次元における指数的抑え込みに至るまで、動的フレーゲ公理に基づく無限木の全域性と絶対上限バウンドが数学的欠陥なく証明された。
本成果が基礎論に示す最も本質的な結論は、抽象化そのものの否定ではない。数学における抽象化は強力な道具であるが、動的原因（実プロセス）を無意識に省略・無視した結果、目の前にある具体的な問題を解決する能力を失ってしまっては本末転倒であるということだ。プロセスを省略せず、問題を鮮やかに解決できる正しい抽象化数学（動的フレーゲ公理）の提示こそが、理論計算機科学（TCS）および形式検証分野に本研究が提供する真の基盤的知見である。
さらに、本研究における \(K < N\) の自明化は、計算論における「適切な実行プロセスの明示（型論的構成）こそが、検証の複雑性を劇的に縮小させる」という原理の美しい体現でもある。原因（プロセス）を無視した従来の枠組みでは判定不能な迷宮に見えたコラッツの挙動が、省略なき遷移系の上では、カチッとした有限の有界性（証拠）として Lean 4 (omega) に一瞬で形式検証される。この事実こそが、動的フレーゲ公理が数学の記述からカオスを排し、必然的な計算現実へと回帰させる唯一の鍵であることの動かぬ証拠である。
参考文献（References）
[Lagarias 1985] Lagarias, J. C. "The 3x+1 problem and its generalizations." The American Mathematical Monthly, 92(1), 3-23. (コラッツ予想の歴史と難度を決定づけた、数論界の絶対的サーベイ文献)
[de Moura 2021] de Moura, L., & Ullrich, S. "The Lean 4 Theorem Prover and Programming Language." Automated Reasoning (IJCAR 2021), LNCS vol 12758, Springer. (強正規化とカーネル健全性を保証する証明アシスタントの基盤)
[Hyama 2025] Hyama, S. "ひゃま予想（4次元自然数からより強いコラッツ予想へ拡張）." Hyama Natural Science Research Institute. Technical Report.
[Hyama 2026a] Hyama, S. "Lean4による自然数の正規化でコラッツ予想の解決（プレプリント）." Hyama Natural Science Research Institute. Preprint.
[Hyama 2026b] Hyama, S. "コラッツ無限木のLean4完全コード解説." Hyama Natural Science Research Institute. Preprint.
[Russell 1902] Russell, B. "Letter to Frege." (フレーゲの静的集合論の外延的崩壊を証明した Russell のパラドックスの起源)
[Wright 1983] Wright, C. Frege's Conception of Numbers as Objects. (フレーゲ算術の再評価と静的同値性の限界)
[Plotkin 1981] Plotkin, G. D. A structural approach to operational semantics. (静的な対応表ではなく、ステップ実行を数理的に定義した「構造的操作意味論」の金字塔)
[Milner 1989] Milner, R. Communication and Concurrency. (動的なプロセスと遷移システムを定式化した並行計算理論)
[Alur 1994] Alur, R., & Dill, D. L. "A theory of timed automata." / [Bournez 2001] "Zeno behavior in hybrid systems." (省略された実行プロセスが引き起こす「ゼノの振る舞い」の計算機科学的モデル)
[Rutten 2000] Rutten, J. J. "Universal coalgebra: A theory of systems." / [Capretta 2005] (無限の生成プロセスと生産性を保証する共帰納・余代数論)
[de Moura 2021] de Moura, L., & Ullrich, S. "The Lean 4 Theorem Prover and Environment." (実行プロセスを厳密に強正規化する現代の証明アシスタントの基盤)
