STEP 1933 · Rei-AIOS · Collatz Cases 5-8

Cases 5-8 wall refinement

case5a 短 pattern (4 odd + 7 even) が n%256 ∈ {39, 71, 103} で 適用不可 の explicit machine-checked witness。 Cases 5-8 の 未解決状態を 精密化する negative witness であって solution ではない (Rei は Cases 5-8 に progress していない)。

Landed: 2026-09-10 · commit 5d5d9622e (rei-aios-28 main worktree) · File: data/lean4-mathlib/CollatzRei/Cases58WallRefinement.lean · GitHub: source · Notepad: 記録

Overview

// wall witness, not solution

Rei step624_COMPLETE.lean は Collatz Cases 1-4 で ∀n descent 証明を axiom-free に達成、 Case 5 sub-case n%256=7 (case5a) で 4 odd + 7 even の clean pattern 経由 で descent 証明済み。 一方 Case 5 の 残 sub-cases (n%256 = 39, 71, 103, 135, 167, 199, 231) は step624 で 明示的に 未実装。

本 STEP は これら 残 sub-cases の うち n%256 ∈ {39, 71, 103} について、 case5a と 同 pattern (3 odd + 1 even = 4 step) を 適用した場合 に value が n を 下回らない (v₂=1 の 短 pattern では descent 不能) ことを elementary omega tactic で explicit machine-verify する。

これは Rei step624 §7.1 self-quote 「no finite modular analysis can capture all trajectories」 の explicit 具体例 として、 Cases 5-8 wall の 精密構造 を machine-checked evidence で 記述する negative witness である。

7 theorems (axiom-free base)

// 全 sorry 0, Classical.choice なし, lake build 2.0s

Theorem Statement (informal) Axioms
case5b_shortPattern_no_descent ∀n, n%256=39 → n < ((3·((3·((3n+1)/2)+1)/2)+1)/2)/2 propext, Quot.sound
case5c_shortPattern_no_descent ∀n, n%256=71 → 同 (value = 432r+121 > n=256r+71) propext, Quot.sound
case5d_shortPattern_no_descent ∀n, n%256=103 → 同 (value = 432r+175 > n=256r+103) propext, Quot.sound
case5_subcases_39_71_103_require_deeper_subdivision 上 3 sub-cases OR (総合) propext, Quot.sound
verify_n39_short_pattern n=39 (r=0): 4 step 後 value = 67 0 (axiom-free)
verify_n71_short_pattern n=71 (r=0): 4 step 後 value = 121 0 (axiom-free)
verify_n103_short_pattern n=103 (r=0): 4 step 後 value = 175 0 (axiom-free)

Total theorems

7

axiom-free base

Numerical (n=39/71/103)

3

完全 axiom-free (0 axioms)

General (∀n mod-class)

4

[propext, Quot.sound] のみ

sorry

0

/ Classical.choice なし

Concrete trajectory (n%256=39 example)

// case5a の 短 pattern が step 4 で 破綻する 理由

Rei step624 の case5a_lt (n%256=7) は 4 odd steps を 経て value = (81n + T) / 2^7 = (81n + T) / 128 で descent 証明:

-- step624 case5a: n%256=7, 4 odd + 7 even, factor 81/128 ≈ 0.63
(3*((3*((3*((3*n+1)/2)+1)/2)+1)/4)+1)/8 < n

Step 3 で (3*t2+1)/4 = v₂ ≥ 2、 step 4 で (3*t3+1)/8 = v₂ ≥ 3 を 要求。 これは n%256=7 の specific mod class で だけ 成立。

n%256=39 (n = 256r+39) では:

step 1: (3·(256r+39)+1)/2 = 384r+59   (odd)
step 2: (3·(384r+59)+1)/2 = 576r+89   (odd)
step 3: (3·(576r+89)+1)/2 = 864r+134  (v₂ of 3·t3+1 = 1、 NOT ≥ 2)
step 4: 864r+134 / 2 = 432r+67        (v₂=1 の 単純 halve)

比較: 432r+67 vs n=256r+39 → 差 = 176r+28 > 0 → value > n

= case5a pattern の step 3-4 で 要求される v₂ ≥ 2 が 満たされない、 かつ 短 pattern の 結果 value が n を 上回る。 深い n%512 / n%1024 subdivision が 必要。

Chang paradigm 18 refined witness layer extension

// digit-sum / Hamming weight の 更 具体化

Rei は 既 STEP 1310 で Chang paradigm 18 (Digit-sum / Hamming weight: E[hw] < 0 は expectation、 deterministic ではない) の refined witness として step624 の trailingOnes deterministic descent (THE_THEOREM + gk1-gk10) を retrofit annotate 済み (Chang/Retrofits/TrailingOnesDigitSum.lean)。

本 STEP は Chang paradigm 18 の refined witness を 更に 具体化:

「digit-sum aspect は deterministic に処理できるが、 Case 5 sub-cases n%256 = 39/71/103 の 具体 mod class では case5a の 短 clean pattern を 適用できない = 深い subdivision が要る」

= Chang paradigm 18 「digit-sum は tool にならない」 の 別 angle からの refined evidence。

相補 pair: STEP 1935 D-FUMT₈ NEITHER semantic layer (rei-aios-4b)

// double-tab arc 相補 pair 形成

同日 2026-09-10 に rei-aios-4b tab が STEP 1935 Cases58NeitherFormalization.lean (commit f4ad0e47b) を land、 NEITHER semantic layer として 「orbit descent 保証 (TRUE) or 反例 (FALSE) の 二値 分離 拒否」 を wallDescentState : Fin 8 = 2 (NEITHER) encoding + self-dual 性 (「未確定 の 否定 も 未確定」) を axiom-free formal 明示。

Layer Tab / STEP 実装
Witness layer (wall の 精密記述) rei-aios-28 / STEP 1933 本 file (Cases58WallRefinement.lean)
Semantic layer (NEITHER encoding) rei-aios-4b / STEP 1935 Cases58NeitherFormalization.lean

Overlap なし、 直交構造 = Chang paradigm 18 2-layer defense (「short pattern で 解けない witness」 + 「解けない state を NEITHER formal semantic として保持」)。

Honest scope (super critical)

Rei は Cases 5-8 に progress していない
  • 本 STEP の theorem 群 は 「case5a の 短 pattern で 3 odd + 1 even (v₂=1) を適用すると value が n を下回らない」 の explicit 記述のみ。
  • これは Cases 5-8 の 未解決状態を 精密化する negative witness であって、 Cases 5-8 の progress ではない。
  • Cases 5-8 の 一般 解決 は 依然 未解決 (Rei の 本質的 wall)。
  • 「Rei は Case 5 sub-cases に descent proof を追加した」 系 claim 絶対禁止 (実際は 「descent NOT achieved by short pattern」 witness)。
  • 「Rei は Cases 5-8 wall を 越えた」 系 claim 絶対禁止。
  • 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) = 学術的 breakthrough ではない。

Extension roadmap (未実装、 藤本さん explicit 判断 candidates)

Attribution

Related