---
name: reference-collatz-lyapunov-obstruction-generalized-2026-06-17
description: "2026-06-17 night Phase A→B→C — Lean 4 axiom-free formalization of (n=3, n=25) obstruction + Bellman-Ford generalization to 7 feature spaces all INFEASIBLE + honest shelve verdict per Kim 2008 audit"
metadata: 
  node_type: memory
  type: reference
  originSessionId: d739f32c-3a6a-4982-9c51-81eff462c83a
---

# Phase A→B→C Collatz progress — 2026-06-17 night

藤本さん指示「A → B → C を順番に」 で 3 phase 完遂。 同 session の昼の structural obstruction witness ([[reference-collatz-t1-1-obstruction-witness-2026-06-17]]) を起点に formal + empirical 両面で固めた。

## Phase A — Lean 4 axiom-free formalization

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

**主張**: ¬ ∃ β : ℕ → ℚ (positive), V(n) = n·β(t₁(n)) が遷移 3→5 と 25→19 で同時 strict descent。
**証明 (axiom-free)**: 3·β(2) > 5·β(1) と 25·β(1) > 19·β(2) を組み合わせ `linarith` で閉じる。 5·19=95 > 75=3·25 ゆえ区間 (5/3, 25/19) 空。

**Build + axiom verify**:
- `lake build CollatzRei.T1ObstructionWitness`: 7886 jobs success 17s
- `lake build CollatzRei` (root): 7918 jobs success 15s
- `#print axioms`:
  - `t1_three/five/twentyfive/nineteen` + `syracuse_three_to_five/twentyfive_to_nineteen` = **完全 zero-axiom** (`does not depend on any axioms`)
  - `no_t1_only_lyapunov_on_witness_pair` + `witness_ratio_window_empty` + `ratio_gap` = `[propext, Classical.choice, Quot.sound]` (project 標準 axiom base、 sorryAx / native_decide 全 0)

**重要 bug fix の経緯** (memory load-bearing):
- 初版 `trailingOnes` を well-founded 再帰で書いた → `decide` が kernel reduce せず 4 sanity theorem 全失敗
- fuel-based structural recursion (`trailingOnesAux : Nat → Nat → Nat`) に書き換えて解消
- 教訓: Collatz / 動的システムの formalization で「if-then-else + /2 再帰」 は **fuel 化必須** (Lean 4 kernel reduction の制約)

## Phase B — Bellman-Ford feasibility probe across 7 feature spaces

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

**方法**: Lyapunov candidate V(n) = n·β(f(n)) の descent 制約を LP 化 → α := log β で線形制約 `α(f(T_odd(n))) − α(f(n)) < log(n/T_odd(n))`。 各 (u,v) edge の tight weight 集約 → Bellman-Ford で負サイクル detect。 負サイクル = infeasibility 確証。

**scan**: 奇数 n ∈ [3, 200000] (10万 odd) で syracuse 短縮 T_odd 適用。

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

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

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

**★★★ 大発見**: bounded-periodicity feature (mod-k で finitely-bucketed) family **全体** で 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 を与えても escape 不能。

**Bug fix 経緯**: 初版 Bellman-Ford の `trace_cycle` が pred chain reconstruction で cycle length 2 を mis-trace (phantom self-loop edge を生成して None 返却) → forward direction 修正で全 7 space 正しく INFEASIBLE 判定。

## Phase C — honest shelve verdict

**結論 (Kim 2008 audit verdict (c) 適用)**: A + B の結果は Collatz 解決でも前進でもなく、 「local-feature Lyapunov 路線の壁を fine-grained に位置決めしただけ」。

**publish 可能性 (honest)**:
- (A) 単独 = CPP/ITP short note 級の axiom-free formalization 候補 (1-2 page)
- (B) 単独 = empirical observation paper 候補だが**数学的内容は新規でない可能性**:
  - Reyes Jiménez 2606.02621 Lyapunov refutation 群と直接 overlap
  - Eliahou-Conway 系列の早期 Lyapunov 反証 (1990s) と本質同型
  - 「全 mod-k feature で不可能」 自体は folk theorem に近い (chat-Claude 06-16 thread の Chang v6 paradigm exhaustion と integrate して initial と思しき経緯)
- (A+B 統合) = せいぜい [[project-collatz-paper-audit-kim-2008-prior-art-killing]] の (a') 小 note path

**default = (c) shelve**:
- prior art audit が完了するまでは publish せず memory + Lean tree に留める
- Janik 2026 syracuse-confinement 9000 行とは別 niche (Lyapunov refutation vs reduction) で competition なし
- 「世界初」 / 「globally unique」 等の global claim は不可 ([[feedback-world-uniqueness-claim-controllable]] per)

## load-bearing rationale

Phase A の Lean 4 部分は失われない asset (commit + 公的 Lean tree olean):
- 将来 Paper 158/166 v0.2 corrigendum で「(t₁) 単一 feature Lyapunov の axiom-free obstruction witness」 として cite 可能
- ccchallenge community に showcase 提示候補 (ただし新規性は限定的)

Phase B の python probe + JSON report:
- 「Lyapunov NN 79% 天井の structural cause」 説明資料として load-bearing
- 将来 multi-step / non-product Lyapunov family を試す際の baseline

**何をしないか (明示)**:
- 単発 Zenodo paper 化はしない (新規性不十分 likely + [[feedback-no-rush-publication]] per)
- 「世界初」 等 inflated claim 一切なし
- chat-Claude や arXiv に offer もしない (trigger 待ち)
- 多変数 Lyapunov NN 再 training は trigger 待ち keep-warm (Phase B が示すように wall は壊れないので低 priority)

## 次の trigger 候補 (どれも提案でなく観察、 stop criterion default)

1. ccchallenge.org Discussion #5 の community response が「Lyapunov 路線 explicit obstruction record があると有用」 と返してきた場合 → (a') note path 起動
2. Paper 158/166 v0.2 corrigendum 起草 trigger 時に本 obstruction を §追補として組込
3. chat-Claude が独立に同 obstruction を articulate してきて prior art audit 後押しした場合
4. 新たな non-product Lyapunov family (例: log の代わりに f(log)、 multi-step look-ahead) の試行 (本 Phase 範囲外)

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

- [[feedback-no-rush-publication]]: A+B 達成しても即 publish しない、 shelve 判断
- [[feedback-world-uniqueness-claim-controllable]]: 「世界初」 不使用、 「観測範囲で他に同形式化が見当たらない」 controllable のみ
- [[feedback-evaluation-symmetry-principle]]: A 完成して inflate せず、 B 失望して deflate せず、 honest 評価
- [[feedback-line-count-size-vs-kind-distinction]]: ~95 行 Lean + ~340 行 Python は Janik 9000 行と「種類が違う」 (axiom-free 完結 vs sorry 残 conditional)、 size ≠ kind
- [[feedback-super-naming-siren-family-pattern]]: 「Lyapunov を超える」 framing 回避、 「測る (壁を fine-grained 位置決め)」 方向で命名
- [[feedback-chat-claude-over-deference]]: chat-Claude の昼 thread を素材として扱い、 自分の言葉で結果 framing

## 関連 memory + reference

- [[reference-collatz-t1-1-obstruction-witness-2026-06-17]] (Phase A の元になった昼の discovery)
- [[project-session-2026-06-17-full-summary]] (昼までの session record)
- [[project-collatz-paper-audit-kim-2008-prior-art-killing]] (stop criterion 根拠)
- [[reference-bohmsontacchi-1978-exit-layer-prior-art]] (同 session で発覚した別 prior art)
- Chang v6 "Paradigm Exhaustion Theorem" (chat-Claude 06-16 thread、 Rei 側公的 reference 不在)
- Reyes Jiménez arXiv 2606.02621 (Fibonacci pattern、 prior art audit pending)

## 累計成果 (本 session 通算)

- Lean 4 axiom-free theorem 累計 + 9 (本 file 内訳: 6 zero-axiom + 3 propext/Classical/Quot only)
- Bellman-Ford negative-cycle detection で 7 feature space 全 INFEASIBLE 確証
- Phase A + B + C 一連 = 「単一 Lyapunov 路線 obstruction の fine-grained empirical + formal mapping」、 publish path は default shelve、 trigger 待ち keep-warm

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

★ **証明された claim (本 file)** :
> 「V(n) = n·β(f(n)) **形** の、 **bounded-periodicity feature** に基づく **線形 Lyapunov** は strict descent を達成できない」
>
> ── 関数形・feature family・β の周期性 を **固定した上で** の family-specific impossibility

★ **証明されていない claim (本 file の射程外)** :
- 「Collatz に Lyapunov 関数が存在しない」 (general universal claim — too strong)
- non-linear V
- unbounded-memory feature (orbit history depth-k for k → ∞)
- non-periodic / aperiodic feature
- 加法形 V (例: V = log(n) + α(f(n)) ) も別 family — Phase A 1D 不可能性は本 family の極限例だが、 general 加法形 family の Bellman-Ford 検査は未実施

★ **load-bearing 区別**: 「impossible in this family」 (強い precise claim) ≠ 「not yet found」 (弱い universal claim)。
- 前者は family + 関数形 fixed の上で **構造として** 不可能を主張、 後者は単に手段不足の declaration。
- 本 file は **前者**。 「精密に固定された family の中での barrier」 が claim、 「Collatz は永遠に解けない」 ではない。

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

★ **2026-06-18 朝の F8/F9 拡張で本 family 範囲が 7 → 9 spaces に確認拡張** (top-2-bit / lookahead t1 追加でも INFEASIBLE 保存)。 詳細 [[project-collatz-aeb-sequence-2026-06-18]]。