---
name: ★ 2026-04-19 Andrica + Erdős-Straus + STEP 879 n=911 arith preds 並行進行
description: Collatz と並行して Andrica 予想 Mathlib 化 + Erdős-Straus 小 n Lean 4 形式化 + STEP 879 n=911 arithmetic predecessor family. 全 zero-sorry.
type: project
originSessionId: 2026-04-19-andrica-erdos-parallel
---

# 2026-04-19 Andrica + Erdős-Straus + Collatz STEP 879 並行 session

## 一行要約

Collatz 連続進化 (STEP 874-879) と並行して Andrica 予想 + Erdős-Straus 予想 Lean 4 形式化. 全 file zero-sorry, native_decide / decide / omega / structural 証明.

## 成果物

### Andrica 予想 (STEP 701 → Mathlib 化)
- `data/lean4-mathlib/CollatzRei/AndricaConjecture.lean`
- **~33 theorems zero-sorry**
- `andricaInt p q := (q-p)² < 4p + 1` (integer-squared form)
- n=1..24 consecutive prime pair 全 verified (`decide`)
- 構造的 sufficient conditions (gap ≤ 4 / 6 / √(4p)) の一般補題
- n=4 extremal case 明示的証明 (g=4, p=7, margin=12)

### Erdős-Straus 予想 (Paper 109 → Lean 4)
- `data/lean4-mathlib/CollatzRei/ErdosStraus.lean`
- **22 theorems zero-sorry**
- `erdosStraus n a b c := 4abc = n(bc + ac + ab) ∧ positives`
- n=2..20 各 explicit witness (TS brute-force 探索で確定)
- aggregate `es_small_solvable: ∀n ∈ [2,20], solvable` (interval_cases)
- 構造的 `n = 4k → (3k, 3k, 3k)` 家族 (infinite ∀k)

### STEP 879 — Collatz n=911 arithmetic predecessors
- `data/lean4-mathlib/CollatzRei/Step879ArithPredecessors.lean`
- **22 theorems zero-sorry, 0 axiom**
- `visits_via_predecessor`: step(m) = 2^k·n ⟹ orbit(m) visits n in k+1 steps
- 具体 predecessor: 607 (k=1), 2429 (k=3), 9717 (k=5)
  - 構造理由: 2^k · 911 ≡ 1 (mod 3) iff k odd (911 ≡ 2 mod 3)
- `collatzIter_add` 補題 (composition)
- 3 無限 sub-family: `2^j · 607`, `2^j · 2429`, `2^j · 9717` 全 reach 911

## 主要定理例

### Andrica
```lean
def andricaInt (p q : Nat) : Prop := (q-p)*(q-p) < 4*p + 1
theorem andrica_n4_extremal : andricaInt 7 11   -- (p=7, q=11, gap=4)
theorem andrica_small_gap: gap ≤ 4 ∧ p ≥ 5 → andricaInt p q
```

### Erdős-Straus
```lean
def erdosStraus n a b c := 0 < a ∧ 0 < b ∧ 0 < c ∧
    4*a*b*c = n*(b*c + a*c + a*b)

theorem es_small_solvable: ∀n ∈ [2,20], erdosStrausSolvable n
theorem es_four_k (k ≥ 1): erdosStraus (4k) (3k) (3k) (3k)
```

### STEP 879
```lean
theorem visits_via_predecessor (m n k) (h: step m = 2^k * n) :
    collatzIter (k + 1) m = n

-- 3 arithmetic predecessors
theorem orbit_607_visits_911  : collatzIter 2 607  = 911
theorem orbit_2429_visits_911 : collatzIter 4 2429 = 911
theorem orbit_9717_visits_911 : collatzIter 6 9717 = 911

-- Extended infinite families (∀j)
theorem two_pow_times_607_visits_911 (j) :
    collatzIter (j + 2) (2^j * 607) = 911
```

## 合計 Lean 4 成果 (累積, 2026-04-18→19)

| STEP / File | Theorems | Status |
|---|---|---|
| 874 LayerDNestedDot | 16+ | zero-sorry |
| 875 Problem011N911OnRamp | 47 | zero-sorry |
| 876 Tier2ResidualBound | 5 | zero-sorry |
| 877 KrasikovLagarias | 10 | 4 axioms + zero-sorry |
| 877b ClassicalDensityLadder | 11 | 6 axioms + zero-sorry |
| 878 Step878N911Subclass | 12 | zero-sorry |
| 879 Step879ArithPredecessors | 22 | zero-sorry |
| Andrica (new) | 33 | zero-sorry |
| ErdosStraus (new) | 22 | zero-sorry |
| **累積** | **178+ theorems** | **all zero-sorry** |

## 構造的発見 (STEP 879)

- **n=911 への arithmetic predecessor は k odd でのみ存在** (911 mod 3 = 2 + 2^k mod 3 パリティ)
- Collatz inverse tree は (i) powers-of-2 全て と (ii) k odd の arithmetic predecessor の混合
- 無限 family: 3 predecessor × ℕ j で 3 × ℕ = ℵ₀ orbit 911 経由

## 次の候補

- Paper 113 (Andrica or Erdős-Straus Lean 4) draft
- STEP 880: n=911 predecessor tree のさらなる拡張 (k=7, 9, ... の確認)
- Erdős discrepancy (Paper 82 関連) の Lean 4 化
- Erdős #414/#409 iteration probe の Lean 4 化