本稿では,コラッツ反復を数値軌道の追跡としてではなく,\textbf{有限レンジの局所書換え過程}として解析し,有限帰着の形で整理する枠組みを与える. 交代二進表記(ABN)とコラッツ相構造表現(CPE)を用い, 加速奇数写像 $F(n)=(3n+1)/2^{v_2(3n+1)}$ の1ステップ更新が CPE列の\textbf{定数サイズ窓}に局在する書換えの合成として記述できることを示す. この局所性に基づき,鎖個数 $\mu$,鎖長総和 $H_{CS}$,節長総和 $H_K$, 全長 $B=H_{CS}+H_K$ などの構造量の増分が普遍定数による不等式で拘束されることを導く. その結果,高$\mu$領域(特に $\mu\ge4$)は有限回の反復で低$\mu$領域($\mu\le3$)へ移行する. 残る $\mu\le 3$ の範囲は有限状態空間への捕獲として扱われ, 決定的な有限検査により,既知の終端ループ(加速写像では $1$ のみ)への帰着が確認される(付録F). 本手法は密度論的結果や部分結果(例:\cite{Lagarias2010,Wirsching1998,Tao2019})とは異なり, 構造量の不等式評価と有限検査仕様の組合せに基づいて議論を組み立てる. 加えて,本稿には証明の依存関係を明確化するための Lean 補助付き証明構造を付しており, 全単射,局所書換え/局所性,構造量不等式,高 $\mu$ 降下,および低 $\mu$ 有限探索への還元インターフェースを,相対的形式化として整理している. さらに,同様の局所性思想は $3n-1$ 型写像にも適用でき, 負の整数領域に対応する挙動についても有限個のループへの収束を示す.

有限探査プログラムなどを追加ファイルとして、公開しました。ABN/CPE変換と構造量(paiza)https://paiza.io/projects/DojCBMKPHNHM10zjY5-SXw3n+1の有限探査プログラム(paiza)https://paiza.io/projects/V-6CJEy2ev6_QzhO-tLmWw3n-1の有限探査プログラム(paiza)https://paiza.io/projects/mNaosdaAJoZHuWGdQpiTkg

今回の更新では,証明構造に対する Lean 対応を追加した.具体的には,全単射(Bijection),CPE の局所キャリー/局所性,構造量不等式,高 \mu 降下,および低 \mu 有限探索への還元インターフェースを,Lean 上で相対的形式化として整理した.