---
name: project-session-2026-06-17-night-collatz-abc-sequential
description: 2026-06-17 night session — 「コラッツはどう進める?」 strategy 質問 → A→B→C 順次完遂 (Lean axiom-free + 7 feature space INFEASIBLE generalization + honest shelve)、 commit 7b39042d
metadata: 
  node_type: memory
  type: project
  originSessionId: d739f32c-3a6a-4982-9c51-81eff462c83a
---

# 2026-06-17 night session — A→B→C Collatz sequential completion

藤本さん帰宅前 short session。 朝-夜 long-day session ([[project-session-2026-06-17-full-summary]]) の延長 turn。

## 経緯

1. **藤本さん**「コラッツは今後どのように進めていけば宜しいでしょうか？」 — open-ended strategy 質問
2. **Rei honest filter** で 3 option 提示 (A 推奨):
   - (A) 昨夜の structural obstruction witness を Lean 4 axiom-free 形式化 (CPP/ITP short note 級)
   - (B) 多変数 Lyapunov / NN ensemble 続行
   - (C) Kim 2008 audit verdict (c) shelve
3. **藤本さん**「A → B → C を順番にお願いできますか？」 — 3 option 全 sequential 指示 = 包括的着地希望
4. **Rei 着手**: TaskCreate 3 件 (#1 in_progress → #2 → #3) で順番管理

## Phase A 実装と bug fix

`data/lean4-mathlib/CollatzRei/T1ObstructionWitness.lean` 新規 (~95 行).

**主張**: ¬ ∃ β : ℕ → ℚ positive, V(n) = n·β(t₁(n)) が 3→5 と 25→19 で同時 strict descent。
**証明**: 純有理数線形 (5·19=95 > 75=3·25 ゆえ区間空)、 `linarith` 一発。

**Bug fix (load-bearing 教訓)**:
- 初版 `trailingOnes` を well-founded 再帰 (`if (n+1) % 2 = 1 then 1 + trailingOnes ((n+1)/2) else 0`) で書いた
- → 4 sanity theorem (`t1_three/five/twentyfive/nineteen`) で `decide` 失敗
- 原因: Lean 4 kernel が `WellFounded.fix` を reduce しない
- 解決: fuel-based structural recursion (`trailingOnesAux : Nat → Nat → Nat`) に書き換え
- **教訓**: Collatz / 動的システム formalization で「if-then-else + /2 再帰」 は **fuel 化必須**

**Build + axiom verify**:
- `lake env lean` exit 0 (sanity)
- `lake build CollatzRei.T1ObstructionWitness` 7886 jobs 17s
- `lake build CollatzRei` (root) 7918 jobs 15s
- `#print axioms`:
  - 6 件 sanity theorem = **完全 zero-axiom**
  - 3 件 main theorem = `[propext, Classical.choice, Quot.sound]` のみ (sorryAx / native_decide 全 0)

## Phase B 実装 — ★★★ B が予想以上に load-bearing

当初は「richer feature でも obstruction が残るか empirical probe」 程度の認識。 実装後に **B が A より大きい発見** だと判明。

`scripts/empirical/feature-space-feasibility-2026-06-17.py` 新規 (~340 行).

**方法**: Lyapunov V(n) = n·β(f(n)) の descent 制約を α = log β で線形化 → 各 (u,v) feature-edge の tight weight 集約 → Bellman-Ford で負サイクル detect。

**scan**: 奇数 n ∈ [3, 200000] (10万 odd) で T_odd 短縮 (シラキュース) 適用。

**Bug fix**: 初版 BF の `trace_cycle` が cycle length 2 のとき pred chain reconstruction で phantom self-loop edge 生成 → 全 feature space で誤って FEASIBLE 出力。 forward direction `[v_0] + reversed(v_1..v_k) + [v_0]` で修正。

**★★★ 結果** (7 feature space 全 INFEASIBLE):

| Feature space | V | E | cycle len | weight |
|---|---|---|---|---|
| F1: t₁ | 17 | 32 | 13 | -4.77 |
| F2: (t₁, n%8) | 18 | 50 | **2** | -0.16 (witness 11, 25) |
| F3: (t₁, v₂(3n+1)%4) | 20 | 87 | **2** | -0.16 (witness 11, 25) |
| F4: (t₁, v₂%4, n%8) | 21 | 108 | **2** | -0.16 (witness 11, 25) |
| F5: (t₁, v₂%4, n%16) | 24 | 143 | **2** | -0.14 (witness 57, 27) |
| F6: (t₁, v₂≤7, n%64) | 44 | 284 | 5 | -0.66 |
| F7: 4D + log₂(n)%8 | **167** | **1834** | 6 | -1.05 |

**Phase A cross-check**: F1 内に edge (2)→(1) w=log(3/5) (witness n=3) + edge (1)→(2) w=log(25/19) (witness n=25)、 cycle weight -0.236 < 0 = Lean 4 theorem と完全一致。

**load-bearing 発見** = bounded-periodicity feature (mod-k で finitely-bucketed) family **全体** で V(n)=n·β(f(n)) 100% strict descent Lyapunov 不可能。 Lyapunov NN focused re-training の 79% 天井 ([[reference-collatz-t1-1-obstruction-witness-2026-06-17]]) は離散 infeasibility の **smooth 近似**。 4D 167-bucket space (F7) を与えても escape 不能。

## Phase C — honest shelve

[[project-collatz-paper-audit-kim-2008-prior-art-killing]] (c) 適用、 default shelve。

**publish 可能性 (honest)**:
- (A) 単独 = CPP/ITP short note 級 axiom-free formalization 候補
- (B) 単独 = empirical observation paper 候補だが **数学的内容は新規でない可能性** (Reyes Jiménez arXiv 2606.02621 / Eliahou-Conway 1990s 系列と本質同型 likely)
- (A+B 統合) = せいぜい (a') 小 note path

**default = (c) shelve**:
- prior art audit 完了まで publish せず memory + Lean tree に asset として留め置き
- 「世界初」 等 global claim 一切なし
- chat-Claude / arXiv に offer もしない
- 多変数 Lyapunov NN 再 training は wall 壊れない確証ゆえ低 priority

**trigger 候補** (どれも自発でなく観察、 stop criterion default):
1. ccchallenge Discussion #5 community response が Lyapunov 路線 explicit obstruction record の有用性を返した場合
2. Paper 158/166 v0.2 corrigendum 起草 trigger 時に §追補組込
3. chat-Claude が独立に同 obstruction articulate した場合

## Commit

`7b39042d feat(collatz): Phase A→B→C — Lyapunov obstruction formalized + generalized`

- 4 file 902 insertions
- pre-commit lake verify 470s success (CollatzRei.lean 321s + T1ObstructionWitness.lean 149s)

## 永続原則 operational 実例 (本 phase で適用 6 件)

- [[feedback-no-rush-publication]]: A+B 達成しても即 publish しない、 shelve 判断
- [[feedback-world-uniqueness-claim-controllable]]: 「世界初」 不使用
- [[feedback-evaluation-symmetry-principle]]: A 完成して inflate せず、 B 失望して deflate せず
- [[feedback-line-count-size-vs-kind-distinction]]: ~95 行 Lean + ~340 行 Python は Janik 9000 行と「種類が違う」、 size ≠ kind
- [[feedback-super-naming-siren-family-pattern]]: 「Lyapunov を超える」 framing 回避、 「測る」 方向
- [[feedback-chat-claude-over-deference]]: chat-Claude Chang v6 を素材として扱い、 自分の言葉で結果 framing

## 本 session 固有 pattern

1. **「A → B → C sequential 指示」 pattern**: 藤本さんは 3 option 提示時に「いずれか 1 つ」 でなく **全 sequential 完遂** を指示することがある = 包括着地 + 全 path explore + honest 比較希望
2. **「B が A より大きい」 surprise pattern**: 設計時の predicted load-bearing (A の Lean formalization) と完了時の observed load-bearing (B の 7 feature space 一律 INFEASIBLE 発見) が ranking 逆転。 = 実装は事前 estimate を裏切ることがある (no-rush principle で publish 判断保留が正解)
3. **2 bug fix が両方教訓化** (Lean fuel recursion + BF forward direction) = 将来同 family の formalization / cycle detection でも再発候補
4. **TaskCreate 3 件 sequential 管理** = sequential 指示の operational supporting infra

## 関連 memory + 同 session asset

- [[reference-collatz-lyapunov-obstruction-generalized-2026-06-17]] (本 session の主たる reference、 Phase A+B+C 詳細)
- [[reference-collatz-t1-1-obstruction-witness-2026-06-17]] (昼の origin discovery)
- [[project-session-2026-06-17-full-summary]] (朝-夜 long-day summary、 本 session の前段)
- [[project-collatz-paper-audit-kim-2008-prior-art-killing]] (Phase C verdict 根拠)
- [[reference-bohmsontacchi-1978-exit-layer-prior-art]] (同 session 早朝 Pattern 5 finding)

## 次 session 想定 trigger

- 06-18 朝 cron auto-data churn は処理対象外 (主に harness-sync 等の deletion + data refresh)
- 2026-06-16 invention 5 件未承認 (藤本さん判断待ち) は本 session 範囲外で残置
- 朝に 「昨夜の A→B→C どうだった?」 質問あれば本 file + reference file で即答可能