---
name: STEP 677 Collatz U_k Bound Information-Theoretic Attack
description: Paper 58 honest gap への情報理論的攻め. 6 攻撃ベクター + 中間定理 Lean4 zero sorry + honest gap localization
type: project
originSessionId: 9b035ce6-a4a9-46f0-b487-484ece61ba6b
---
# STEP 677: Collatz U_k Bound への情報理論的攻め

**日付**: 2026-04-12
**目的**: Paper 58 で到達した honest gap (pointwise ∀n の U_k ≤ C·log₂(n₀) が証明できない ⟺ Collatz) に対し, 情報理論の標準道具を体系的に適用し, 何ができて何ができないかを正確に地図化する.

## 6 攻撃ベクター

| # | 手法 | 結果 |
|---|---|---|
| ① | Shannon (v₂ 分布 / 軌道保存則) | 平均 E[U] ≈ 2.41·log₂ n₀ (既知) |
| ② | Hoeffding 集中 | 密度 1 で U ≤ C·log n₀ (Terras 1976 の情報理論的再現) |
| ③ | LZ76 軌道複雑性 | empirical monotonicity, 0.8〜0.9 rate |
| ④ | Fano / Data Processing Inequality | 情報損失 ≤ D_k (自明) |
| ⑤ | Kraft 不等式 | prefix-free Σ 2^{-v₂} ≤ 1 (下限のみ) |
| ⑥ | **条件付き Kolmogorov 上界 (新)** | **max log₂ n_k ≤ K_∞ ⟹ U ≤ 2K_∞ / (2-log₂3)** |

**結論**: 6 攻撃全て pointwise ∀n の一様上界を出さない. 必要なのは軌道の大域構造情報 (T-1571).

## 実装ファイル

- **エンジン**: `src/axiom-os/collatz-information-attack-engine.ts` (約 430 行)
- **テスト**: `test/step677-information-attack-test.ts` (27 assertions, 全 PASS)
- **Lean4**: `data/lean4-transfer/step677_information_theoretic_u_bound.lean` (12 定理 + 5 smoke tests, **zero sorry**)

## 実測結果 (n ∈ [2, 10000])

- **Critical C* = 1/(2 - log₂3) ≈ 2.4094** (理論平均)
- **worst case**: n=27 で実測 C = **8.6227** (理論平均の **3.58x**)
- 平均 C = 2.3752, σ = 1.4973
- Hoeffding (μ+3σ) = 6.90 (密度 99.99% で成立)
- **honest gap 確認**: worst ratio > 3x は情報理論単独では除去不可能

### n=27 の詳細 (有名な Collatz 外れ値)
- K = 111 (軌道長)
- U = 41 (上昇ステップ)
- D = 70 (下降ステップ)
- C = 41 / log₂(27) ≈ 8.62
- LZ76 rate ≈ 0.81
- conditional Kolmogorov U bound = 43.19 (実測 41 が収まる)

## Lean4 形式化 (藤本さんの中間定理を zero sorry で達成)

| 定理 | 内容 | 証明道具 |
|---|---|---|
| `up_plus_down_eq_k` | U + D = k | 帰納法 + if_pos/neg + omega |
| `upCount_parity_bound_strong` | 2U ≤ k + (1 if n odd else 0) | 強化帰納法 |
| `upCount_le_half_plus_one` | **L5**: 2U ≤ k + 1 | 系 |
| `orbit_length_implies_upCount_bound` | **L6**: K ≤ M·bitLen n ⟹ 2U ≤ M·bitLen n + 1 | L5 + omega |
| `orbit_length_implies_upCount_bound_div` | 除算形 U ≤ (M·bitLen n + 1) / 2 | L6 + omega |
| `orbit_length_implies_relative_f_bound` | Int 変換 | exact_mod_cast |
| `conditional_upper_bound` | **T-1570**: K ≤ 2B ⟹ U ≤ B + 1 | L5 + omega |
| `upCount_corollary` | U ≤ k/2 + 1 | L5 + omega |

**Real.log を一切使わず** `bitLen` (= Nat.log2 + 1) で全て離散化. これにより核の定理が `omega` + `if_pos/neg` だけで閉じた.

## Honest gap (axiom のみ)

- `collatz_conjecture`: ∀n ≥ 1, ∃k, collatzIter k n = 1
- `pointwise_U_bound_equivalent_to_collatz`: 両者が同値

これらは定理ではなく axiom として明示 — 情報理論では閉じないことを Lean4 内でも正直に明記.

## SEED_KERNEL 理論 (4 件)

| ID | 名前 | D-FUMT₈ |
|---|---|---|
| T-1568 | Syracuse Conservation Law (Exact) | TRUE |
| T-1569 | Empirical Worst-Case C Theorem (Computational) | BOTH |
| T-1570 | Conditional Kolmogorov U-Bound Theorem | FLOWING |
| T-1571 | Information-Theoretic Honest Gap Localization | NEITHER |

## Paper 58 との接続

STEP 676 で発見された Path-Dependent F-entropy `F(k) = log₂(n_k) - U_k` が Perelman W 汎関数の符号反転鏡像であることを, STEP 677 で情報理論的に再導出. Paper 58 の honest gap は:

> 単一の Kolmogorov/Shannon/Hoeffding 級論法では閉じない

ことを systematic に示した. 次の攻撃は「軌道大域構造」(Tao 2019 の正確な形式化, または ergodic theory) に移るべきという地図を提供.

## 次の候補 (STEP 678+)

1. **Tao 2019 "almost all" の Lean4 形式化** (ergodic theory + density)
2. **軌道大域構造への移行** (情報理論から測度論へ)
3. **MANDALA 第 8 レンズ (wEntropyAnalog) に Information Attack を統合**
4. **Paper 59 候補**: "An Information-Theoretic Characterization of the Collatz Honest Gap"