---
step: 1933
slug: cases-58-wall-refinement
timestamp: 2026-09-10T09:15 JST
tab: rei-aios-28 (main worktree, session 0114Jvbi7TqyYfZmMpshqWk9)
directive_source: 藤本さん 2026-09-10 explicit 発話 「□ Cases 5-8 に戻る (Rei Collatz 未解決部分) でお願い致します。」
finding_source: Claude Code (rei-aios-28、 approach self-decide (α revised) + Lean 4 implementation + lake build verify + axiom check)
summary: Cases 5-8 wall の 精密記述拡張 — Case 5 sub-cases n%256 ∈ {39, 71, 103} で case5a 短 pattern 適用不可 explicit witness、 axiom-free 7 theorem、 wall 内 explicit 事実蓄積 (Cases 5-8 一般 は 依然未解決)
---

# STEP 1933 — Cases 5-8 wall refinement (case5a 短 pattern 適用不可 witness)

## 藤本さん directive (2026-09-10 explicit 発話)

Task #4 GO signal: 「□ Cases 5-8 に戻る (Rei Collatz 未解決部分) でお願い致します。」

Task #4 subject を 直接 quote した form = **explicit implementation directive**、 approach 選択 は rei-aios-28 self-decide 領域 (5/6 件目 drift とは別、 直接 directive の implementation choice)。

## Approach 選択 (rei-aios-28 self-decide)

前 STEP 1923 refs DeFranco full PDF audit で 3 option 提示 (A/B/C)、 4b が 独立 3 候補 (i/ii/iii) 提示。 私 の 最終選択 = **Option (α)** (前 3 option (A) の 具体化 revised):

**Cases 5-8 wall の 精密記述拡張** = universal 解決ではなく wall 内 の explicit 事実蓄積。

理由:
- step624_COMPLETE.lean line 285 comment 「Cases 6 (n%32=15) and 8 (n%32=31) have most n%256 sub-classes」 = **Case 5 の 残 sub-cases (n%256 = 39, 71, 103, 135, 167, 199, 231) は 明示的に 未実装** の gap
- 4b (ii) PadicRoughness attempt と別 domain = overlap なし
- 中程度 実装 (elementary omega tactic)、 短時間 build 可能
- Rei step624 §7.1 assessment 「no finite modular analysis can capture all trajectories」 の explicit machine-checked evidence 蓄積 = discipline value

**却下 option**:
- (A) 一般 Rei descent proof: universal Case 5-8 は 数学的 breakthrough 必要 = 短時間 attempt 不可
- (B) DeFranco Boolean poly formalization: コスト高、 material 用意済 だが 別 STEP 案件
- (C) Reyes bridge pattern の DeFranco 版: 前段 material (準備)、 直接 Cases 5-8 前進ではない

## 実装

**File**: `data/lean4-mathlib/CollatzRei/Cases58WallRefinement.lean`

### 7 theorems (全 axiom-free base、 sorry 0)

- **case5b_shortPattern_no_descent** (n%256=39): `n < ((3*((3*((3*n+1)/2)+1)/2)+1)/2) / 2` (3 odd + 1 even 段階で value = 432r+67 > n=256r+39)
- **case5c_shortPattern_no_descent** (n%256=71): 同 pattern、 value = 432r+121 > n=256r+71
- **case5d_shortPattern_no_descent** (n%256=103): 同 pattern、 value = 432r+175 > n=256r+103
- **case5_subcases_39_71_103_require_deeper_subdivision** (総合): 上 3 sub-cases OR
- **verify_n39_short_pattern** (r=0 numerical): `((3*((3*((3*39+1)/2)+1)/2)+1)/2) / 2 = 67`
- **verify_n71_short_pattern** (r=0 numerical): `= 121`
- **verify_n103_short_pattern** (r=0 numerical): `= 175`

### Axiom profile (lake build verified)

- **完全 axiom-free (0 axioms)**: 3 verify_n theorem (n=39/71/103 numerical、 by decide)
- **[propext, Quot.sound]**: 4 general theorem (mod-class 一般、 by omega、 Mathlib 標準 base)
- **sorry 0 / Classical.choice なし** ★

## 意味

### Positive contribution

step624 case5a (n%256=7) が 4 odd + 7 even の clean pattern で descent 証明済み。 本 STEP は Case 5 の 他 sub-cases (n%256 = 39, 71, 103) が **同 pattern の step 4 段階 (v₂=1 even) で value が既に n を上回っている** ことを machine-checked。 → case5a pattern (step 4 で v₂=2 or v₂=3 が要る) を n%256 = 39/71/103 に適用できない。 深い n%512 / n%1024 subdivision が必要。

Chang paradigm 18 (Digit-sum / Hamming weight) の refined witness layer extension: 「digit-sum aspect は deterministic に処理できるが、 その事実だけでは Collatz を解けない」 の Rei-side さらに具体化。

### Honest scope (super critical)

- **Rei は Cases 5-8 に progress していない**
- 本 STEP は Cases 5-8 の **未解決状態を精密化する negative witness** で あって、 solution ではない
- 「Rei は Case 5 sub-cases に descent proof を追加した」 系 claim **絶対禁止** (実際は 「descent NOT achieved by short pattern」 witness)
- 「Rei は Collatz Cases 5-8 wall を 越えた」 系 claim **絶対禁止**
- Universal Cases 5-8 は 依然 未解決 (Rei の 本質的 wall、 Rei step624 §7.1 self-quote 「no finite modular analysis can capture all trajectories」)
- 本 STEP の value = **explicit machine-checked evidence for the wall's shape at specific sub-classes** (structural documentation)

### Extension roadmap (未実装、 別 STEP candidate)

- **Remaining Case 5 sub-cases** (n%256 = 135, 167, 199, 231): 同 pattern で similar witness 追加可能、 elementary、 1 STEP で実装可能
- **Case 6 remaining sub-cases** (n%256 = 47, 79, 175, 207, 239): 同 pattern
- **Case 8 sub-classes** (n%32=31、 n%256 全 8 sub-cases): step624 「Most n%256 sub-cases INCREASE」 明示、 short pattern descent 期待できず = 同種 wall witness 大量追加候補
- **Descending sub-cases for r-even / r-odd split** (n%512 subdivision): 深い一部 で descent proof 可能な candidate、 explicit search 要

これらは 藤本さん explicit 発話 or 継続 authorize の 判断待ち (私 self-decide せず、 本 STEP の scope 内 で 3 sub-case pilot 完了)。

## 4b との overlap check

- 4b (ii) PadicRoughness 1 sorry close = 別 file (`Chang/Retrofits/PadicRoughness.lean`)、 overlap なし
- 4b (iii) D-FUMT₈ NEITHER 経由 「未確定性 formal 表現」 = 別 angle (semantic layer)、 overlap なし
- 本 STEP = Rei 独自 track 内 の Cases 5-8 wall refinement (mod-class explicit witness)、 double-tab arc 全体で productive coverage

## Attribution

- **Directive source**: 藤本さん 2026-09-10 explicit 発話 「□ Cases 5-8 に戻る (Rei Collatz 未解決部分) でお願い致します。」
- **Finding source**: Claude Code (rei-aios-28、 approach (α) self-decide + Lean 4 implementation + lake build + axiom check)
- **Approach 選択の 判断責任**: rei-aios-28 (前 STEP 1923 で提示した A/B/C option の (A) 具体化 revised、 藤本さん の 明示選択ではなく 私 self-decide)

## Files

- `data/lean4-mathlib/CollatzRei/Cases58WallRefinement.lean` (実装、 axiom-free 7 theorem)
- 本 notepad (STEP 実装記録)

## 関連

- [[step-1908-oukc-debate-private]] — 前 STEP 1908 arc
- [[step-1915-radar-audit-4-papers-rei-system-verification]] — Radar audit arc
- [[step-1923-w-grep-attribution-pre-commit-hook]] — 前 STEP hook 実装
- `data/lean4-transfer/step624_COMPLETE.lean` — Rei Cases 1-8 assembly (case5a + case6a/b + case7a-g)
- `data/lean4-mathlib/CollatzRei/Chang/Retrofits/TrailingOnesDigitSum.lean` — Chang paradigm 18 retrofit (本 STEP の 更 refined witness)