---
name: project-collatz-paper-feasibility-next-session-2026-06-16
description: Collatz × Lean 4 axiom-free coinductive paper 制作 next session 引き継ぎ — Q2 Installment 2A の StreamExitLayerBridge.lean (11 theorem axiom-free + 完全 zero-axiom 1 件) + PW emergence axiom-free を core contribution として paper 化 candidate
metadata: 
  node_type: memory
  type: project
  originSessionId: 725f5113-4019-47c7-995d-a18c67907a9d
---

# Collatz paper feasibility — next session 引き継ぎ (2026-06-16)

## ★★★ SUPERSEDED 2026-06-16 dusk — Phase 1 audit completed in same thread ★★★

**事態**: 本 file 想定の Phase 1 prior art audit (半日想定) を、 chat-Claude が **同 session thread 内で完遂**。 結果は両 major claim killed:

- **Kim 2008** "Coinductive properties of Lipschitz functions on streams" が 2-adic Collatz = final bit-stream coalgebra を **既に証明**
- **Coq coalgebras contrib (2008-2009) + Niqui "Coalgebraic Reasoning in Coq"** で stream coalgebra 形式化インフラ **成熟済**
- → claim #3 (νF Stream' coalgebraic bridge 新規発見) + 「新規余帰納的 methodology」 **両方死亡**

**残るのは小さな擁護可能 claim のみ**: 「(Kim 既知 coalgebraic 視点下の) exit-layer Collatz convergence を初の axiom-free Lean4 形式化 + zero-axiom witness 限定記録」 = CPP/ITP short note candidate、 major result でない。

**Net publish 確率訂正**: ~56% → **~10-20% (a' 小 note path) / 0% (c stop criterion)**。 chat-Claude + Rei lean (c)。

**残る唯一 load-bearing (藤本さんのみ可能)**: Pattern 5 自己 audit (Janik 9000 行 + STEP 1176-1179 と本 Q2 Installment 2A の差分確認、 言語層 reformulation のみ or mathematical content 重複か)。

**詳細**: [[project-collatz-paper-audit-kim-2008-prior-art-killing]] (新規 memory) 参照。 三方針 reframe + Perelman 設計図 + コアルゲブラ articulation + 他研究者 「結果素材 ≠ 手法乗換」 規律 は [[project-three-track-reframe-perelman-coalgebra-post-audit-2026-06-16]] 参照。 「超える」 看板 siren 家族 は [[feedback-super-naming-siren-family-pattern]] 参照。 行数比較罠 は [[feedback-line-count-size-vs-kind-distinction]] 参照。

**Phase 2-4 (起草 / chat-Claude cross-check / publish)** は Pattern 5 自己 audit (a' open) 通過後に初めて re-evaluate。 デフォルトは (c) stop criterion + memory 永続化のみ。

以下 (旧 mission section) は record として保持するが、 **Phase 1 確率前提が 70% pass → 0% に変わった** 事実を反映して読むこと。

---

## 1. 次 session 開始時 mission (★ 旧記述 — SUPERSEDED 参照)

**藤本さん explicit instruction (2026-06-16, 本 session 終盤)**:
> 「次回は論文制作からお願い致します」

→ 次 session の **core mission** = Collatz × Lean 4 paper 制作 (起草 / audit / publish 判断)。

## 2. Paper candidate core contribution

### 2.1 Mathematical content (audit 済、 axiom-free verified)

**Primary**: `data/lean4-mathlib/CollatzRei/StreamExitLayerBridge.lean` (Q2 Installment 2A, commit `66e22240`)
- **11 theorem 全 axiom-free zero-sorry**
- ★ `head_collatzOrbit` 完全 zero-axiom (`does not depend on any axioms`)
- ★ 9 件 `[propext, Quot.sound]` のみ (Classical.choice 不要 = STEP 1220 Lawvere axiom base より strong)
- ★★ `collatzOrbit_one_isCoalgebraicFixedPoint` — STEP 1223 νF Stream' `IsCoalgebraicFixedPoint` への explicit 接続
- ★★★ `collatzOrbit_exitM_eventuallyConst` — ExitLayer (STEP 1176 m_p = (4^p−1)/3) の **coinductive reformulation** = 「orbit が finite prefix 後 const 1 と等しい」

**Secondary** (paper 拡張 candidate): `PageWoottersSkeleton.lean` (commit `43b89751`)
- PW emergence theorem **sorry → axiom-free zero-sorry** (本日 2026-06-16 dusk 達成)
- `pageWootters_emergence_of_constraint` + `pageWootters_emergence_for_any_H_S` 両方 axiom-free
- IsTimelessConstraint = concrete discrete formula (opaque から脱却)
- 但し scope mismatch risk (Collatz と PW を一 paper にまとめると broader paper になる)

### 2.2 Paper-worthy claims (load-bearing, 主張可能)

1. **「Lean 4 axiom-free coinductive characterization of exit-layer Collatz convergence」**
2. **完全 zero-axiom theorem** (`head_collatzOrbit`) = STEP 1220 Lawvere の axiom base よりも更に minimal
3. **νF Stream' coalgebraic fixed point** ↔ Collatz orbit の **formal bridge** (STEP 1223 NuFStreamSelfLoop との接続)
4. ExitLayer (STEP 1176 algebraic μF) との **dual** (inductive μF vs coinductive νF)
5. Mathlib v4.27.0 `Stream'` API 上の minimum-axiom-base record

### 2.3 ★ Paper NG claims (overclaim trap、 起草時 honest filter で除去)

- ❌ 「Collatz 解決」 / 「Cases 5-8 wall 突破」
- ❌ 「Tao 2019 を超える」
- ❌ 「Janik 2026 6 critical sorries の解消」
- ❌ 「世界初」 (要 prior art audit、 [[feedback-world-uniqueness-claim-controllable]])
- ❌ 「新 attack vector」 (Q2 survey で ~0% 予測通り、 観察的 reformulation のみ)

## 3. 起草前 必須 audit (multi-day, [[feedback-no-rush-publication]])

### 3.1 Prior art WebSearch (推定半日〜1 日)

確認項目:
- **Lean 4** で Collatz coinductive formalization の既存例?
- **Coq / Isabelle / Agda** での同 approach 既存?
- **νF Stream' (final coalgebra)** で Collatz orbit characterization 既存?
- **「completely zero-axiom Collatz theorem」** prior art 例?
- Janik 2026 12,947 行 Lean 4 が我々の approach と重複していないか cross-check
- arXiv + Google Scholar + leanprover-community Zulip search

### 3.2 Pattern 5 自己 audit ([[feedback-chat-claude-hallucination-warning]] Antipattern 防止)

- STEP 1176 ExitLayer 既 axiom-free との差分 = **言語層 reformulation のみ** (algebraic → coinductive)
- 新 mathematical content は **無し** (既結果の言語変換)
- → Paper 主張は **「Lean 4 formalization methodology contribution」** に絞る
- Paper 132 系 (Lean 4 residual sorry roadmap) と同 framing style

### 3.3 chat-Claude cross-check (三者共著 model, OUKC charter v1.0)

- 独立 instance で 「coinductive Collatz formalization paper」 framing が overclaim でないか verify
- chat-Claude が独立に prior art check (Pattern 1 hallucination 警戒)
- 我々の paper claim の structural homomorphism evaluation

### 3.4 三者共著協議 (藤本さん + Rei + Claude Opus 4.7)

- Paper title 案: 「**Coinductive νF-Stream' Formalization of Exit-Layer Collatz Convergence with Completely Zero-Axiom Witness (Lean 4)**」 (仮)
- Scope: methodology contribution (新 math でない)
- Honest scope footer 5 項目以上 (Cases 5-8 wall 不変 / Tao 2019 を超えない / Janik 2026 と独立 / 「世界初」 不使用 / 既存 ExitLayer reformulation)
- DOI 取得 → Zenodo + 11 platform publish

## 4. 次 session 推奨進行 (4 phase)

### Phase 1: Prior art audit (半日〜1 日)
1. WebSearch 4-5 query (Lean 4 Collatz + coinductive Collatz + νF Stream' Collatz + Janik 2026 audit)
2. WebFetch で specific candidates 詳細 verify
3. 結果を `papers/collatz-coinductive-prior-art-audit.md` に永続化
4. Decision: 既存あり → paper 化見送り (memory record のみ) / 既存無し → Phase 2 へ

### Phase 2: Paper draft 起草 (1-2 日)
- Paper 132 系 methodology paper template に倣う
- Title + Abstract + Introduction (~prior art audit 結果準拠)
- Section 2: Stream'-based discrete Collatz orbit + halt variant
- Section 3: 11 axiom-free theorems + 完全 zero-axiom 1 件 detail
- Section 4: ExitLayer (STEP 1176) との dual (μF vs νF)
- Section 5: STEP 1223 NuFStreamSelfLoop との bridge
- Section 6: Honest scope (Cases 5-8 不変 / Tao 2019 / Janik 2026)
- Section 7: Limitations + future work
- Bibliography (Mathlib + Janik + Tao + Conway + Lagarias + etc.)

### Phase 3: chat-Claude cross-check (半日)
- 独立 instance で paper draft review
- Pattern 1/2/5 全件 audit
- Overclaim detection
- Honest scope sufficiency check

### Phase 4: Publish 判断 + execute (1 日)
- 三者協議で final approval
- Zenodo DOI 取得
- 11 platform publish (Paper 145/150/163/164 同様 standard)
- Harvard Dataverse: opt-in only per [[feedback-harvard-dataverse-opt-in]]

## 5. 関連 memory + files

### 5.1 Memory files (本 session 関連)
- [[project-session-2026-06-16-full-summary]] — 本日 全 commit summary (13 commit + cleanup)
- [[project-paper-145-v05-corrigendum-tang-nano-2026-05-09]] — corrigendum 先例 (publish 後の honest correction 永続原則)
- [[feedback-no-rush-publication]] — 急がず ゆっくり
- [[feedback-evaluation-symmetry-principle]] — inflate せず deflate せず
- [[feedback-world-uniqueness-claim-controllable]] — 「世界初」 不使用 controllable framing
- [[feedback-chat-claude-hallucination-warning]] — Pattern 1-6 + Antipattern 過度 reject 警戒

### 5.2 Lean 4 files (paper core)
- `data/lean4-mathlib/CollatzRei/StreamExitLayerBridge.lean` (Q2 Installment 2A) ← **paper primary content**
- `data/lean4-mathlib/CollatzRei/NuFStreamSelfLoop.lean` (STEP 1223) ← coalgebraic FP infra
- `data/lean4-mathlib/CollatzRei/ExitLayer.lean` (STEP 1176) ← μF algebraic version (dual)
- `data/lean4-mathlib/CollatzRei/Basic.lean` ← collatzStep 定義
- `data/lean4-mathlib/CollatzRei/LawvereFixedPointExperiment.lean` (STEP 1220) ← related axiom-base comparison

### 5.3 Markdown documents (本 session)
- `papers/collatz-rei-toolkit-survey-2026-06-16.md` (Q2 Installment 1 honest survey) ← **paper の base + stop criterion record**
- `papers/super-transcendence-roadmap.md` (STEP 1224) ← 全体 roadmap context
- `papers/port-feasibility-audit.md` (STEP 1224) ← chat-Claude critique response model

## 6. Honest expectations (load-bearing)

### Paper 起草 確率
- Phase 1 audit pass 確率: ~70% (prior art audit で 「我々の specific approach は無い」 と判明)
- Phase 1 fail 確率: ~30% (既存に completely zero-axiom Collatz Lean 4 が見つかる)
- Paper publish 達成確率 (Phase 1 pass 前提): ~80% (起草 + 三者協議 + publish standard process 通過)
- ★ **Net 確率**: paper publish ~56% (70% × 80%)

### Paper 化された場合の expected impact
- Mathlib contribution candidate (Mathlib Collatz section に integration 可能性)
- Paper 132 系 methodology paper として 11 platform standard publish
- DOI 取得 + Zenodo permanent record
- 「世界初」 不使用、 「Lean 4 axiom-base methodology contribution」 として position

### Paper 化見送り判断の場合
- Memory に永続化 (本 file が次 session の判断 input)
- Q2 stop criterion 適用 (Q2 Installment 1 survey で 「Candidate A + B で何も新規無ければ stop」)
- 別 direction pivot (PW emergence 完全形式化 / harfe port 完成 / Foundation Gödel port / etc.)

## 7. 永続原則 適用

- [[feedback-no-rush-publication]] — 急がず ゆっくり、 Phase 1 audit 必須
- [[feedback-evaluation-symmetry-principle]] — inflate せず deflate せず、 11 theorem + 完全 zero-axiom 1 件 を honest claim
- [[feedback-world-uniqueness-claim-controllable]] — 「世界初」 不使用、 「我々の観測範囲では」 framing
- [[feedback-chat-claude-hallucination-warning]] Antipattern 「過度の reject 警戒」 防止 — paper-worthy candidate を「無理」 と deflate せず、 audit 結果で判断
- [[project-paper-145-v05-corrigendum-tang-nano-2026-05-09]] — publish 後 corrigendum 不可避前提で起草時 5 重 verify

## 8. 一言 summary

**「Q2 Installment 2A の StreamExitLayerBridge.lean (11 axiom-free + 完全 zero-axiom 1 件) は paper-worthy candidate。 次 session で Prior art audit → Phase 2-4 順次。 起草見送り判断も valid (Q2 stop criterion 適用)。 急がず ゆっくり、 audit 結果次第。」**