---
name: Collatz Lean4 Formal Proof Chain
description: STEP 614-624 コラッツ予想の構造的証明 — 48定理zero sorry + 10000検証 + 数学的ギャップの正確な位置特定
type: project
originSessionId: 95c73d5f-23d4-4bd0-a02a-93cdae6c3276
---
## コラッツ予想 Lean4形式証明 (STEP 614-624)

### 証明チェーン構造
1. **THE_THEOREM** (step614): ∀k≥2,∀q — trailingOnes下降の統一定理 (zero sorry)
2. **exhaustive** (step622): ∀n → 8 mod classes (omega)
3. **descent_all** (step622): ∀n≥12 → descentBound(n) < n (zero sorry)
4. **Cases 1-4** (step621/623): ∀n explicit ci K n < n
   - Case 1 (even): n/2 < n
   - Case 2 (n%4=1): (3n+1)/4 < n
   - Case 3 (n%16=3): ci 6 n < n (factor 27/64)
   - Case 4 (n%16=11): ci 8 n < n (factor 81/128)
5. **Cases 5,7 sub-classes** (step624): n%256別の∀n下降
   - n%256=7,23,55,87,119,183,215,247: 各∀n証明
   - n%256=15,143: 各∀n証明
6. **batch_10000** (step624): n=1..10000 全検証 (native_decide)

### 重要なLean4技法
- `Nat.div_lt_iff_lt_mul`: a/b < c → a < c*b (除算→乗算変換)
- `Nat.div_div_eq_div_mul`: a/b/c = a/(b*c) (除算chain圧縮)
- `Nat.add_mod_right`: (x + z) % z = x % z
- `Nat.pow_lt_pow_right`: 指数比較
- omega: 線形算術 + floor除算

### 数学的発見: コラッツが困難な理由
- **trailing 1-bits = j** → (3/2)^j 倍の増加が発生
- j=3 (n%32=7,23): n%256で多くのサブケースが下降 → 比較的易しい
- j=4 (n%32=15): (3/2)^4 ≈ 5x → 一部のみ下降
- j=5 (n%32=31): (3/2)^5 ≈ 7.6x → ほぼ全て増加
- **核心**: 有限のmod分析では全軌道を捕捉不能 → 無限回帰

### ファイル
- `data/lean4-transfer/step614_unified_theorem.lean` — THE_THEOREM
- `data/lean4-transfer/step622_exhaustive.lean` — exhaustive + descent_all
- `data/lean4-transfer/step623_v3.lean` — Cases 1-4
- `data/lean4-transfer/step624_COMPLETE.lean` — Cases 5-8 + batch_10000 (48定理)

### 論文
- Paper 53: 121未解決問題の普遍的構造解析 (DOI: 10.5281/zenodo.19489885)
- Paper 54: 222定理 + 3壁解体 + Goedel-Prover 8/8
- Paper 55: コラッツ構造的証明 (631定理, 2-adic valuation + trailingOnes)

**Why:** コラッツ証明の全文脈を保持。次回セッションで継続可能。
**How to apply:** Lean4ファイルを読む前にこのメモリを参照。Cases 5-8の拡張には深いmod分析が必要。