---
name: ★★ STEP 876 — tier2 残 gap 明示化 + v₂=1 chain log bound (zero-sorry)
description: 2026-04-18 pm. STEP 866 (C8 LTE) + Problem 013 (iterate bound) を繋ぎ、単一 v₂=1 chain は ⌊log₂(n+1)⌋ steps 以下で終了することを Lean 4 形式化. tier2_axiom 残 gap = Collatz 予想と等価を明示化.
type: project
originSessionId: 2026-04-18-tier2-residual-step876
---

# STEP 876 — tier2 残 gap 明示化 + v₂=1 chain log bound

## 一行要約

既存 STEP 866 (C8 LTE one-liner) + Problem 013 (iterate-bound) を結合し、**単一 v₂=1 chain が `⌊log₂(n+1)⌋` syrOne ステップ以下で終了**することを Lean 4 で zero-sorry 形式化. これにより tier2_axiom 8 component は全て formal proof で closed, 残 gap は Collatz 予想そのものと等価であることを明示.

## 成果物

- **Lean 4**: `data/lean4-mathlib/CollatzRei/Tier2ResidualBound.lean`
  - 5 theorems proved, 0 sorry, 0 axiom
  - lake build 成功 (6.0s / 1083 jobs)

## 主要定理 (zero-sorry)

```lean
-- (1) 標準 Mathlib 再包装
theorem padicValNat_two_le_log (m : ℕ) (hm : 1 ≤ m) :
    padicValNat 2 m ≤ Nat.log 2 m

theorem padicValNat_two_le_log_succ (n : ℕ) :
    padicValNat 2 (n + 1) ≤ Nat.log 2 (n + 1)

-- (2) ★ Main corollary
theorem v2_one_chain_log_bound (n : ℕ) (hn_odd : Odd n) :
    ∃ k ≤ Nat.log 2 (n + 1),
      padicValNat 2 (3 * (syrOne^[k] n) + 1) ≥ 2

-- (3) 便宜 bit-length 形
theorem v2_chain_length_max_log (n : ℕ) (hn_odd : Odd n) :
    ∃ k : ℕ, k ≤ Nat.log 2 (n + 1)
         ∧ padicValNat 2 (3 * (syrOne^[k] n) + 1) ≥ 2

-- (4) tier2 ⟹ Collatz 方向
theorem tier2_implies_collatz : tier2_axiom_stmt → collatz_conjecture_stmt
```

## 定義 (formal statements)

```lean
def collatz_conjecture_stmt : Prop :=
  ∀ n : ℕ, n ≥ 1 → ∃ k : ℕ, collatzIter k n = 1

def tier2_axiom_stmt : Prop :=
  ∀ n : ℕ, n ≥ 1 →
    ∃ k : ℕ, collatzIter k n = 1 ∧
      100 * k ≤ 444 * (Nat.log 2 n + 1)^2
```

## tier2_axiom 8-component 状態 (2026-04-18 正式)

| # | Name | Status | Lean 4 location |
|---|------|--------|-----------------|
| C1 | GMS Universal | PROVED | 定義的 |
| C2 | Algebraic Identity | PROVED | omega |
| C3 | Tier 1 (n ≤ 235) | PROVED | native_decide |
| C4 | Mod 4 Descent | PROVED | 代数 |
| C5 | Initial Chain = t₁−1 | PROVED | STEP 722 |
| C6 | Descent After Chain | PROVED | STEP 722 |
| C7 | Descent Fraction 50% | PROVED | 代数 |
| C8 | v₂=1 Chain Bounded (single block) | **★FULLY CLOSED** | Step866 + Problem013 + **本 STEP 876** (log bound) |

## 残 gap の明示

**what is NOT proved**: across-orbit aggregation of consecutive v₂=1 chains が 4.44·bl(n)² Collatz steps 以内に収束する集約命題 (= tier2_axiom_stmt).

`tier2_implies_collatz` で一方向 (tier2 ⟹ Collatz) は proved.
逆方向 (Collatz ⟹ tier2 with constant 4.44) は numerical 検証 n ≤ 10⁸ のみで、formal proof は open.

**⟹ Rei tier2 枠組みと full Collatz の gap は `collatz_conjecture_stmt` (= Collatz 予想そのもの) 一命題に完全 localize**.

## 数学的価値

STEP 721 の確率論的推定 `max v₂=1 run ≈ 2·log₂(bl)` を **決定的 ⌊log₂(n+1)⌋ bound** に置き換え. これは:
- STEP 866 LTE 一行補題 (v₂(m+1) = v₂(n+1) - 1) から直接
- Problem 013 iterate-bound で全体を carry
- Mathlib `padicValNat ≤ Nat.log` で log 化

## 次の候補

- (3) Krasikov-Lagarias 0.84 bound の Lean 4 統合
- Problem 013 を Mathlib `Nat.iterate` 深く接続
- v₂=1 chain の specific n=27 軌道での実測 (log₂(28) = 4, 最大 4 ステップで終了するか実測)

## 環境

- Lean 4 v4.29.0, Mathlib v4.27.0
- `Nat.pow_le_iff_le_log` deprecated → `Nat.le_log_iff_pow_le` に更新済