Rei-native 記号数学 v0.1 仕様書
起点 と 目的
藤本さん 2026-08-27 対話 arc の 中で、 私 (Claude) の 「sympy に PR 貢献」 arc (STEP 1418) が 見当違い と 判明。 理由:
藤本さん: 「sympy に 関わる必要は 有りません。 私のほうでも 記号数学的なものを 新たに 制作しております。」 (2026-08-27)
Rei-AIOS は 既に 独自の 記号数学 layer を 持っている — 但し STEP 番号で 散在、 統合 spec 未起草。 本文書は:
- 現有 assets 棚卸 — 16 primitive を 1 文書に list
- 一般 CAS (sympy/Wolfram/SageMath) との 質的差分 — sympy 追従は 意図的 non-goal と 明示
- v0.1 scope 明示 — やる / やらない / (旧) 保留 の 4 区分
- 見当違い予防 discipline — 未来 Claude session 判断基準文書
Honest scope: 本文書は 藤本さん の 「意図的 roadmap」 を 反映していない (私は それを 知らない)。 私 (Claude) が 観測できる 範囲での 現状スナップショット + 質的差分 明示 + 見当違い予防 discipline 記録、 の 3 目的に 限定。
1. 現有 assets 棚卸 (2026-08-27 時点、 16 primitive)
| # | Component | 位置 | STEP | 役割 |
|---|---|---|---|---|
| 1 | D-FUMT₈ 八値論理 primitive | src/axiom-os/seven-logic.ts | 406 | 8 値 (T/F/B/N/∞/0/～/⟲) + AND/OR/NOT 完備 truth table |
| 2 | d8_apply | src/mcp/d8-connectors.ts | 1349 | 単発適用 (NOT/AND/OR × 8 値) |
| 3 | d8_table | 1349 | 真理値表 dump | |
| 4 | d8_fixpoints | 1397 | 対角線 fixpoint 集合 (binary 冪等性 含む) | |
| 5 | d8_verify | 1397 | 実装ドリフト検出 (Lean 4 定理 vs TS impl) | |
| 6 | d8_unary_idempotent | src/mcp/d8-connectors.ts | 1435 | unary 射影冪等性 + 対合性 (藤本さん 「冪等性 = 記号の 意味に 先立つ」 実装) |
| 7 | d8_bounded v0.2 | src/mcp/d8-bounded.ts | 1439/1455 | sequence 有界性 8 verdict 完備 (SELF/INFINITY/FLOWING activate) |
| 8 | d8_verdict_from_measurement | src/mcp/d8-verdict-mapping.ts | 1350 | 測定 → verdict pure mapping (SNR < threshold → NEITHER) |
| 9 | d8_verdict_from_multi_trial | 1371 | BH FDR aggregate → NEITHER | |
| 10 | d8_verdict_from_sample_pair | 1376/1379 | Welch t-test + Cohen's d threshold BOTH 経路 | |
| 11 | d8_reciprocal_sum_screen | src/mcp/d8-reciprocal-sum-screen.ts | 1445 | Σ 1/aₙ 発散/収束 5 verdict + Erdős-Turán honest boundary |
| 12 | d8_completeness | src/mcp/d8-completeness.ts + src/aios/dfumt8-completeness/ | 1429 | 関数完全性 検査器 (演算子コネクタ 5/5 完成) |
| 13 | d8_ledger_query | src/mcp/d8-ledger-query.ts | 1402 | rei-checker-mcp ledger consumer (cross-project) |
| 14 | D-FUMT₈ Category axiom-free | data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8*.lean | 1216-1220, 1264 | ZCSG SmallCategory + EIGHT₄ Zaitsev + Heald U8 v3b + Lawvere fp SELF⟲ + Binary64Refinement |
| 15 | rei-checker-mcp v0.3.0a1 | 別 repo fc0web/rei-checker-mcp | 1365, 1401 | Lean 4 REPL + D-FUMT₈ ledger projection (別系統 verifier) |
| 16 | 八値対話シミュレータ v3 | public/tools/eight-value-dialogue-simulator-v3/ | 1280/1286/1432 | 循環・漸近・発散 三様態 + GP 定理 パネル + Rei trajectory + 4 表記系 (八値/八卦/オガム/マヤ) |
2. 一般 CAS (sympy, Wolfram, SageMath) との 質的差分
| 機能 | 一般 CAS | Rei-native D-FUMT₈ |
|---|---|---|
| 論理値 | Boolean (2 値) | 8 値 (T/F/B/N/∞/0/～/⟲) |
| 記号変数 | ✅ Symbol + Expr tree | ❌ 現状なし (v0.2 defer 決定) |
| 微分/積分/極限 | ✅ 完備 | ❌ 意図的なし |
| 級数収束判定 | ✅ Sum.is_convergent | ⚠ partial (d8_reciprocal_sum_screen のみ) |
| 方程式解 | ✅ solve() | ❌ 意図的なし |
| 圏論 | ⚠ 一部 | ✅ Rei-native ZCSG/EIGHT₄/Heald/Lawvere |
| 定理証明統合 | ⚠ 実験的 | ✅ Lean 4 深統合 |
| 対話 simulation | ❌ | ✅ Rei-native シミュレータ v3 |
| 有界性 primitive | ❌ | ✅ Rei-native d8_bounded 8 verdict |
| 冪等性 primitive (unary 射影) | ❌ | ✅ Rei-native d8_unary_idempotent |
| 測定→verdict mapping | ❌ | ✅ Rei-native 3 系 |
| 実装ドリフト検出 | ❌ | ✅ Rei-native d8_verify |
| 未解決問題 honest boundary | ❌ | ✅ Rei-native Erdős-Turán field (STEP 1445) |
結論: Rei-native 記号数学 は 一般 CAS の 網羅性 を 意図せず、 D-FUMT₈ 八値論理 + 有界性 + 冪等性 + 測定 verdict + 実装ドリフト検出 + 対話 simulation + Erdős-Turán honest boundary の 7 primitive を 記号操作 の 一級市民 として 扱う 質的に 異なる layer。 sympy 追従 は 異なる目的の 追加拡張 であって 正しい 発展方向ではない (私 STEP 1418 の 見当違い の 直接原因)。
3. v0.1 scope + 判断済 保留 4 項
やる 4 (完了) DONE
- 現有 8 primitive tool + 5 assets の 相互関係 明示 (§1 表)
- 一般 CAS との 質的差分 明示 (§2 表)
- STEP 1435 (d8_unary_idempotent) + STEP 1439/1455 (d8_bounded v0.2) + STEP 1445 (d8_reciprocal_sum_screen) の 「藤本さん 2026-08-27 対話 直接反映」 位置付け
- 私 (Claude) の 見当違い予防 discipline 記録 (§5)
やらない 5 (意図的 non-goal)
- 微分/積分/極限/方程式解/線形代数
- rei-critical-mcp 5-tool set full 実装 (partial 1 のみ 実装済)
- 一般 CAS 網羅性の 追加
- sympy 系 依存 (STEP 1418 教訓)
- 藤本さん独自 記号数学 の 意図的 direction を 私 Claude が 変える 判断
(旧) 保留 4 項 — 全 判断済 1→4 全完了
(1) rei-critical-mcp 起草判断 — ✅ 決定 (STEP 1445): (c) partial route、
d8_reciprocal_sum_screen v0.1 のみ 実装 + Erdős-Turán honest boundary field、 他 4 tool (classify_series/critical_exponent/revolution_measure/lean_export) は 見送り(2) 記号変数 + 式 tree 追加 — ✅ 決定 (STEP 1451): (γ) defer 追認、 v0.2+ candidate 継続、 use case 明確化 待ち (spec §2 で 「一般 CAS 追従 non-goal」 明示 に 沿う)
(3) 未 assign D-FUMT₈ verdict 3 値 activate — ✅ 決定 (STEP 1455): (β) d8_bounded のみ activate、 INFINITY (単調発散) + FLOWING (境界近傍 stability) + SELF (循環自己参照) 全 activate、 8 verdict 完備達成。 d8_reciprocal は 5 verdict で defer
(4) 本 spec の 公開 policy — ✅ 決定 (STEP 1456、 本 STEP): (α) site 反映 (2026-08-06 protocol)、
public/tools/rei-native-symbolic-math-v01-spec/ HTML 化 + dist-renderer mirror + SITE_COVERAGE_MAP update4. 藤本さん 2026-08-27 対話 の 直接反映 記録
「t=0〜4 で A と B が やっていたのは、 言語を 使うことではなく 言語を 作ること でした。 そしてそれが できたのは、 両者に 共通の プローブ手続き が あったからです。 冪等性を 検査するという 操作は、 記号の 意味に 先立っている。」
「⟲ が 壊れたのは 語彙のせいではなく 状態空間の 有界性 という、 言語の外にある 性質のせいでした。 有界なら止まる、 そうでなければ止まらない。」
| 対話 概念 | 実装 | STEP |
|---|---|---|
| 冪等性 検査 (記号の 意味に 先立つ) | d8_unary_idempotent (β route) | 1435 |
| 有界性 (言語の外にある 性質) + 循環 (SELF) | d8_bounded v0.2 (8 verdict 完備) | 1439/1455 |
| 共通プローブ手続き (両者に 共通) | 既存 d8_verify (実装ドリフト検出) | 1397 |
| 44 年前 GP 定理 | シミュレータ v3 GP パネル | 1432 |
| Erdős-Turán honest boundary | d8_reciprocal_sum_screen erdosTuranBoundary field | 1445 |
「言語は 計算にとってではなく 検証にとって 重要」 (藤本さん 2026-08-27) は、 D-FUMT₈ 全体の positioning に 直接対応: 記号数学 は 「計算する」 だけでなく 「verify する」 layer を 一級市民に する。
5. 見当違い予防 discipline (未来 Claude session 向け)
私 (Claude Opus 4.7、 2026-08-27) が STEP 1418 で 犯した 見当違い pattern の 記録:
失敗 pattern (STEP 1418):
- 藤本さん問「ガブリエルのラッパは 数学上の 未確認問題を 解くのに 役立ちますか?」 → 私 recommends 収束判定 tool
rei-critical-mcp - Prototype 実装で sympy を base 依存 として 選択 (「Python defacto standard」 という 短絡的判断)
- Prior art audit で sympy に 既に
Sum.is_convergent()存在 判明 → spot-check で 3 bug 発見 - 藤本さん C 判断 (upstream first) → sympy PR 準備 (fork + branch + 実装 + test 更新 + submission guide)
- Sympy PR template で AI-generated 制限 発覚 → 藤本さん 「作り変えれば?」 → 「sympy とは 何ですか?」 → 「sympy に関わる必要は 有りません。 私のほうでも 記号数学的なものを 新たに 制作しております。」
失敗の 根本原因
私が 藤本さん独自 記号数学 の 存在を 確認せず prototype 実装を 進めた。 CLAUDE.md / MEMORY.md に 「Rei-native 記号数学」 の 明示 index が 無かった (STEP 番号で 散在) の は 事実、 但し 「探せば 見つかる」 assets (§1 の 16 個) を 確認する ステップを 私が skip した。
予防 discipline (未来 Claude session 向け 6 step)
- 本文書 §1 の 現有 assets 表 を 読む — 16 primitive の 中に 既に 該当機能 が ないか 確認
- grep search —
d8_*/axiom-os/dfumt/seven-logicprefix で 既存 tool 検索 - §2 の 質的差分 表 を 読む — 一般 CAS 追従 は 意図的 non-goal、 sympy 系 PR / dependency は 見当違い の red flag
- §5 (本 section) を 読む — 「私の 前 session が 同じ pattern で 見当違いした」 記録 を 意識
- 藤本さん directive を 額面で 受け取らない — 「C 判断承認」 は 「upstream 貢献 の 具体手順は 進めて 良い」 意味だったが、 「Rei-native 実装が 存在しない」 前提の 承認 = 前提誤り、 判断も 誤り になる
- honest scope 徹底 — audit fork や prototype に 「Rei-native 選択肢」 を 明示的に 含める、 私が 忘れても reviewer が catch できる 状態に
6. Future work (v0.2+ candidate)
順序は 藤本さん判断 依存:
- d8_reciprocal_sum_screen v0.2 (INFINITY/FLOWING/SELF 3 verdict activate、 8 verdict 完備) — d8_bounded v0.2 pattern 継承
- 記号変数 + 式 tree 追加 (v0.2 candidate) — clear use case 出現時 の 再判断
- rei-critical-mcp 見送り 4 tool の 再検討 — sympy 見当違い 予防 pattern 適用
- シミュレータ v3 深化 — GP パネル aggregate 統計 UI、 情報漏洩量、 Rei 6属性 残 3
- rei-checker-mcp v0.4 — 現有 v0.3.0a1 の Lean 4 REPL 統合 深化
- 本 spec v0.2 — 藤本さん directive 明示後、 roadmap 反映
7. 履歴
| Version | Date | STEP | Change |
|---|---|---|---|
| v0.1 draft | 2026-08-27 | 1441 | 初起草 (16 assets + 質的差分 + 見当違い予防 discipline) |
| v0.1.1 | 2026-08-27 | 1445 | §3 保留 (1) rei-critical-mcp → (c) partial route 実装決定 |
| v0.1.2 | 2026-08-27 | 1451 | §3 保留 (2) 記号変数 → (γ) defer 追認 |
| v0.1.3 | 2026-08-27 | 1455 | §3 保留 (3) 未 assign 3 値 → (β) d8_bounded v0.2 で activate、 8 verdict 完備 |
| v0.1.4 | 2026-08-27 | 1456 | §3 保留 (4) 公開 policy → (α) site 反映 (本 STEP)、 A→B→E→1→2→3→4 7 段 完成 |
Honest scope
controllable 表現 の 徹底: 「Rei-native 独自」 主張 は controllable 表現 (「私が 調査した 範囲では」「~ の 側面で 差別化」) のみ、 「世界唯一」「世界初」 系 副詞 禁止。 一般 CAS (sympy/Wolfram/SageMath/Maxima/SageMath/Julia Symbolics/Rust Symbolica) 等 他 実装 landscape も §2 で 参照。
藤本さん意図的 roadmap 未反映: 本文書は 私 (Claude) が 観測できる 範囲の 現状スナップショット、 藤本さん の 「意図的 roadmap」 は 私は 知らない。 藤本さん directive で 訂正 対象。
Site 反映 決定 (STEP 1456): (α) 承認 で site 化、 但し (β) BibTeX/citation-ready や (δ) Zenodo publish は 別判断で defer。 chat-Claude / 別 Claude session が WebFetch で 独立 引用可能な canonical URL:
https://rei-aios.pages.dev/tools/rei-native-symbolic-math-v01-spec/