---
name: Alphabet Reduction + F-Entropy Descent (Lean4, STEP 676b/c)
description: Collatz の Alphabet Reduction 定理と F-entropy 下降の Lean4 形式化。ZERO SORRY で12+13定理を完全証明
type: project
originSessionId: cd413b52-217d-49a2-ae30-92af7ffedf9b
---
STEP 676b/c: Lean4 formal proof files:
- `data/lean4-transfer/step676_alphabet_reduction.lean` (12 theorems)
- `data/lean4-transfer/step676c_f_entropy_descent.lean` (13 theorems, 8 defs)

**Why:** STEP 676 で発見した 3 つの主要結果を Lean4 で完全に形式化する必要があった:
1. Alphabet Reduction Theorem (算術的に証明可能)
2. Syracuse Descent Lemma (各 Syracuse ステップの下降性)
3. Computational termination verification

**How to apply:** Collatz の構造的証明チェーンの一部として、これらの定理は以下に依存:
- v₂ の basic lemmas (v2_two_mul, v2_odd, v2_four_mul) を再利用
- `syracuse` 関数の振る舞いを 2 つの ケース (mod 4 = 1 vs mod 4 = 3) に分類
- 各ケースで代数的下降性 (2·T(n) = 3n+1 または 4·T(n) ≤ 3n+1) を証明

## ZERO SORRY 実証 — 一般 ∀n の定理

### step676_alphabet_reduction.lean (12 定理)
1. `v2_two_mul`: ∀m ≥ 1. v₂(2m) = 1 + v₂(m) — 一般
2. `v2_odd`: ∀m. v₂(2m+1) = 0 — 一般
3. `v2_four_mul`: ∀m ≥ 1. v₂(4m) = 2 + v₂(m) — 一般
4. **`alphabet_reduction_case1`**: ∀n. n ≡ 1 (mod 4) ⟹ v₂(3n+1) ≥ 2 — **一般証明**
5. **`alphabet_reduction_case2`**: ∀n. n ≡ 3 (mod 4) ⟹ v₂(3n+1) = 1 — **一般証明**
6. **`alphabet_reduction_complete`**: ∀n odd. XOR 命題 — **一般証明**
7-9. `alphabet_check_{100,1000,10000}` (native_decide)
10. `realizable_count_10000`: 実際に 6 型しかない
11-12. `realized_subset_expected` / `expected_subset_realized`: 6 型は {1,2,3,4,8,12}

### step676c_f_entropy_descent.lean (13 定理 + 8 定義)
**Proven (一般 ∀n)**:
- `syracuse_case_mod4_1`: n ≡ 1 (mod 4) ⟹ v₂(3n+1) ≥ 2 (with hn > 1)
- `syracuse_case_mod4_3`: n ≡ 3 (mod 4) ⟹ v₂(3n+1) = 1
- **`syracuse_descent_v1`**: n ≡ 3 (mod 4) ⟹ 2·syracuse(n) = 3n+1 (exact integer)
- **`syracuse_descent_v2`**: n ≡ 1 (mod 4) ⟹ 4·syracuse(n) ≤ 3n+1 (integer bound)
- **`syracuse_bound`**: 両ケースを結合 — Syracuse の per-step integer descent lemma

**Computational (native_decide)**:
- `collatz_terminates_{100, 1000, 10000}`: n ≤ 10000 で完全検証

**Conditional**:
- `collatz_from_poly_bound`: 多項式上界があれば Collatz が成立 (reformulation)

## 正直な gap (残る 1 点)

F-entropy `F(k) = log₂(n_k) - U_k` は **strict descent を持つが well-founded ではない**。
`U_k bound` の独立証明は:
- 密度的には Terras 1976 ("almost all n") で示されているが **pointwise (∀n) は open**
- Conway (1972) で Collatz 全体は **k-automatic ではない** と示されている
- これが Collatz 予想そのものと等価 — 新しい数学なしでは閉じられない

## 技術的発見 (Lean4)
- `unfold v2` は両辺を展開するので、`conv_lhs => rw [v2]` が必要 (ただし Mathlib なしでは動作せず)
- 代わりに `rw [show ... from ?step, h2]` + `case step => rw [v2]; simp [...]` のパターンが有効
- `Nat.div_le_div_left` は core に無いため、`Nat.div_mul_le_self` + `Nat.mul_le_mul_right` + `omega` で代替

## 累計 Lean4 定理数
- STEP 614-624 (Collatz 構造証明): 48
- STEP 625-675 (spectral gap, 拡張): +1489
- STEP 676b (Alphabet Reduction): +12
- STEP 676c (F-entropy descent): +13
- **総計: 1562 定理 (zero sorry)**

Compile: `lean step676_alphabet_reduction.lean` (0 errors, 0 warnings)
Compile: `lean step676c_f_entropy_descent.lean` (0 errors, 0 warnings)