ETP-t1 v0.1 v0.1 無料継続

Collatz t1 (trailing-ones) 遷移規則の 含意グラフ prototype / Equational Theories Project 縮小版 / 藤本伸樹 / 2026-08-12

GitHub source: github.com/fc0web/etp-t1 (MIT License、 npx tsx main.ts で 30 秒実行可能)

1. 装置の目的

Collatz odd-step f(n) = (3n+1) / 2^ν(3n+1) の τ(n) = trailing 1-bits dynamics 上で、 候補法則 (Lyapunov / bound / modular / etc.) を 経験的に test し、 全 pass 規則 + 経験的含意 edges で 「地図」 を描く 小さな measurement device。

Tao et al. Equational Theories Project (2024-25) の 縮小版 (規模 1/200 以下)。 全 4694 magma equations ではなく、 t1 rewrite 規則の 20 個規模 subspace で 個人 PC で閉じる scale。

★ 目的は Collatz 解決の approach ではない: Lyapunov 候補 V(n) = log₂(n) + β·τ(n) が 有限証拠を同時に満たせない (chat-Claude 曰く 「79% NN wall」) 事実を、 経験的に測定 + 構造化する装置。 装置は 発見器ではなく 計測器 / 難易度測定器 として使う (AlphaEvolve-hard label 系譜、 Silent Visual Verifier v0.1 と 同 product philosophy)。

2. v0.1 実測 findings

odd n ∈ [3, 65535] (32,767 samples) × 19 rules で 30 秒実行:

2.1 経験的 全 pass = 「地図の頂点候補」 9 rules

全て τ≥2 領域の classical + τ=1 部分結果 (Terras 1976 系譜 well-known):

R02: τ(n)≥2 → τ(f(n)) < τ(n)                (well-known)
R03: τ(n)≥2 → τ(f(n)) = τ(n) - 1              (well-known, tight)
R05: τ(n)≥2 → ν(3n+1) = 1                      (well-known)
R06: τ(n)=1 → ν(3n+1) ≥ 2                      (well-known)
R09: f(n) ≤ n·(3/2)^τ(n)                       (naive bound)
R10: τ(n)=1 → f(n) ≤ n                         (即降下)
R16-R18: τ(n)≥4 領域 (R02/R03 の subset)

2.2 ★ Lyapunov 候補 5 件 全滅 = 79% wall 経験的裏付け

RuleDomainPass ratio備考
R11: V = log₂(n) 単純減少全 odd33.4%単純 log₂ は decrease しない
R12: V = log₂(n) - τ(n)全 odd41.7%β=1 も 不足
R13: V = log₂(n) - 2τ(n)全 odd41.7%β=2 でも 同水準
R14: V = log₂(n) - τ(n) を τ≥2 領域限定τ≥2 のみ0%「良い」 領域でさえ 0/16384
R15: V = log₂(n) + τ(n) を τ≥2 領域限定τ≥2 のみ33%符号反転でも 不足

R14 = 0% は 最強 negative signal: τ が確定減少する 「良い」 τ≥2 領域 (τ(f(n)) = τ(n)-1 が 決定的に成立) でさえ、 V = log₂(n) - τ(n) は decrease しない。 V_new - V_old ≈ log₂(3/2) - (-1) = +1.585 = 実は Lyapunov が 1.585 だけ 増加 する 病理的挙動。 これが chat-Claude 「V=log₂(n)+α(t1) では 有限証拠を 同時に 満たせない」 の 直接根拠。

2.3 含意 edges 204 件

「A が 成立する n 全てで B も 成立する」 という 経験的含意を 検出。 但し vacuous case (dom(A) ∩ dom(B) = ∅ で 真空的 true) が 多数含まれ、 実質的な含意 edges は 60-80 件程度と推定。 v0.2 で vacuous filter 予定。

3. Honest scope 6 条 (譲れない線)

  1. Collatz 解決の approach ではない = 全 pass 規則は 全て 既知結果の 再確認 (Terras 1976 以降 well-known)、 未知 discovery ゼロ
  2. log₂ を integer bit-length 近似で実装 = Lyapunov precision が低い、 v0.2 で rational 化 必要
  3. Lean 4 verify 未接続 = v0.2+ で Rei stack の Mathlib 基盤 (3,471 axiom-free theorem) を活用予定
  4. 含意 edges に vacuous case 多数 = 現状 204 件のうち 真の含意は 60-80 件推定、 v0.2 で filter 必須
  5. 「面白いか」 (interestingness) 判定 なし = 藤本さん judgment 必須。 chat-Claude 21 turn debate 到達 「AI ≠ 発見器 = 計測器 / 解析器」 core と 一致
  6. Rei stack novelty ゼロ = 装置骨格の scaffold 実装のみ。 Tao's ETP + AlphaEvolve + FunSearch の 系譜継承、 「Rei-side 独立到達」 主張ゼロ

4. v0.2 candidate (roadmap)

  1. log₂ を exact rational 比較に修正 = Lyapunov test の precision 向上
  2. 含意 edge の vacuous case filter = 「地図」 の 実質的 topology 明確化
  3. 全 pass 規則を Lean 4 axiom-free で verify する pipeline = Rei stack の Mathlib 基盤活用
  4. Modular rules 追加 (τ(n) mod k のパターン、 k=2..16)
  5. 2-step / 3-step 遷移規則追加 = 一歩先の predictive structure 探索
  6. Refutable graph (「A が false になる n では B も false」 逆側含意) 追加

5. Product Transition Judgment

現在 Product Transition Judgment Framework v0.1 の 5 checklist で 0 件該当 = 無料継続:

Checklist item該当
(1) 有機的購入シグナル 3 件以上0 件
(2) サポート負荷 週 1 件以上0 件
(3) regulated 用途 pilot fit未該当
(4) enterprise features 明示要求未該当
(5) 3+ dimension benchmark advantage未該当

判定: 全 5 checklist で 0 件 = 無料継続 (site + GitHub OSS 3-way publication default)。 有料化検討開始は AND で 3 件以上該当時のみ、 v0.1 段階では 該当ゼロ。

6. 関連

直接 downstream:

系譜 (external prior art):

  • Tao et al. Equational Theories Project (2024-25) — 全 4694 magma equations 完全 implication graph、 本 v0.1 は 1/200 縮小版
  • AlphaEvolve (DeepMind 2024) — 進化探索型 発見装置、 「AlphaEvolve-hard」 label 系譜
  • FunSearch (DeepMind 2023-24) — 進化探索、 cap set 突破
  • AM (1977) / HR (2000) / QuickSpec — 予想生成型 古典系
  • Graffiti (Fajtlowicz 1996) → 2026 AI proof — loop-closing 事例

chat-Claude 21 turn debate arc (2026-08-08):