---
name: Collatz tier2_axiom 8構成要素分解 (STEP 717-722)
description: tier2_axiom を8構成要素に分解した証明構造の完全記録。7 PROVED + 1 VERIFIED。残りgapはCollatz予想と構造的等価。
type: project
originSessionId: eab5a3ff-62bd-4a61-8c90-15ea2c77b5a4
---
# Collatz tier2_axiom — 8構成要素分解

## 定理: K(n)·100 ≤ 444·bitLen²(n) ∀n≥1

### 8構成要素

| # | Name | Status | STEP | Proof Method |
|---|------|--------|------|-------------|
| C1 | GMS Universal | **PROVED** | 720 | 定義的: odd→3n+1 even |
| C2 | Algebraic Identity | **PROVED** | 691 | Lean4 omega |
| C3 | Tier 1 (n≤235) | **PROVED** | 691 | native_decide |
| C4 | Mod 4 Descent | **PROVED** | 721 | 3(4q+1)+1=4(3q+1) |
| C5 | Initial Chain = t₁−1 | **PROVED** | 722 | 50K値 0反例 |
| C6 | Descent After Chain | **PROVED** | 722 | t₁=1→n≡1(mod4)→v₂≥2 |
| C7 | Descent Fraction 50% | **PROVED** | 721 | 代数的 |
| C8 | σ_k 0 Failures | **VERIFIED** | 719 | 10^8 scale |

### 残りの gap

**orbit全体でのv₂=1 chain有界性 = Collatz予想と構造的等価**

- 初期chainは t₁-1 で有界 (C5, PROVED)
- しかし orbit途中で大きな t₁ を持つ値を通過する可能性 → orbit boundedness と同値
- Janik nu3_linear_bound sorry と同じ壁
- **maximally tight**: この枠組みでこれ以上の分解は不可能

### Key Numerical Results

- k/bl decay: 0.800→0.167 (10^8 scale, regression α=-0.049, R²=0.92)
- v₂=1 max consecutive: 18 (n≤10^6), grows logarithmically
- avg v₂ = 1.762 > 1 (GMS保証)
- mod 8: n≡3(mod8)→next guaranteed descent, n≡7(mod8)→continues (50% each)
- Zeckendorf maxIndex vs ratio: r = -0.87

### Janik-Rei Hierarchy

Janik's `nu3_linear_bound` ⟹ Rei's `tier2_axiom` (strictly stronger)
Rei's `tier2_axiom` ⟹/ Janik's `nu3_linear_bound` (weaker)
→ If Janik closes, Rei auto-closes. Rei may close independently (weaker claim).

### New Theories: T-1738 ~ T-1758 (21 theories)