BACKLOG #6 Tier 2
Rei-Solver evolution arc (v0.1 → v0.4) + 万能 TM 外 3/3 全経路 operational
1. なぜ backlog に入っていたか
Rei-Solver は 2026-07-31 藤本さん chat-Claude 6-msg で kairo processor design philosophy 経由で発想 → 08-01 spike で v0.1 (single Z3 engine)、 04 日間で v0.4 まで急速拡張 (6 engine + 4 原則 + 万能 TM 外 3/3 全経路)。 既存の /tools/rei-solver/ は detailed spec + technical documentation 系 site page。
但し 5 日間 arc の evolution timeline + memory-preservation focus + 万能 TM 外 3 経路の相互関係 + verify_with_mathlib v0.4 R1 の Rei stack 自己 verify pipeline 完成 の意味 は memory + CLAUDE.md のみで参照。 STEP 1297 で dedicated backlog site page 化 = Tier 2 top-5 の 1 番目。
本 page は「新しい成果」 ではない。 2026-07-31 → 08-04 の 5 日間 arc 実装済成果を集約 memory-preservation site 反映。 詳細 spec + technical documentation は既存 /tools/rei-solver/ 参照。
2. 4 原則 (SPEC.md 冒頭、 arc 全体で不変)
| # | 原則 | 内容 |
|---|---|---|
| 1 | 実装しない、包む | SAT / SMT / 定理証明 / 数値計算の中核を自前で書かない。 数十年の検証実績があるエンジンを呼ぶ。 Rei の価値は「どの道具に何を投げるかの判断 + 入力の組み立て + 結果の解釈」 |
| 2 | 全てのツールは非同期ジョブ | Z3 は数 ms、 DFT は数時間 = 最初から submit → poll 統一 (軽い engine に合わせない) |
| 3 | 実行前に同期検証する | 「ソルバは入力を疑わない」 = LLM が入力組み立てる以上、 唯一の防御線。 solver_validate は solver_submit 内部でも走る |
| 4 | 保証の種類を必ず返す (assurance taxonomy) | 全結果に assurance field: proof (機械証明) / witness (第三者独立検算可) / numeric (離散化誤差依存) / heuristic (未証明近似) |
3. 5 日間 evolution timeline (2026-07-31 → 08-04)
| Date | Version | Milestone | Key add |
|---|---|---|---|
| 2026-07-31 | — | kairo processor design philosophy 6-msg (chat-Claude) | 「回路 = 検算」 spec 起源、 「万能 TM 外」 concept 導入 |
| 2026-08-01 | v0.1 | Spike (single Z3 engine) | 4 原則 + 基本 op (solver_validate + solver_submit + solver_poll) + Z3 engine |
| 2026-08-01 | v0.1 + | B-16R Prototype + Rei-Solver bridge | TypeScript bridge (experiments/rei-solver/bridge/reiSolverBridge.ts) 追加 |
| 2026-08-02 | v0.2 | Lean 4 + mathlib engine 追加 | verify_with_mathlib op、 Rei env で 2/2 mathlib golden + 7/7 lean4 PASS |
| 2026-08-02 | v0.3 | Limit engine (Gold-Putnam + Karp-Lipton) 追加 | 3 op (compute_limit + decide_halting + advice_query) × 6 golden PASS = 万能 TM 外 2 経路 (B/C) cover |
| 2026-08-04 | v0.4 R1 | verify_with_mathlib allowedImportPrefixes option 追加 | project-scoped namespace (CollatzRei.*) 許可 = Rei stack 自己 verify pipeline 完成 (`data/lean4-mathlib/CollatzRei/` 100+ axiom-free theorem を直接 verify 可能) |
| 2026-08-04 | v0.4 R2 | QRNG engine (NIST Beacon v2) 追加 | 1 op (sample_certified_random) × 1 golden PASS = 万能 TM 外 経路 A cover → 3/3 全経路 operational |
4. 6 engine 現状 (v0.4 時点)
| Engine | Version | Purpose | Assurance types |
|---|---|---|---|
lean4 | lean --version 依存 | Lean 4 + mathlib 定理証明 + verify_with_mathlib (v0.4 R1 で allowedImportPrefixes 追加) | proof / witness / heuristic (sorry 検出時) |
limit | 0.1 (Gold-Putnam 1965 + Karp-Lipton 1980) | 極限計算 (compute_limit) / 停止判定近似 (decide_halting) / non-uniform advice (advice_query) | witness (経路 B/C) |
pysat | python-sat | SAT solver | proof (unsat) / witness (sat model) |
qrng | 0.1 | NIST Beacon v2 authenticated randomness (RSA signed) | witness (signed record independently verifiable、 経路 A) |
sympy | sp.__version__ | symbolic mathematics | proof (identity) / numeric |
z3 | z3.get_version_string() | SMT solver | proof (unsat) / witness (sat model) |
5. ★★★ 万能 TM 外 3/3 全経路 operational (v0.3 → v0.4 R2 で達成)
藤本さん 2026-08-02 session 「層3」 議論 (chat Claude 提示) から派生の 4 分解 concept。 万能チューリング機械 (Universal TM) は物理宇宙内で実現可能な計算モデルの「上限」 だが、 その外に触れる 4 経路 がある。 うち 3 経路 (無限を要求しない) が operational。
2026-08-04 v0.4 R2 で 3/3 全経路 operational 達成。 60 年前既知の教科書事項の Rei-Solver 統合。 novel algorithm ではない、 Rei 独自の貢献は assurance taxonomy 内での位置付け提供のみ。
| 経路 | 実装 | Engine | Base theory | 実装 date |
|---|---|---|---|---|
| 経路 A 計算不能系列生成 | sample_certified_random = NIST Beacon v2 authenticated randomness | qrng | NIST SP 800-90B (量子・カオス系 physical entropy + RSA signed) | 2026-08-04 (v0.4 R2) |
| 経路 B 一様性を捨てる | advice_query = P/poly の operational demonstrate | limit | Karp-Lipton 1980 (non-uniform advice) | 2026-08-02 (v0.3) |
| 経路 C 停止判定を捨てる | compute_limit + decide_halting = 極限計算 | limit | Gold-Putnam 1965 (limit computation) | 2026-08-02 (v0.3) |
| 経路 D 無限を要求する | 物理的に閉じているため実装不可 | — | Bekenstein 限界 / MH 時空 / 質量インフレーション | 永久 skip |
各経路の意味
- 経路 A: TM は 決定論的、 生成 sequence は必ず TM で計算可能 = 真の randomness は TM 外側の物理現象 (量子ゆらぎ) から来る。 NIST Beacon は authenticated randomness を提供、 Rei は「TM 外から witness を持ち込む」 pipeline を確立。
- 経路 B: TM は 一様 algorithm (同じプログラムで全 input サイズ処理) = advice string (input サイズごとに違う non-uniform bit string) を許すと TM 上限を超える言語が decidable になる (P/poly)。 実用的には「lookup table を大きくすれば任意の関数が実現可能」 の formal statement。
- 経路 C: TM は halt/non-halt の 2 値判定 だが halting problem 自身は undecidable = 極限を許すと Gold-Putnam の「limit computable」 class が halting problem を含む言語 class を decidable にする。
- 経路 D: 物理的に不可能 (Bekenstein 限界 = 有限領域に有限 bit しか入らない、 Malament-Hogarth 時空は observational relativity 内で hyper-computation 可能だが物理宇宙は closed で成立しない) = 永久 skip。
6. ★★ v0.4 R1 breakthrough — Rei stack 自己 verify pipeline 完成
2026-08-04 v0.4 R1 で verify_with_mathlib に allowedImportPrefixes payload option 追加 = project-scoped namespace (CollatzRei.*) 許可 → 未指定時は project_root/lakefile.toml の name + [[lean_lib]] + [[require]] から auto-detect。
意味
これにより Rei stack の data/lean4-mathlib/CollatzRei/ (147+ axiom-free theorem) を Rei-Solver 経由で直接 verify 可能。 従来は Mathlib.* / Std.* / Aesop.* / Batteries.* のみ import 許可 = Rei-specific theorem (CollatzRei.PhaseC.Dfumt8Binary64Refinement、 CollatzRei.Chang.Retrofits.* 等) は verify 対象外だった。
v0.4 R1 で解消 = Rei stack 自己 verify pipeline 完成。 具体的な verify 対象例:
- Cantor v0.9-b (Paper 26 v3.0)
- Chang 20/29 paradigm retrofit (backlog #2 で反映済)
- Collatz 48 定理 (STEP 614-624)
- ExitLayer arc (memory backlog #6 対象)
- Fermat Paper 176 (F_5-F_11 v_2(ω))
- Paper 26 v3.0
numSurvivors_eq_0 - D-FUMT₈ Category arc (backlog #3 で反映済)
- Constructor Theory 5/5 (backlog #7 予定)
7. Honest scope (譲れない線)
(1) 「実装しない、 包む」 原則継承 — Rei-Solver は SAT/SMT/定理証明/数値計算 の中核を自前で書かない。 6 engine 全て external tool (Z3 / python-sat / Lean 4 mathlib / sympy / NIST Beacon / Karp-Lipton framework) の wrap のみ。 novel algorithm 主張 なし。
(2) 万能 TM 外 3/3 は「60 年前既知の教科書事項の Rei-Solver 統合」 — Gold-Putnam 1965 + Karp-Lipton 1980 + NIST Beacon (2013- authenticated randomness) を 4 原則 + assurance taxonomy の統合枠組みに包んだのみ。 Rei 独自の貢献は「assurance taxonomy 内での位置付け提供」 のみ。 「Rei が hyper-computation を実現」 系主張 絶対 不可。
(3) 経路 D 永久 skip — 物理的に閉じている (Bekenstein 限界 + MH 時空の observational relativity 内非成立) ため 実装不可。 「Rei は物理限界を超える」 系主張 絶対 不可。
(4) 数値計算 (OpenMM / PySCF / FEniCSx) 未着手 — SPEC.md で「未着手」 明示、 4 engine は未実装。 assurance=numeric の実運用は現在 sympy 経由の一部のみ。
(5) REPL / v0.3 以降の 「証明修復ループ」 は別 op (repl_step) として設計予定 = v0.4 でも未実装。 lake project 直接 verify (相対 import 大量含む file 群) も v0.3 以降の別 op で対応予定。
(6) 24 test は spec-required golden のみ — engine 追加時の regression + assurance taxonomy conformance + 4 原則遵守 check。 6 engine × 完全 branch coverage ではない = 「動く証明」 レベル。
8. 関連 memory + Rei stack impact
直接 origin memory
reference_kairo_processor_design_philosophy_arc_2026-07-31.md— kairo philosophy origin (chat-Claude 6-msg + spike 5 訂正 + 「回路=検算」 spec)project_session_2026-08-01_full_arc.md— spike + v0.1 initial + B-16R Prototype 4-arc sessionproject_session_2026-08-02_full_arc.md— v0.2 lean4 + v0.3 limit + 層 4 ConstructorTheoryBasic 5-arc sessionreference_computability_layers_taxonomy_2026-08-02.md— 万能 TM 外 4 経路 + 5 層分類 (層 3 = limit computability に対応)project_v04_pending_hardening_candidates_2026-08-02.md— v0.4 pending 集約 (I1-I3 / R1-R3 / 層4 全完了)project_session_2026-08-04_hardening_marathon_12arc.md— v0.4 R1 + R2 + Constructor Theory 4 個 axiom-free 完成 12-arc marathonproject_session_2026-08-04_rei_solver_site_v04_reflection_arc.md— v0.4 site 反映 arc
本 backlog site 反映の origin
feedback_all_research_site_reflection_default.md— 2026-08-06 藤本さん永久 protocolproject_site_backlog_catch_up_pending_2026-08-06.md— Tier 2 top-5 の 1 番目として本 STEP 1297 起動 (Tier 1 完了後の判断)
Honest scope discipline
feedback_world_uniqueness_claim_controllable.md— 「Rei が hyper-computation 実現」 主張禁止feedback_zero_sorry_floor_not_ceiling.md— verify_with_mathlib は sorry 検出時 heuristic 格下げ (proof でなく)feedback_lean_build_verify.md— Rei stack 自己 verify pipeline の operational discipline
Rei stack cross-references
- 既存 /tools/rei-solver/ = detailed spec + technical documentation (本 backlog page と補完関係)
- Constructor Theory 5/5 (backlog #7 予定 = STEP 1298) = 層 4 (Deutsch-Marletto 2015/2025) で Rei-Solver 万能 TM 外 と 直交する物理層 (「何が可能か」 vs 「何が計算可能か」)
- Paper 145 v0.9-c (backlog #1 反映済) = D-FUMT₈ silicon 4-substrate、 verify_with_mathlib で
CollatzRei.PhaseC.Dfumt8Binary64Refinementの 18 axiom-free theorem を直接 verify 可能 - Chang paradigm arc (backlog #2 反映済) =
CollatzRei.Chang.*= verify_with_mathlib で 13 retrofit 63 defs を直接 verify 可能