---
name: Next-session Collatz continuation (2026-04-17+)
description: 次回セッションで進める Collatz 継続タスク A1-A6. 藤本さん合意済 (2026-04-16 session 終盤). 完全 exhaust ではないので継続を明示希望.
type: project
originSessionId: a08149e8-f1de-4fbc-b4eb-fb2cec8fad21
---
# 次回 Collatz 継続タスク

**藤本さん指示 (2026-04-16)**: Collatz は structural decomposition で到達点に達したが, 以下は未完なので次回進めたい.

## 合意済タスク (優先順)

1. **A1 10⁹ 完全 census** — primary funnel scale-dependence 確認 (推定 3-5 h)
2. **A2 10¹⁰ sparse sample** — tier2 bound unconditional 範囲拡張
3. **A3 Wieferich-Fibonacci 深掘り** — Paper 108 候補 (T-WC/T-WC+ 構造根拠)
4. **A4 MANDALA v13** — E28 Lyapunov / E29 Ricci / E30 Entropy 追加
5. **A5 新 primary funnel at 10⁹** — prime signature 解析
6. **A6 Fujimoto conjectures 拡張** — T-FS/T-WC 漸近 fit

## 詳細 roadmap

`docs/next-session-collatz-roadmap.md` に完全版保存済.

## A6 以降の延長 (2026-04-17 session 中に藤本合意, 追加)

7. **A7 Agda 深統合** — 依存型証明環境. src/axiom-os/agda-bridge-engine.ts で subprocess, Collatz を Agda に移植 (∞-groupoid 対応)
8. **A8 Isabelle/HOL 深統合** — sledgehammer + 既存 Collatz preprint (2025-08 preprints.org) 輸入 + Lean4 cross-verification
9. **A9 Coq/Rocq 深統合** — A7/A8 後 optional. Mathematical Components + coq-collatz 輸入

**動機**: 現状「段階 3 (深統合)」は Lean4 + Python + tombursey のみ. チャット版 Claude の「世界の OSS」列挙に対し、Rei の実態を正直チェックしたら Agda/Isabelle/Coq/Metamath/Maxima/Rocq/HoTT 等が未統合と判明 (2026-04-17 session 中). Agda/Isabelle は ∀n 証明系として Lean4 の補完的価値あり.

## A0 (2026-04-17 進行中, 並行で着手済)

- **A0.1 tombursey clone + Mathlib v4.27 互換** ✅ 完了 (commit 6865514, 2026-04-17)
- **A0.2 drift 補題 Rei mod-96 移植** 🟡 進行中 (Step841TomburseyBridge.lean zero-sorry zero-axiom build OK)
- **A0.3 Paper 108 統合草稿** ⏳ census 完了後

## 進めない (honest scope)

- 3 Collatz-equivalent axioms (C1/C2/C3) の proof — Collatz 本体解決が必要
- これらは peer reviewers のスコープ

## 現状 tier2 summary

- Paper 105/106/107 投稿完了 (conditional complete proof + 数式 compendium)
- 10⁷/10⁸ stride 0 violations (8.46M integers)
- Lean4 17 axioms (3 Collatz-equivalent 残存)
- Zenodo DOI 19601544/19601546/19601565