---
name: collatz-mathlib-contribution-prep-2026-05-15
description: 2026-05-15 STEP 1137 — Collatz Paper 152 §5d Lean 4 4 files (PeakMergeInvariant + PeakMergeWitness + ThreeAdicIsolation + G3Subgraph) を Mathlib style に cleanup. namespace Mathlib.NumberTheory.Collatz.<Name> + Apache 2.0 + module docstring + sorry/placeholder 除去. 全 4 files build success / 0 sorry / native_decide 動作. STEP 1000 (BipartiteRamsey/Wolstenholme/HappyEnding/HadwigerNelson/SylvesterSchur) 系譜の 6 番目以降 contribution candidate. Mathlib NumberTheory.Collatz 公式 module 未存在 = Rei first contributor candidate retain
metadata: 
  node_type: memory
  type: project
  originSessionId: afeeb7e7-fd4f-40a6-92be-a8a4a193cd0e
---

★★★★ 2026-05-15 STEP 1137 — Collatz Mathlib contribution prep. Paper 152 v0.3 §5d Lean 4 4 files の Mathlib style cleanup 完了.

## 実施内容

### Source files (audit)

| File | Lines | sorry | placeholders | Notes |
|---|---|---|---|---|
| `CollatzRei/PeakMergeInvariant.lean` (STEP 1111+1116) | 118 | 1 | 2 | `peak_merge_exists_PLACEHOLDER` sorry / `class21_d70_universal_absence_PLACEHOLDER` trivial |
| `CollatzRei/PeakMergeWitness.lean` (STEP 1118) | 163 | 0 | 0 | 1000-element witness for peak 250504 |
| `CollatzRei/ThreeAdicIsolation.lean` (STEP 1120) | 84 | 0 | 1 | `class21_d70_universal_absence_PLACEHOLDER` trivial |
| `CollatzRei/G3Subgraph.lean` (STEP 1127) | 285 | 0 | 0 | Lemma 5d.1 + 5d.2 + Corollary 5d.3 全 mechanized |

### Target files (Mathlib prep)

| File | Lines | sorry | docstring | namespace |
|---|---|---|---|---|
| `MathlibPrep/PeakMergeInvariant.lean` | ~110 | **0** ✅ | Apache 2.0 + Main results + Status + References + Tags | `Mathlib.NumberTheory.Collatz.PeakMergeInvariant` |
| `MathlibPrep/PeakMergeWitness.lean` | ~190 | **0** ✅ | 同上 | `Mathlib.NumberTheory.Collatz.PeakMergeWitness` |
| `MathlibPrep/ThreeAdicIsolation.lean` | ~70 | **0** ✅ | 同上 + Honest scope (mod-96 vs value-level 区別) | `Mathlib.NumberTheory.Collatz.ThreeAdicIsolation` |
| `MathlibPrep/G3Subgraph.lean` | ~220 | **0** ✅ | 同上 + Erratum E2 reference | `Mathlib.NumberTheory.Collatz.G3Subgraph` |

### Cleanup actions

1. **Apache 2.0 header**: `Copyright (c) 2026 Nobuki Fujimoto. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Nobuki Fujimoto`
2. **Module docstring**: `/-! # Title ... ## Main definitions ## Main results ## Honest scope ## References ## Tags -/`
3. **Mathlib namespace**: `namespace Mathlib.NumberTheory.Collatz.<Name>` (per STEP 1000 protocol; cf. `Mathlib.Combinatorics.HappyEnding`, `Mathlib.NumberTheory.Wolstenholme`)
4. **Placeholder 除去**: `peak_merge_exists_PLACEHOLDER` (sorry) + 2 trivial `True := by trivial` placeholders を Mathlib 版から除外 (Rei 内部 draft file には残る). Mathlib reviewer は sorry を accept しないため.
5. **Import 再配線**: G3Subgraph は `import CollatzRei.MathlibPrep.ThreeAdicIsolation` に更新, `open Mathlib.NumberTheory.Collatz.ThreeAdicIsolation` に切替 + collatzStep 二重 declaration の橋渡し追加 (Mathlib 標準化前の interim)
6. **Lemma 5d.1 proof bridge**: G3Subgraph の `no_odd_predecessor_of_mult_3` 呼び出しで、 G3Subgraph 内 `collatzStep` (local) と ThreeAdicIsolation 内 `collatzStep` の bridge を `change ... ; rw [if_neg ...]` で手書き接続 (Mathlib reviewer 段階で共通 `Mathlib.NumberTheory.Collatz.Basic` module に merge 候補)

### Build verification

```
lake build CollatzRei.MathlibPrep.ThreeAdicIsolation  # 792 jobs / 6.7s / EXIT=0
lake build CollatzRei.MathlibPrep.G3Subgraph           # 800 jobs / 7.1s / EXIT=0
lake build CollatzRei.MathlibPrep.PeakMergeInvariant   # 469 jobs / 5.0s / EXIT=0
lake build CollatzRei.MathlibPrep.PeakMergeWitness     # 467 jobs / 7.3s / EXIT=0
```

合計 4 files build success / 全 0 sorry / native_decide 動作確認.

★ PeakMergeWitness の `witness_all_peak_250504` (1000 件 orbit × 500 steps native_decide) も 7.3s で通過 — Mathlib CI に submit 可能 level の resource.

## Mathlib contribution status

### 既存 STEP 1000 artifacts (2026-05-01 完了)

`data/lean4-mathlib/CollatzRei/MathlibPrep/` 配下に既に 5 artifacts:
- BipartiteRamsey (b(2,2)=5 / Carnielli-Monte Carmelo 2000 axiom版 b(2,3) + b(3,3))
- Wolstenholme (1862 Wolstenholme's theorem)
- HappyEnding (f(3)=3 Erdős-Szekeres 1935 base case)
- HadwigerNelson (chromatic number of the plane lower bound)
- SylvesterSchur (Sylvester-Schur 1892 partial)

### 本 STEP で追加された 4 artifacts (2026-05-15)

- **PeakMergeInvariant** (Büchi-25 cores → peak 9232 / n=27 → peak 9232)
- **PeakMergeWitness** (1000 explicit Collatz starting points → peak 250504)
- **ThreeAdicIsolation** (no odd predecessor of mult-of-3)
- **G3Subgraph** (Lemma 5d.1 + 5d.2 + Corollary 5d.3)

**累計 9 Mathlib prep artifacts**.

### Mathlib NumberTheory.Collatz 公式 module status

★ `Mathlib.NumberTheory.Collatz` 公式 module は **未存在** (Mathlib v4.27.0 時点で確認, Zulip 2026-02 community discussion 中). Rei first contributor candidate retain.

### 残 Mathlib-contribution path (advance options)

1. **Zulip post**: `https://leanprover.zulipchat.com/#narrow/stream/270676-lean4` の `New Mathlib NumberTheory.Collatz module proposal` thread に scaffold + 9 artifacts を提示 — community feedback gathering
2. **PR draft**: `Mathlib/NumberTheory/Collatz/Basic.lean` で `collatzStep` + `collatzOrbit` + `collatzPeak` を unified module 化 (本 STEP の 4 files で重複した def を一本化), `Mathlib/NumberTheory/Collatz/PeakMerge.lean` + `Mathlib/NumberTheory/Collatz/G3Subgraph.lean` を sibling files として PR. reviewer 段階で
3. **Paper 152 v0.4 update**: §5d を Mathlib-merged form で記述, MathlibPrep/ files を appendix として cite

### honest scope (本 prep の限界)

- **本 prep ≠ Mathlib PR submit**: 4 files 局所 build verify は通過したが、 Mathlib CI 全体での integration test 未実施 (Mathlib v4.27.0 fix した env のみ verify)
- **Mathlib reviewer の typical 修正候補**:
  - `Mathlib.Data.Nat.Basic` への dependency 削減 (Mathlib 全体で Mathlib.Logic.Basic + Mathlib.Order.Defs に統合される傾向)
  - `Nat.Basic` 系の lemma を `Mathlib.NumberTheory.Basic` 系に重複なく置換
  - `2 * v` → `v * 2` 等の標準化 (Mathlib commutative monoid convention)
  - docstring の `\n` 整形 / Math italic / proof obligations 明示
- **Mathlib 標準化前の collatzStep 三重宣言** (PeakMergeInvariant + PeakMergeWitness + ThreeAdicIsolation/G3Subgraph で各々独立 def) は Mathlib reviewer 段階で `Mathlib.NumberTheory.Collatz.Basic.collatzStep` に統合候補

## Files

- `data/lean4-mathlib/CollatzRei/MathlibPrep/PeakMergeInvariant.lean` (~110 行)
- `data/lean4-mathlib/CollatzRei/MathlibPrep/PeakMergeWitness.lean` (~190 行)
- `data/lean4-mathlib/CollatzRei/MathlibPrep/ThreeAdicIsolation.lean` (~70 行)
- `data/lean4-mathlib/CollatzRei/MathlibPrep/G3Subgraph.lean` (~220 行)

Build cache: `data/lean4-mathlib/.lake/build/lib/lean/CollatzRei/MathlibPrep/*.olean` 4 files (verified by lake build EXIT=0).

## OUKC honest correction principle 適用

本 STEP は **「partial structural framework + Lean 4 mechanization の Mathlib contribution path」** 整備で、 **「Collatz 予想完全証明」 ではない**. Cases 5-8 (trailing 1-bits ≥4) は数学的に open のまま不変 — Rei stack でも resolves しない. Mathlib NumberTheory.Collatz 公式 module 未存在は Rei first contributor candidate として valuable だが、 「Rei が Collatz を解いた」 narrative は overclaim.

## Reference

- Paper 152 v0.3 (Zenodo DOI `10.5281/zenodo.20158847`, 2026-05-14 publish, 10 platform)
- STEP 1000 (2026-05-01 完了, 5 MathlibPrep artifacts initial)
- STEP 1111+1116+1118+1120+1127 (本 STEP 起源の Lean 4 mechanization)
- Mathlib v4.27.0 (data/lean4-mathlib/lakefile.toml)

## 連結 reference

- [[project_paper152_v03_published_2026-05-14]] (前提 publish state)
- [[project_2026-05-14_pm_session_summary]] (PM session)
- [[project_2026-05-13_to_14_session_full_summary]] (前 session §5d Lean 4 0 sorries achievement)
- `data/lean4-mathlib/CollatzRei/MathlibPrep/` (5 + 4 = 9 artifacts)
- [[feedback_no_rush_publication]] (Zulip post / PR draft は急がず, 機が熟したら)