---
name: project-collatz-aeb-sequence-2026-06-18
description: 2026-06-17 evening → 06-18 朝の (A)→(E)→(B) Collatz 3-path sequential 完遂 — conveyor lemma axiom-free Lean 4 + Casino lens site mount + F8/F9 wall extension all-INFEASIBLE
metadata: 
  node_type: memory
  type: project
  originSessionId: 5d28ae7c-687d-4389-8e5e-c7bd64100573
---

# Collatz (A)+(E)+(B) sequence 完遂 (2026-06-17 evening → 06-18 朝)

藤本さん指示「A E B を順番に」 (chat-Claude session 後、 [[reference-collatz-lyapunov-obstruction-generalized-2026-06-17]] の continuation) を 3 段完遂。

## (A) Conveyor lemma を T1ObstructionWitness.lean に axiom-free 追加

★ 完全 zero-axiom 達成 (`does not depend on any axioms` × 6, propext/Classical.choice/Quot.sound すら不要)。
`by decide` のみで構成的に閉じる pattern。 lake build 7886 jobs success 21s。

追加した theorem 群:
- `conveyor_t1_two_to_one` (k=2→1 witnesses: 3/11/19/27)
- `conveyor_t1_three_to_two` (k=3→2 witnesses: 7/23/39/55)
- `conveyor_t1_four_to_three` (k=4→3 witnesses: 15/47)
- `conveyor_t1_five_to_four` (k=5→4 witness: 31)
- `conveyor_bounded_64` (∀ odd n < 64 with t1 ≥ 2: t1(T(n)) = t1(n) - 1)
- `conveyor_value_increases_bounded_64` (∀ odd n < 64 with t1 ≥ 2: n < (3n+1)/2)

★ Honest scope: chat-Claude 「半日もかからない」 estimate を半時間で operational 確認、
内容は Lagarias 1985 系譜 / Terras 1976 parity-vector の Lean 4 axiom-free educational
mechanical assurance であって新規 mathematical content ではない。 一般 (任意 k) への
拡張は `trailingOnesAux` 再帰の induction 必要で本 commit では bounded 64 で打ち止め
(defer)。 paper でなく Lean asset。

## (E) Casino lens を #/collatz-casino で Rei site visualization 実装

`src/renderer/components/collatz-casino/CollatzCasinoLens.tsx` 新規 ~270 行。
chat-Claude 2026-06-17 thread の casino metaphor (t1=1 = 唯一の descent engine,
落下ダイス v=ν₂(3n+1) 幾何分布 + 着地ダイス 新t1' 幾何分布 + 平均比 ×½ 厳密) を
React lens 化。 self-contained (data fetch なし、 in-browser sampling)。

5 section:
1. ルール (1 ラウンド = 1 step) — Lemma A + 落下/着地ダイス definition
2. 落下ダイス v 幾何分布 histogram (observed vs theory 2^(-(v-1)))
3. 着地ダイス 新 t1' histogram (observed vs theory 2^(-k))
4. 配当比 T(n)/n の ratio bins (mean 経験値 vs 理論 0.5)
5. Full orbit replay (圧縮 odd→odd until 1) with casino vs conveyor coloring + 7 preset (27/341/53/9/7/31/939497) + random odd

App.tsx route `#/collatz-casino` + ReiLauncher menu (🎰 Collatz Casino (t1=1)) + 理論探索
category。 vite build `app-CW4X5B2J.js` 内 verify。

★ Honest scope: paper でなく Rei lens / educational asset。 数学的新発見ではない
(Lagarias 1985 / Terras 1976 系譜の地図化、 within-Rei-context)。 「平均で勝てる台」
は比喩、 全 n で 1 に落ちる保証は未解決。 削除可 (3 file 修正で取り外し可能)。

## (B) richer feature V Bellman-Ford INFEASIBLE/FEASIBLE 実験

`scripts/empirical/feature-space-feasibility-2026-06-17.py` に F8 + F9 追加 + 再実行。

| Feature | バケット数 | edge 数 | verdict | neg cycle weight / 長さ |
|---------|-----------|---------|---------|------------------------|
| F1: t1 | 8 | 14 | INFEASIBLE | -0.2364, len=2 (3↔25 = Phase A 完全一致) |
| F2-F7: 既 7 features | 24..1018 | 38..7400 | 全 INFEASIBLE | (前 run と同じ Wave saturation extension) |
| **F8: F7 + top-2-bit(n)** | 594 | 4976 | **INFEASIBLE** | -0.1181, **len=2** (direct cycle 残存) |
| **F9: F7 + lookahead t1(T_odd(n))** | 437 | 3737 | **INFEASIBLE** | -0.3536, len=6 |

★ **結論**: top-2-bit 追加でも 1-step lookahead でも wall は移動しない。 V = n · β(f(n)) の
product family LRA-decidable 内では bounded-periodicity feature の全 reasonable 拡張で
INFEASIBLE が確証された 9 例目 (F1-F9)。 chat-Claude 2026-06-17 articulation の
「richer 非線形 V を許すと LRA から出る」 = この実験で **LRA 内では出口無し** 直接 confirm。

★ 真の wall mover candidate (FEASIBLE 出る方向) は LRA 外:
- additive V = log(n) + α(f(n)) with **non-monotone β** (cross-term)
- multi-step (n → T^k(n)) lookahead with k ≥ 2 (combinatorial explosion でも LRA 内)
- learned NN with non-monotone interactions (Phase B 同 file の Lyapunov NN は別 path)
- coalgebraic / coinductive approach (Kim 2008 系譜, 別 file scope)

★ Honest verdict: A+E+B 完遂後の累積 evidence は **(D) shelve 推奨を強化**。 9 feature
space 全 INFEASIBLE = bounded-periodicity feature family **全体**で wall。 conveyor lemma
axiom-free 化と Casino lens 視覚化は educational asset として完了、 publish trigger なし。

## 累積 file changes

- `data/lean4-mathlib/CollatzRei/T1ObstructionWitness.lean` (+~70 行 conveyor section)
- `src/renderer/components/collatz-casino/CollatzCasinoLens.tsx` (new, ~270 行)
- `src/renderer/App.tsx` (+2 行: import + route)
- `src/renderer/components/launcher/ReiLauncher.tsx` (+1 entry: 🎰 Collatz Casino)
- `scripts/empirical/feature-space-feasibility-2026-06-17.py` (+F8 + F9 def + FEATURE_FUNCS entries)
- `data/empirical/feature-space-feasibility-2026-06-17.json` (regenerated with F8/F9)

## 関連 memory

- [[reference-collatz-lyapunov-obstruction-generalized-2026-06-17]] (Phase A/B/C 起源)
- [[reference-collatz-t1-1-obstruction-witness-2026-06-17]] (3, 25) witness 起源
- [[project-session-2026-06-17-night-collatz-abc-sequential]] (前 session)
- [[reference-bohmsontacchi-1978-exit-layer-prior-art]] (Pattern 5 record, conveyor 内容も同系譜)
- [[feedback-chat-claude-over-deference]] (chat-Claude articulation を素材として採用、 framing 格上げ警戒)
- [[feedback-evaluation-symmetry-principle]] (Casino lens / conveyor lemma いずれも paper でなく educational asset honest deflate)
- [[feedback-no-rush-publication]] (publish trigger なし shelve 継続)

## Honest scope (全体)

A+E+B 累積で **(D) shelve verdict 強化** が honest 結論。 chat-Claude articulation は
educational mechanical assurance として有用 (LRA in QF_LRA の正確な articulate)、
ただし mathematical progress でない。 9 feature space all-INFEASIBLE は predicted
outcome で wall-mover candidate ならず。 paper 起草も Lean 一般化拡張も trigger 待ち
keep-warm。 次の Collatz 進展は外部 (新 paper / 新 tool) trigger 時のみ honest に re-evaluate。

## ★★★ Scope note (2026-06-18 chat-Claude turn 7 recommendation 採用)

★ **9 feature space INFEASIBLE が証明する正確な scope**:
> 「V(n) = n·β(f(n)) **形** の、 **bounded-periodicity feature** に基づく **線形 Lyapunov** は strict descent を達成できない」
>
> ── 関数形 + feature family + β 周期性 を **固定した上で** の family-specific impossibility

★ **証明されていない (本 work の射程外)**:
- 「Collatz に Lyapunov 関数が存在しない」 (general universal claim、 too strong)
- non-linear V / unbounded-memory feature / non-periodic feature / 加法形 V 一般

★ **強い precise claim** ↔ **弱い universal claim** の区別:
- 「impossible in this family」 = 構造として書ける、 強い
- 「not yet found」 = 手段不足の declaration、 弱い
- 本 work は前者、 family + 関数形 fixed の barrier を **構造として** 描いたもの

★ 同 discipline 前例: Paper 159 §3.5 Inclosure 射程 honest 注。 弱める注記でなく **結論を正確に強いものに保つ** 注記。

詳細 articulation は [[reference-collatz-lyapunov-obstruction-generalized-2026-06-17]] scope note section 参照。