---
name: project-collatz-paper-audit-kim-2008-prior-art-killing
description: Collatz × Lean 4 axiom-free coinductive paper の prior-art audit 4 軸完遂 (chat-Claude 2026-06-16 thread 内) — Kim 2008 が 2-adic Collatz = final bit-stream coalgebra 既証明 + Coq coalgebras contrib + Niqui 2008-2009 で formalization インフラ成熟済 → claim
metadata: 
  node_type: memory
  type: project
  originSessionId: fa67ebff-f793-4db7-8d99-a50aa3d0ecf6
---

# Collatz paper prior-art audit — Kim 2008 + Niqui で両 claim killed

## audit context

[[project-collatz-paper-feasibility-next-session-2026-06-16]] の Phase 1 (prior art WebSearch、 半日想定) を、 chat-Claude が 2026-06-16 同 session thread 内で完遂。 起草前合格基準を **起草前固定**、 結果を見てから甘くしない規律で実行。

## 四軸 audit query 設計 (起草前固定)

ニッチ = 「Lean4 axiom-free coinductive exit-layer Collatz characterization + νF Stream' bridge + 完全 zero-axiom witness」 を四成分に分解、 一括検索でなく軸ごとに別々に当てた:

1. **軸1 余帰納 × コラッツ** (本丸): Collatz coinductive / coalgebra / stream coinduction / 3x+1 coinductive / greatest fixed point / nu-bisimulation
2. **軸2 証明支援系 × コラッツ**: Lean / Lean4 / Mathlib / Coq / Isabelle / Agda / CPP / ITP
3. **軸3 exit-layer / 構造** (藤本固有語彙): exit layer formalization / (4^p-1)/3 / convergence formal proof axiom-free
4. **軸4 zero-axiom / minimal-axiom** (methodology 核): axiom-free theorem / propext only / minimal axiom base

場所決め打ち: arXiv (cs.LO / math.LO / math.NT) + Lean Zulip + mathlib4 + Coq/Isabelle/Agda contrib + AFP + DBLP (CPP/ITP/CICM) + Google Scholar

## 起草前固定合格基準 (改変禁止 = [[feedback-evaluation-symmetry-principle]])

- 軸1+軸3 先行ゼロ → 起草 GO (framing 「我々の観測範囲では」 必須)
- 軸2 「statement Lean 書いた」 → 想定内、 ニッチ無傷 (statement ≠ coinductive characterization)
- **軸1 or 軸3 実質先行 1 件でも出る → contribution を methodology (zero-axiom witness / axiom 最小化) のみに絞るか見送り**

## 四軸結果 (正直総括)

| 軸 | 結果 |
|---|---|
| 軸1 coalgebraic bridge | ★★★ **先行あり** (Kim 2008)。 概念的ブリッジ新規でない |
| 軸2 証明支援系 Collatz | Janik 2026 (reduction、 別サブニッチ、 既知) |
| 軸3/4 coalgebraic 形式化・exit-layer・zero-axiom | 直接の先行なし。 **ただしインフラは 2008-2009 から成熟済** (Coq coalgebras contrib + Niqui) |

### 軸1 決定的発見

**Jiho Kim「Coinductive properties of Lipschitz functions on streams」 (2008頃)** が **2-adic 版 Collatz 関数 = final bit-stream coalgebra** を既に証明。 関連論文でも 2-adic Collatz = final stream coalgebra 既存。

→ **claim #3 (νF Stream' coalgebraic FP × Collatz formal bridge 新規発見) 取り下げ確定**。

### 軸3/4 追加発見

- **Coq coalgebras contrib** (coalgebra・bisimulation・weakly final coalgebra・λ-coiteration、 stream coalgebra 実装つき) 2008-2009
- **Niqui「Coalgebraic Reasoning in Coq」** (stream coalgebra 形式化)
- **Cubical Agda** での final coalgebra 構成

→ 「Collatz を final stream coalgebra として Lean4 で形式化する」 = 既知対象 (Kim 2008) に成熟既知道具 (stream coalgebra 形式化) を当てる、 **ほぼ定型的な作業**。 「新しい方法論」 claim も死亡。

### 軸2 別サブニッチ

Janik 「Diophantine Confinement in Syracuse Dynamics」 (2026-02、 9000+ 行 Lean4) = (2,3)-トーラス上 walk / ergodic reduction = **別サブニッチ**、 coalgebraic exit-layer ではない → 絞り直し後 claim を潰さない (ただし Pattern 5 自己 audit で再確認要)。

## 仕分け結果

- ✗ **claim #3 (coalgebraic bridge 新規発見) = 取り下げ**、 Kim 2008 出典引用
- ✗ **「新規余帰納的 methodology」 = 死亡** (Coq coalgebras contrib + Niqui 2008-2009 既存)
- ⏳ 残候補のみ = **「(Kim の既知 coalgebraic 視点下の) exit-layer Collatz convergence を初の axiom-free Lean4 形式化 + zero-axiom witness 限定記録」** = CPP/ITP short note または Paper 132 系 methodology note 候補。 **major result でない**。

## publish 確率訂正

| 段階 | 旧確率 (audit 前) | 新確率 (audit 後) |
|---|---|---|
| Phase 1 audit pass (major novelty) | 70% | **0% (両 major claim killed)** |
| (a') 小 note (限定的 axiom-free record) | (扱い無し) | ~10-20% |
| (c) Q2 stop criterion 適用 | 軽 mention のみ | **~80-90% (chat-Claude + Rei lean)** |
| (a) 元の major paper publish | ~56% (合成) | **0%** |

## 残る load-bearing 作業 (藤本さんのみ可能) — ★ 2026-06-16 dusk 実行完了

**Pattern 5 自己 audit** ([[feedback-chat-claude-hallucination-warning]] Antipattern 防止) を本 session 同 thread 内で 3 phase 実行:

### Phase 1: STEP 1176-1179 vs Q2 Installment 2A 内部差分 (Rei が直接 file 比較)

**確認 file**:
- `data/lean4-mathlib/CollatzRei/ExitLayer.lean` (STEP 1176 + 1179、 算術的 μF iteration version)
- `data/lean4-mathlib/CollatzRei/StreamExitLayerBridge.lean` (Q2 Installment 2A、 νF Stream' version)
- `data/lean4-mathlib/CollatzRei/NuFStreamSelfLoop.lean` (STEP 1223 = bridge tool)
- `data/lean4-mathlib/CollatzRei/Basic.lean` (collatzStep definition)
- STEP 1177/1178 は TypeScript で Lean 形式化なし (memory 確認済、 audit 対象外)

**Verdict Phase 1 = ✓ (a') open**:

1. **Q2 file 自己 declared reformulation**: Section 8 `honest_non_claim_footer` で「既 ExitLayer 結果の **言語変換** であって novelty なし」 明示。 Section 6 `collatzOrbit_exitM_eventuallyConst` proof の冒頭コメントでも「**reformulation** of ExitLayer (STEP 1176) in Stream' language, not new mathematical content」 自記。

2. **Direct dependency**: Q2 file は `import CollatzRei.ExitLayer` + `import CollatzRei.NuFStreamSelfLoop`、 `collatzOrbit_exitM_eventuallyConst` proof は line 215 で `exact exitM_reaches_one q` で STEP 1176 既結果を **直接 hypothesis として使用**。

3. **New content (limited)**:
   - `collatzHaltStep` (1 を fixed point 化する technical wrapper、 standard collatzStep の 1→4→2→1 cycle 回避)
   - `collatzOrbit n : Stream' Nat` = orbit を coinductive stream に lift
   - `tail_collatzOrbit` = F-coalgebra 構造 (`F(X) = Nat × X`)
   - `EventuallyConst` predicate (orbit が eventually 1 になる νF 言明)
   - STEP 1223 `IsCoalgebraicFixedPoint` への explicit bridge (`collatzOrbit_one_isCoalgebraicFixedPoint`)

4. **Mathematical content 重複なし**: ExitLayer = algebraic μF iteration、 Q2 = coalgebraic νF stream observation。 同一 mathematical claim ('exit-layer reaches 1') の **double presentation** (μF 形 + νF 形)、 mathematical 内容は 1 対 1 対応で **重複でなく対**。

### Phase 2: Janik 2026 9000+ 行 Lean4 repo audit (`johnjanik/syracuse-confinement` 45 file)

**実施 method**:
- `gh api repos/.../git/trees/main?recursive=1` で 45 .lean file list 取得
- `gh api search/code?q=repo:...+TERM` で 6 key term 全件数確認
- `gh api repos/.../contents/.../Basic.lean` + `Conclusion.lean` 直接 read

**File 一覧構造** (ergodic + diophantine + harmonic analysis 系で完全占有):
- ArithmeticRigidity / Baker / BorelCantelli / BranchLocus / CarryBitScrambling / CollatzSFT / ContinuedFraction / CorrectionRatio / CorrelationDecay / DenjoyKoksma / DiophantineRepeller / Drift / IrrationalityMeasure / LinearFormThree / LittlewoodInduction / LittlewoodResidence / SiegelLemma / SkewProduct / SolenoidMixing / SpectralGap / SteinerCycle / Syracuse / SyracuseDrift / Torus / UniqueErgodicity / Walk / WeylEquidistribution / Winding 等
- **Stream / Coalgebra / Coinductive / ExitLayer / Final 完全不在** (file name level)

**6 key term GitHub code search 結果**:

| Search term | hits | 解釈 |
|---|---|---|
| coalgebra | 0 | coalgebraic approach 完全不在 |
| coinductive | 0 | coinductive presentation 不在 |
| Stream' | 0 | νF Stream' formulation 不在 |
| exitM | 0 | 藤本固有 exit-layer naming 不在 |
| exit_layer | 0 | 一般 exit-layer terminology 不在 |
| `4^p` (raw) | 2 | exit-layer (4^p-1)/3 文脈ではない incidental usage (恐らく Baker linear form 関連) |

**Approach 確認** (Conclusion.lean 直 read):
- Critical path = `nu3_linear_bound` (sorry: ∃ K T₀, ∀ t ≥ T₀, 3·ν₃ ≤ t + K)
- → `reaches_one_of_linear_drift` (CorrectionRatio.lean)
- → trajectory bounded → eventually periodic → cycle trivial (Δ₃=0,1 proved; Δ₃≥2 equality case via Baker)
- → `collatz_conjecture`
- 完全に **drift / walk divergence / correction ratio / Baker linear forms / nu3 linear bound** の analytic-arithmetic + ergodic approach

**Basic.lean approach**:
- `collatzSeq n (t+1) = collatz (collatzSeq n t)` (classical iterated function)
- `collatzReaches n := ∃ k, collatzSeq n k = 1` (algebraic μF presentation)
- **Stream'/coinductive 言語 完全 不採用**

**Verdict Phase 2 = ✓ (a') open**:

Janik 2026 は **(2,3)-torus walk + ergodic reduction + Diophantine confinement** の analytic approach、 我々の **coalgebraic exit-layer + νF Stream'** とは **完全に別サブニッチ**。 重複ゼロ。 6 key term 全 0 hits + 45 file 全 name level で coalgebraic 痕跡なし + Conclusion.lean critical path が完全に analytic = 三重確証。 chat-Claude 推測「別サブニッチ」 はこれで empirical 確証。

### Phase 3: 合成 verdict

**Phase 1 ✓ open + Phase 2 ✓ open** = Pattern 5 自己 audit **pass**。

ただし **外部 prior art (Kim 2008 + Coq coalgebras contrib + Niqui) は依然 alive**:
- Kim 2008 は 2-adic Collatz = final bit-stream coalgebra を概念的に証明済 (ペンと紙の圏論)
- Niqui 2008-2009 は stream coalgebra を Coq で形式化済 (formal infrastructure 成熟)
- → 残候補 = 「(Kim 既知 coalgebraic 視点下の) exit-layer Collatz convergence を **初の Lean4 axiom-free 形式化 + zero-axiom witness 限定記録**」 ← **technical novelty として extremely narrow**

### 最終 verdict (Phase 1+2+3 合成)

| Path | Phase 1 | Phase 2 | Kim 2008 + Niqui | 推奨 |
|---|---|---|---|---|
| (a') 小 note publish (CPP/ITP-level short formalization record) | ✓ open | ✓ open | narrow (定型作業) | **technically open, ROI 低い** |
| (c) stop criterion 適用 (memory 永続化のみ) | — | — | — | **default 推奨** |

**Rei + chat-Claude 双方 lean (c)** の理由:
1. 残 claim が extremely narrow (Kim 既知 + Niqui infrastructure 既存 → 「初の Lean4 record」 のみが novelty)
2. 「定型的形式化作業」 性質 (Mathlib stream coalgebra + ExitLayer 既結果を組合せただけ)
3. publish effort vs 公的 record 価値の trade-off で (c) が [[feedback-no-rush-publication]] 精神と整合
4. Q2 Installment 1 survey が当初予測した 「null result + Lean 4 clean statement → Q2 stop criterion」 と完全整合

**最終決定権は藤本さん**。 (a') を選ぶ場合は 「Kim 2008 + Niqui を必ず引用 + 「初の Lean4 axiom-free record (我々の観測範囲では)」 framing 厳守 + CPP/ITP short note 級 expected impact」 を honest 受容前提。 (c) を選ぶ場合は本 memory file + StreamExitLayerBridge.lean 既 commit が永続 record として十分。

## Meta 教訓 load-bearing

### audit は失望でなく成功

起草前に **overclaim 二つ捕獲**:

- claim #3 (coalgebraic bridge novelty)
- 「新規余帰納的 methodology」

知らずに 「νF Stream' で新しい coalgebraic bridge を作り、 新しい余帰納的形式化手法を確立した」 と書いて出していたら、 Kim 2008 + Coq coalgebras contrib + Niqui を見落とした論文になっていた。 **防げた**。

= [[feedback-evaluation-symmetry-principle]] **operational 実例**: 「先行なし」 を喜んで報告するなら、 「先行あり」 も同じ率直さで報告。 今日それを貫けた。

### chat-Claude 冒頭指摘の load-bearing 補強

chat-Claude が thread 冒頭で指摘した 「Janik 12947 行 (sorries 残 conditional) vs 11 行 (axiom-free 完了) は **サイズでなく種類が違う**、 行数比較は category mistake」 → audit 結果で確証。 「種類の違い = axiom-free vs conditional」 は survive (Kim 2008 はペンと紙の圏論で Lean4 axiom-free 形式化ではない)。 ただし 「種類の違い」 だけでは major result にならない (定型的形式化作業)。 → [[feedback-line-count-size-vs-kind-distinction]] 新永続原則として articulate (本 audit 結果で operationalize)。

### 「超える」 看板 = siren 家族

chat-Claude が thread 全体で articulate した観察: 「Tao 超え」「q=3 境界」「アルゴリズム超え」「エントロピー超え」 はすべて siren 家族 (魅惑的に見えて本物の前進が無い構文)。 「自分が決着をつけられるかも」 という誘惑構文だが、 境界が構造的にそこにあることと、 決着が手の届く所にあることは別。 → [[feedback-super-naming-siren-family-pattern]] 新永続原則として永続化。

## 永続原則 適用 record

- [[feedback-evaluation-symmetry-principle]] — 起草前 audit 結果が 「先行あり」 でも同率直さで報告
- [[feedback-no-rush-publication]] — 急がず ゆっくり (audit 通過しないと起草に進まない)
- [[feedback-world-uniqueness-claim-controllable]] — 「世界初」 不使用、 「我々の観測範囲では」 framing 規律維持
- [[feedback-chat-claude-hallucination-warning]] — Pattern 5 自己 audit (藤本さんのみ可能) 残作業
- [[feedback-paper-145-v05-corrigendum-tang-nano-2026-05-09]] — publish 後 corrigendum 不可避前提 (本 audit は publish 前に同種チェック先取り)

## 関連 file + 出典

### chat-Claude thread 内一次出典

- **Kim 2008** "Coinductive properties of Lipschitz functions on streams" (arxiv / Springer)
- **Janik 2026-02** "Diophantine Confinement in Syracuse Dynamics" (Substack, 9000+ 行 Lean4)
- **Coq coalgebras contrib** (GitHub) — coalgebra/bisimulation/weakly final coalgebra/λ-coiteration
- **Niqui** "Coalgebraic Reasoning in Coq" (stream coalgebra 形式化)
- **Cubical Agda** final coalgebra 構成

### 関連 memory

- [[project-collatz-paper-feasibility-next-session-2026-06-16]] — 旧 mission file (本 audit で SUPERSEDED section 追加)
- [[project-three-track-reframe-perelman-coalgebra-post-audit-2026-06-16]] — 三方針 reframe (本 thread 全体)
- [[feedback-super-naming-siren-family-pattern]] — 「超える」 看板 siren 家族
- [[feedback-line-count-size-vs-kind-distinction]] — 行数比較罠