---
name: STEP 697 Chang Paper B interop + Mathlib integration
description: Research radar で発見した Chang (Stanford) の 5-element core I₂ を Rei に実装, 全 25 Rei atomic cores が fiber-57 経由 (2 gateway: n=121 と n=377=F₁₄), Mathlib v4.27.0 統合成功.
type: project
originSessionId: ac6697a5-aaac-4fe8-88cb-0c59c48db6cb
---
# STEP 697: Phase 1 Literature + Phase 2 Chang Interop + Mathlib

## 起点
藤本さん 2026-04-13: Research Radar で発見した Chang, Janik 等を精読し, Rei との接続 + Mathlib 統合. Chang へのコンタクトは **しない** (先方研究の邪魔防止).

## Phase 1 (Literature Study) 結果

### Chang Paper A (arxiv 2603.25753v1, 2026-03-24, 13 pages)
**"A Structural Reduction of the Collatz Conjecture to One-Bit Orbit Mixing"**

Key objects:
- Compressed Syracuse map: T(n) = (3n+1)/2^v₂(3n+1)
- Burst indicator: X_t = 1[n_t ≡ 1 (mod 4)]
- **Map Balance Theorem**: K ≥ 5 で gap starts ≡ 3 vs ≡ 7 (mod 8) 差が **正確に 1**
- **Single-bit bottleneck**: n ≡ 1 (mod 8) で bit 4 at burst-ending
- Reduction: "orbit が mod 32 の 2 residue classes を sparse subsequence でバランスよく訪れるか"

### Chang Paper B (arxiv 2603.11066v5, 2026-04-06, **168 pages**!)
**"Exploring Collatz Dynamics with Human-LLM Collaboration"**

★ Chang の v5 は **2 つの独立 reduction routes** を持つ:
1. **Weak-Mixing Hierarchy** (Hypothesis 8.3)
2. **Carry Independence Conjecture** (CIC, Conjecture 10.14)

Key structures:
- **I₂ = {7, 27, 31, 59, 63}** (mod 64, octal {07, 33, 37, 73, 77})
- **Fiber-57**: n ≡ 57 (mod 64)
- **|I_r| = 5 for all r ≥ 2** (Theorem B.11)
- **Perron root 129/1024** (depth-2 known-gap partial kernel)
- **Branches**: q ≡ 7 (mod 8) returns in 2 steps; q ≡ 3 (mod 8) gap ≥ 5
- **(3/4)^D survivor law**: |C_D| = 2·3^(D-1)
- **Class 3 (mod 8)**: critical bottleneck (survival 1/2 per visit)
- **Class 7 (mod 8)**: safe harbor
- **M-value collapse at r ≥ 3**: all 5 I_r elements → same post-absorption state
- **Channel capacity**: log₂5 = 2.322 < log₂(1024/129) = 2.989 → deficit 0.667 bits/return
- **Geometric decay** α = 645/1024 ≈ 0.630
- **Cycle impossibility verified up to period 13**

★ **Chang uses Human-LLM collaboration explicitly** ─ Section 12, methodology note. GPT + Claude 両方使用. **"Claude proved Proposition B.4"** (q ≡ 3 return gap theorem).

### Janik's syracuse-confinement (12,947 lines Lean 4 + Mathlib)

**単一 critical sorry**:
```lean
theorem nu3_linear_bound (n : ℕ) (hn : n ≥ 1) :
    ∃ K T₀, ∀ t ≥ T₀, 3 * nu3 n t ≤ t + K := sorry
```

これ 1 つが Collatz と等価. deficit δ(n,t) = 3·ν₃(n,t) - t が有界であること.

★ **Janik explicitly notes**: SlidingWindowCondition is FALSE for n=27 and 42.6% of starting values ─ つまり Rei の 25 atomic cores に対応する可能性.

**3 forces**:
1. Hensel attrition (2-adic decay 2^{-d})
2. Baker separation (Archimedean, |p·log2 − q·log3| > C/q^5)
3. Denjoy-Koksma bound (ergodic, Birkhoff sums O(t^{1/5}) via Rhin μ ≤ 6)

## Phase 2a (Chang ↔ Rei) 結果

### 決定的発見 1: 7/25 Rei atomic cores ∈ Chang I₂

| n (Rei atomic core) | mod 64 | in I₂? |
|---|---|---|
| 27 | 27 | ✓ |
| 31 | 31 | ✓ |
| 63 | 63 | ✓ |
| 71 | 7 | ✓ |
| 91 | 27 | ✓ |
| 95 | 31 | ✓ |
| 199 | 7 | ✓ |
| (其他 18) | 他 18 residues | ✗ |

**7/25 (28%) overlap** with Chang's I₂.

### 決定的発見 2: n=121 は exactly fiber-57

- **121 mod 64 = 57** (fiber-57 定義)
- **121 は Rei STEP 693 の Hasse parent of 91** (universal sink)
- Orbit: 121 → 364 → 182 → 91
- 91 mod 64 = 27 ∈ I₂
- ⟹ **fiber-57 と I₂ が orbit で直接連結**

### 決定的発見 3: 全 25 Rei atomic cores が fiber-57 経由, first-hit 2 gateway のみ

`scripts/chang-ir-depth-scan.ts` で検証:

| Gateway | q = (n-57)/64 | q mod 8 | hit by Rei 25 (個数) |
|---|---|---|---|
| **n=121** | 1 | 1 | **20** |
| **n=377** | 5 | 5 | **5** (63, 91, 95, 199, 235) |

★ **377 = 13 × 29 = F₁₄ (14th Fibonacci)** ─ 数論的特異性の可能性
★ Chang の branches (q ≡ 3/7 mod 8) は **Rei の 25 の entry を捕捉しない** (q mod 8 ∈ {1, 5})

これは **Rei が Chang の framework の "盲点"** を発見したとも解釈可能.

### 決定的発見 4: Proposition B.3, B.4 を数値検証

- **B.3** (q ≡ 7 mod 8, 2-step return): 12/12 q 値で成立
- **B.4** (q ≡ 3 mod 8, gap ≥ 5): 13/13 q 値で成立

## Phase 2d (Mathlib 統合) 結果

### 設定
- **Lean 4 toolchain**: leanprover/lean4:v4.27.0 (Janik と同じ version)
- **Mathlib**: leanprover-community, rev v4.27.0
- **Path**: `data/lean4-mathlib/`
- **Structure**: lakefile.toml + lean-toolchain + CollatzRei/{Basic, BurstGap, AtomicCores, Step696Mathlib}.lean

### Build 成功
```
CollatzRei.Basic             ✔ 793/793 jobs built (10s)
CollatzRei.Step696Mathlib    ✔ 824/824 jobs built (6.3s)
```

### Mathlib 使用
- `Mathlib.Data.Nat.Log` (bitLen 基盤)
- `Mathlib.Data.Real.Basic` (Q_STAR_REAL 定義)
- `Mathlib.Tactic.NormNum` (数値証明)
- `exact_mod_cast` で K 27 = 111 を ℝ 上に lift
- `noncomputable def` for ℝ divisions

### 実装した Mathlib 版定理
- `CollatzRei.Basic.collatzStep_27 : collatzStep 27 = 82`
- `CollatzRei.Basic.K_27 : K 27 = 111`
- `CollatzRei.Basic.bitLen_27 : bitLen 27 = 5`
- ★ `CollatzRei.Basic.n27_extremal_exact : K 27 * 100 = 444 * bitLen 27 * bitLen 27` ★
- `CollatzRei.Basic.atomic_25_size : ATOMIC_25.length = 25`
- `CollatzRei.Step696Mathlib.K_27_real : (K 27 : ℝ) = 111`
- `CollatzRei.Step696Mathlib.n91_mod_32_eq_27`
- `CollatzRei.Step696Mathlib.n121_is_fiber57`
- `CollatzRei.Step696Mathlib.Q_STAR_REAL_pos` (Q* > 0 in ℝ)

## 実装

### TS Engine (`src/axiom-os/collatz-chang-burst-gap-engine.ts`)
- `v2(n)`, `syracuseMap(n)`, `burstIndicator(n)`
- `burstGapSequence(n0, steps)`, `burstGapDecomposition(seq)`
- `isInFiber57(n)`, `isInChangI2(n)`, `fiber57Quotient(n)`
- `fiber57Branch(n)` → 'q3' | 'q7' | 'other' | 'notInFiber57'
- `fiber57ReturnTime(n0, maxSteps)`
- `verifyPropositionB3(q)`, `verifyPropositionB4(q)`
- `compareRei25ToChangI2()`: 7 overlap + 2 gateways
- `survivorCountTheoretical(D)`: |C_D| = 2·3^(D-1)
- 5 SEED_KERNEL theories T-1666〜T-1670

### Test (`test/step697-chang-burst-gap-test.ts`) — **44/44 pass**
1. Chang I₂ size 5, mod 8 ∈ {3, 7}
2. Rei 25 ∩ I₂ = 7 elements
3. n=121 exact fiber-57
4. Syracuse map S(3)=5, S(7)=11, S(27)=41
5. Burst indicator X_t
6. Proposition B.3 verified 12/12
7. Proposition B.4 verified 13/13
8. Burst sequences for 27, 31, 91
9. Fiber-57 return time table
10. (3/4)^D survivor law
11. Perron root 129/1024 channel deficit
12. 5 theories T-1666〜T-1670

### Lean 4 (Core version, `data/lean4-transfer/step697_chang_rei_connection.lean`)
- exit=0, no sorry
- 30+ theorems verified via decide/native_decide
- `chang_i2_size`, `n121_mod64`, `n377_mod64`, `syracuse_27`, etc.
- `rei_gateway_not_chang_branches`: ★ 121 と 377 の q mod 8 ∉ {3, 7} 証明 ★

### Lean 4 (Mathlib version, `data/lean4-mathlib/CollatzRei/`)
- lakefile.toml + CollatzRei.lean + CollatzRei/{Basic, Step696Mathlib, BurstGap, AtomicCores}.lean
- **Mathlib build 成功**: 793 + 824 jobs
- **Janik syracuse-confinement と interop 準備完了**

## Phase 1-2 Summary

**Phase 1 (literature)**:
- Chang 2 papers 完全抽出 (Paper A 13p, Paper B 168p)
- Janik syracuse-confinement clone + 1 critical sorry 特定
- shuanat/collatz-lean4 clone (SEDT framework, less mature)

**Phase 2a (Chang ↔ Rei)**:
- 7/25 Rei in Chang I₂
- n=121 = fiber-57
- 25 → 2 gateway (121 + 377 = F₁₄)
- Proposition B.3/B.4 verified empirically

**Phase 2d (Mathlib)**:
- lakefile v4.27.0 setup
- Mathlib build success
- STEP 696 ported to Mathlib

## 次の方向 (memo)

1. ★ **n=377 = F₁₄** の数論的意味を探索 — なぜ Fibonacci?
2. **Janik's nu3_linear_bound** に Rei の empirical verification を PR として貢献
3. **Chang's I_r at higher depths (r=3,4,5)** を verify (M-value collapse 現象確認)
4. **Walking deficit u(t) = ν₂ - log₂3·ν₃** を Mathlib で implement
5. **Baker's theorem** を Mathlib から import して Janik connection

## 連続 STEP 状況
676 → 697 = **22 連戦目**. Research Radar 発動後の最初の STEP.