---
name: ★★★ Problem 011 / STEP 875 — n=911 Universal On-Ramp Lean 4 形式化完了 (zero-sorry)
description: 2026-04-18 pm. 25 atomic cores 全てが Collatz orbit で n=911 を経由、Lean 4 で 47 theorems zero-sorry proved via native_decide. K(n) = K_to_911(n) + 41 全 cores で K_911_to_1 一定。89/89 TS cross-check.
type: project
originSessionId: 2026-04-18-problem011-n911-lean
---

# Problem 011 / STEP 875 — n=911 Universal On-Ramp Lean 4 形式化

## 一行要約

STEP 872-873 の empirical finding "25 atomic cores 全 visit n=911" を Lean 4 で 47 theorems zero-sorry (native_decide) 形式化完了 + **K_911_to_1 = 41 が 25 cores 全てで constant** の構造的発見.

## 成果物

- **Lean 4**: `data/lean4-mathlib/CollatzRei/Problem011N911OnRamp.lean` (47 theorems, 0 sorry, 0 axiom)
  - lake build 成功 (6.4s, 582 jobs)
- **TS cross-check**: `test/problem011-n911-cross-check-test.ts` (89/89 assertions pass)

## 主要定理 (全 zero-sorry)

### Main theorem
```lean
theorem all_atomic_cores_visit_911 :
    ATOMIC_CORES_25.all (fun n => visits 911 n 150) = true := by native_decide
```

### Individual (25)
```lean
theorem core_27_visits_911  : visits 911  27 150 = true := by native_decide
theorem core_31_visits_911  : visits 911  31 150 = true := by native_decide
... (25 個)
theorem core_235_visits_911 : visits 911 235 150 = true := by native_decide
```

### Reach-one + combined
```lean
theorem all_atomic_cores_reach_one :
    ATOMIC_CORES_25.all (fun n => reachesOne n 200) = true := by native_decide
theorem atomic_cores_visit_911_then_one :
    ATOMIC_CORES_25.all (fun n => visits 911 n 150 && reachesOne n 200) = true
```

### Decomposition theorems
```lean
theorem steps_27_to_911 : stepsTo 911 27 100 = 70
theorem steps_911_to_1  : stepsTo 1 911 100 = 41
theorem steps_27_to_1   : stepsTo 1 27 150 = 111
theorem k_27_decomposition_via_911 :
    stepsTo 1 27 150 = stepsTo 911 27 100 + stepsTo 1 911 100
-- STEP 696 original via 91:
theorem steps_27_to_91 : stepsTo 91 27 30 = 19
theorem steps_91_to_1  : stepsTo 1 91 100 = 92
theorem k_27_decomposition_via_91 :
    stepsTo 1 27 150 = stepsTo 91 27 30 + stepsTo 1 91 100
```

### Structural facts
```lean
theorem sibling_91_27_mod32 : 91 % 32 = 27                    -- sibling mod-32
theorem ninety_one_eq_seven_thirteen : 91 = 7 * 13             -- semiprime
theorem peak_9232_factorization : 9232 = 2^4 * 577
theorem five_seventy_seven_prime : Nat.Prime 577
theorem predecessor_3077_to_9232 : collatzStep 3077 = 9232
theorem three_thousand_seventy_seven_eq : 3077 = 17 * 181
```

## ★ 新構造発見 (cross-check) ★

25 atomic cores 全てで **K_911_to_1 = 41 が constant**:

| n | K(n) | K_to_911 | K_911→1 |
|---|------|----------|---------|
| 27 | 111 | 70 | **41** |
| 31 | 106 | 65 | **41** |
| 91 | 92 | 51 | **41** |
| 121 | 95 | 54 | **41** |
| 231 | 127 | 86 | **41** |
| 235 | 127 | 86 | **41** |
| 他 19 | 全て | 変動 | **41** ← 全一致 |

→ **K(n) = K_to_911(n) + 41**  for all n ∈ ATOMIC_CORES_25

→ n=911 は "merge point" として機能し、合流後は deterministic 41 ステップで 1 到達。この 41 は Collatz 数列「911→1」の固定長。

## 合計 Lean 4 成果 (累積)

| File | Theorems | Axioms | sorry |
|---|---|---|---|
| LayerDNestedDot | 16+ | 0 | 0 |
| Problem011N911OnRamp | **47** | 0 | 0 |
| step678_tao_2019 | 7 | 4 (honest gaps) | 0 |
| (ほか 累積) | 数百 | — | — |

## 数学的 positioning

- **empirical**: n ≤ 10⁶ で 100% (STEP 873)
- **formal**: n ∈ ATOMIC_CORES_25 (有限 25 elements) で Lean 4 zero-sorry (本 STEP 875)
- **gap**: ∀ 有界 "hardness" を持つ n (K/bl² > 1.8) の ∀n 拡張 — これは open
- ** Problem 011 candidate claim**: "n is an atomic core ⟺ K/bl² > 1.8 ∧ orbit visits 911"
  - ⟹ direction: verified n ≤ 10⁶
  - ⟸ direction: 911 visit は非-atomic orbits でも発生する (empirical 39%) — not sufficient alone
  - Stronger form: "atomic ⟺ K/bl² > 1.8 ∧ n ≤ 235 ∧ orbit visits 911" で true (25 cores enumerated)

## 次の深掘り候補

1. **Problem 011 ⟸ direction の Lean 4 化** — 911 visit の必要条件性を supplementary predicates と組む
2. **Main trunk `MainTrunk : Set ℕ`** = orbit(911-to-1) の 41-element 列を Set として定義、⊂ orbit(core) を形式化
3. **Krasikov-Lagarias 0.84 bound** の Lean 4 統合 (density の counting 下界)

## memo 末尾

47 theorems zero-sorry + 25 individual cores + 3 decomposition + 6 structural + 1 summary = Problem 011 の closure.
STEP 696 原 STEP 696 の "n=91 downstream of 27" と本 STEP の "n=911 universal on-ramp" は **階層的構造** (91 → 911 → 1) を構成. 91 visit → 911 visit → 1 descent の 3 段階 merge.