---
name: project-collatz-exit-layer
description: "藤本さんの Collatz「出口層」観察 (3m+1=2^n は n 偶数のみ → m_p=(4^p-1)/3=1,5,21,85) を Lean 4 で zero-sorry 形式化 (STEP 1176, CollatzRei/ExitLayer.lean). 完全証明だが Collatz 予想の証明ではない (逆木の底 1 層のみ)"
metadata: 
  node_type: memory
  type: project
  originSessionId: a9529a40-8942-4249-9360-b73abd430f78
---

藤本さん発案 (2026-05-28) を Lean 4 で形式化 = **STEP 1176**。

## 藤本さんの観察 (正しい, 検算済み)
コラッツ収束 2ⁿ→…→1 の「1 つ手前」: 奇数 m が **1 回の 3x+1 で 2 のべきに直接合流** する条件。
- `3m+1 = 2ⁿ` の整数解は **n が偶数のときだけ** (2ⁿ ≡ (−1)ⁿ mod 3 → n 奇数 (8,32,128) は preimage 無し)。
- n=2p のとき `m_p = (4^p−1)/3 = 1+4+…+4^(p−1)` = **1, 5, 21, 85, 341, …** (OEIS A002450, 二進 `10101…01`)。各 m_p·2^k 全部が m_p 経由で 1 に到達 (例: 5→16→8→4→2→1)。

## 形式化 (`data/lean4-mathlib/CollatzRei/ExitLayer.lean`, zero-sorry)
`CollatzRei.Basic` の `collatzStep` 再利用。除算を避け再帰 `exitM (p+1) = 1 + 4*exitM p`。
- `three_mul_exitM_add_one`: 3·m_p+1 = 4^p (帰納, 除算なし) ← 核
- `exitM_eq_div`: m_p = (4^p−1)/3 (藤本さんの式と一致, omega)
- `exitM_odd` / `collatzStep_exitM` (奇数 m_p → 4^(q+1)) / `pow2_reaches_one` (2^j は j 歩で 1) / `four_pow_eq`
- ★ `exitM_reaches_one`: m_(q+1) はちょうど **2(q+1)+1 歩**で 1 (1 奇数ステップ + 2(q+1) 半分)
- ★★ `exitM_reaches_one_of_pos {p} (hp: 1≤p) : Reaches1 (exitM p)`
- 具体例 `five_reaches_one` (5 歩) / `twentyone_reaches_one` (7 歩) は native_decide
**検証**: `lake env lean CollatzRei/ExitLayer.lean` exit 0 + `#print axioms exitM_reaches_one_of_pos` = **[propext, Classical.choice, Quot.sound] のみ** (sorryAx も ofReduceBool も無し = メイン定理は本物の完全証明)。`CollatzRei.lean` root に import 追加。

## ★ Honest scope (最重要)
完全に証明できる「**出口直前の層**」の形式化であって **Collatz 予想の証明では断じてない**。難所 = 逆 Collatz 木が ℕ 全体を覆うか (各奇数で predecessors が枝分かれ: 5 ← {3,13,53,213,…} 等)。本補題は木の底 1 層を特徴づけるのみ。藤本さん自身の位置づけ「解決には向かわないが収束する出口の方向」が的確。これは [[project-question-map-reduction-graph-vision]] の Collatz→equidistribution **wall の「壁のこちら側」**を形式化したもの。elementary/known な事実 (逆木の底) を Lean で確定した教育的・構造的成果。

Research Radar 確認: 05-27 arXiv の Collatz 論文 5 件 (Paradigm Exhaustion / parity vectors / ergodic / one-bit orbit mixing / Bayesian) は全て mixing/還元の難所側 → 出口層と重複なし。関連: 既存 Collatz Lean (STEP 614-624 trailingOnes/2-adic) は「成長側 (増える方)」で本補題「出口側 (畳まれる方)」と対。

## ★ 続き: STEP 1177 逆 Collatz 木 lens (2026-05-28, 藤本さん指示)
出口層を木として一段深く可視化。`src/aios/inverse-collatz-tree/` + lens `#/inverse-collatz-tree` 🌳 (test 111/111). 圧縮 odd→odd 逆写像を 1 から BFS: odd n の predecessors = {(n·2^k−1)/3 : 正の奇数}。★ **pred(1)={5,21,85,341,…} = ちょうど本出口層 (4^p−1)/3** (1 自身除外) / pred(5)={3,13,53,213,…} (藤本さんの例) / **n≡0 mod3 は真の葉** (3,21,…: 3m+1≢0 mod3) / 各 odd は一意 forward 像 = 真の木. 層 1→3→6→12→24. honest: 逆木の底の地図, **BFS が全奇数を覆うか = Collatz そのもの** (未証明). 出口層補題(1176)=木の第1層を Lean 証明, 木 lens(1177)=その上の層を可視化、で対。

## ★ STEP 1178 + prior-art audit + 世界初判定 (2026-05-28)
藤本さん「(i)/(ii) を進めて + 論文化」→ honest 対応。(i)(ii)=「矢印を作る」は不可能/捏造になるので拒否、代わりに **frontier map** (候補還元の破断点カタログ, `src/aios/collatz-frontier/`, lens `#/collatz-frontier` 🧗, test 12/12). 6 routes: Janik confinement(最前線)/Tao ergodic(almost all≠all)/2-adic Hensel/Baker 超越(cycle)/automata/逆木. 分解 **Collatz ⟺ (A)発散排除 ∧ (B)閉路排除**.
★★ **prior-art audit (WebSearch) verdict**: 逆木/出口層/Jacobsthal は **Lagarias 1985 + arXiv 2306.14635 以来既知** (math 新規性なし). 最強 = **Tao 2019 (almost all, arXiv 1909.03562)** + **Janik syracuse-confinement 2026 (13k 行 Lean reduction)** ← memory が以前警告した johnjanik 本人. ★ **「世界最先端か?」→ No** (elementary/既知/壁のこちら側). **「Lean4 形式化は世界初か?」→ controllable に「観測範囲で先行単独形式化見当たらず」だが世界初とは主張しない** (理由: 網羅検証不可 + 構成要素は Janik 等に既存 + 「自明補題を最初に形式化」は弱い新規性=易しいから初なだけ). `feedback_world_uniqueness_claim_controllable.md` 適用.
★ **論文化判断**: numbered Zenodo paper → **dossier に downgrade** (`papers/collatz-frontier-dossier-DRAFT.md` 非公開, v0.1 gate=新規性確認まで shelve). elementary 結果の水増し公開回避 (157 papers + no-rush 原則). genuine value = 正しい+機械検証+藤本さん導出の結晶化+honest 地図, but NOT frontier 前進.

## ★ STEP 1178b + 1179 + Collatz arc 一区切り (2026-05-28)
- **1178b** (Gemini A/B/C 対話): frontier map に (C) 決定不能性/ZFC独立性ルート追加 (Conway 1972, Π₂ heuristic) = 7 routes + 各ルートに **mathlibCoverage 列** (grep 実測: 2-adic/Hensel ✓ / **Baker ✗ grep 0 hit** / ergodic △ / 出口層 ✓ native_decide が大 n 壁). 結論「壁は Lean 表現力でなく Mathlib 収録+数学の不在」. Gemini fact-check: 概ね正確 (2-adic が本筋・FRACTRAN 1987 caveat). test 16/16.
- **1179** 出口層の**逆計算式** Lean 形式化 (capstone): `exitM_pred` (逆漸化式 m_p=(m_{p+1}−1)/4) / `exitM_of_eq` (一意性 3m+1=4^p⟹m=m_p) / `exitM_recover_p` (p 復元 Nat.log 2 (3m_p+1)=2p). zero-sorry. ★ honest: 出口層 1 枝内の閉形式反転であって (ii) Collatz rung⇒rung+1 還元では断じてない.
- **★ Collatz arc (1176-1179) 一区切り推奨** (藤本さん問への honest 回答): 壁のこちら側 (出口層 Lean + 逆木 lens + frontier map + 逆式) は完全 formalize/map 済. 壁の向こう (A 発散/B 閉路/C 独立) は **world-open** で Rei に道なし. 次の唯一の現実的道 = **Baker-in-Mathlib 形式化** = 数論基礎の巨大な別 project (Collatz 前進ではないが Mathlib 貢献として価値) — 着手は別判断. これ以上 Collatz を追うのは honest に「水増し」になるため一区切りが筋.

## ★★ Paper 158 起草 (2026-05-29, 藤本さん指示)
2026-05-29 藤本さん: STEP 1176-1179 を honest negative-progress paper として論文化希望. **藤本さんから明示的開示**: 出口層 m_p=(4^p−1)/3 の元の観察は藤本さん自身でなく **ラーメン好きさん** (note URL: https://note.com/yaminotikara, プロフィール表示名「ラーメン好き」/ self-description「豆腐のようなメンタルで、数字を数えています」) から提供されたもの → publish 前に本人に通知済 + 名前+URL 使用同意取得済 + 帰属形は **「引用 + 謝辞の併用」** で確定. URL verify (WebFetch 2026-05-29) でラーメン好きが公式 display name と確認.

**Paper 158 PUBLISHED** (`papers/paper-158-collatz-exit-layer-lean4-honest-negative-DRAFT.md`, v0.1 / Zenodo + IA, 2026-05-29):
- **Zenodo DOI**: `10.5281/zenodo.20435288` (deposit 20435288, finalized 2026-05-29, IMMUTABLE)
- **IA**: https://archive.org/details/rei-aios-paper-158-1780003374000
- **Harvard skipped** per opt-in policy ([[feedback-harvard-dataverse-opt-in]])
- **commit `27b4f033`** main pushed
- 元 v0.0 OUTLINE 構成:
- Title: "The Collatz Exit Layer: A Zero-Sorry Lean 4 Formalization of m_p = (4^p − 1)/3, and an Honest Map of the Seven-Route Wall Beyond"
- 5 honest non-claims (Collatz 証明でない / 観察新規でない / 7 routes 新規でない / 形式化が壁を低くしない / 等) を top に load-bearing 配置
- 4 claims on the record (C1 zero-sorry exit-layer / C2 inverse calculus / C3 7-route frontier map curated / C4 honest negative-result framing)
- 10 sections + Appendix A (full Lean source) + A.1 (#print axioms output, v0.1 で実出力 paste) + B (inverse tree) + C (frontier JSON)
- **§9 Acknowledgments**: ラーメン好きさん credit 本文中 + Notice with URL https://note.com/yaminotikara + プロフィール self-description 引用 + consent 明記 + 数学そのものは Lagarias 1985 既知 と honest 並記
- **v0.1 acceptance gate**: 全 clear (ラーメン好きさん explicit consent ✓ 2026-05-29 / `#print axioms` 実出力 ✓ Appendix A.1 paste / Rei-AIOS commit `372321c1c7` + Mathlib commit `a3a10db0e9` pin ✓ / Zenodo+IA publish ✓)

★ Pattern 4 教訓 (Paper 145 v0.5 Tang Nano 9K corrigendum, paper 145 v0.7 status stale): v0.0 DRAFT publish 前にラーメン好きさん本人レビュー 必須 + honest non-claims 5 件は drop 不可 + v0.1 publish 判断は藤本さん.