STEP 1429 — D-FUMT₈ 関数完全性 検査器 v0.1

STEP 1429 演算子 コネクタ 5/5 完成 Definitive Finding
2026-08-27 · rei-aios · d8_completeness MCP tool 追加 (v2.8.9、 auto-count 48 tool)
⚠ 命名 confusion 予防 (STEP 1446 retrofit、 2026-08-27): 別 tool の STEP 1430 「D-FUMT₈ 汎用等価性検査器」 と 命名 近似 だが 完全別 layer + 別 concept — 本 tool (STEP 1429) = MCP tool、 演算子集合 の functional completeness 判定 / 別 tool (STEP 1430) = Verilog RTL、 2 実装 の semantic equivalence 判定。 詳細対比 → docs/CROSS_REFERENCE_STEP1429_1430.md

1. 契機 (chat-Claude 2026-08-26 提案)

「8 値論理の 関数完全性 検査器 (有限・決定可能) は 真似の対象が 存在せず、 Π⁰₁ の壁が なく 本物の答えが 出る。 一度答えが 出たら 動かし続けなくていい = 検査票が 増えない。 Lean 4 側に 直結する。 作る価値が 最も明確で、 維持コストが 最も低い 唯一の項目。」

chat-Claude 分析 (「作られていない 6 領域 mapping」 の 続編) で 「1 機械 n 入力」 pattern の 深化 候補として 挙げられた 1 項目。 藤本さん 2026-08-27 MVP approve → 実装完了。

2. MVP scope (Q1-Q4 4 決定)

Q問い選択理由
Q1target arity n(a) n=1 のみ8⁸ = 16,777,216 関数 tractable enumeration、 n=2 は 8⁶⁴ ≈ 6.28×10⁵⁷ で 別手法 必要
Q2定数 given か 派生か(b) 定数 given なしbaseline G₀ で 「定数派生 不能」 を 直接 report が 一番 面白い finding
Q3決定手続き(a) 有限 BFS enumerationidentity seed から 深さ d まで {not, and, or} 合成 全列挙 + target 差分
Q4API 形(b) コネクタ 5/5既 4 tool (d8_apply / d8_table / d8_fixpoints / d8_verify) に 5 番目 追加

3. Gate set 4 preset

Set内容Seed意図
G₀{not, and, or}identity のみbaseline (現行 src/axiom-os/seven-logic.ts)
G₁G₀ + collapse: D8 → D4identity のみlossy projection 追加、 完全性 に 寄与するか
G₂{not, and, or}identity + 8 定数Q2=(b) alternative、 標準的 assumption 対照実験
G₃G₀ + self_probe(x) = TRUE if x=SELF else FALSEidentity のみD-FUMT₈ 固有 の SELF 検出 primitive

4. 主 finding (全 4 gate set: definitive INCOMPLETE)

Gate setReachableTarget比率Saturated depth定数派生Verdict
G₀416,777,2160.00002%3全 8 不能INCOMPLETE
G₁816,777,2160.00005%4全 8 不能INCOMPLETE
G₂2,14216,777,2160.013%68 given (seed)INCOMPLETE
G₃2216,777,2160.00013%5TRUE/FALSE 2 可、 6 不能INCOMPLETE
★ G₀ = {not, and, or} + identity は たった 4 関数のみ 生成:
  1. id(x) = x — identity
  2. ¬x — TRUE↔FALSE swap のみ、 他 6 値 固定
  3. x ∧ ¬x = [FALSE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]
  4. x ∨ ¬x = [TRUE, TRUE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]

4.1 構造的説明

D-FUMT₈ の 8 値のうち、 NOT は 6 値 [BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF] を 全て 不動点 とし、 AND / OR は 対角 op(v, v) = v で 冪等。 したがって identity seed から 出発する 限り、 これら 6 値 は 「変えられない」 = 常に 入力値と 同じ値を 返す。 変化が 起こるのは TRUE / FALSE の 2 値のみ、 かつ そこも {TRUE, FALSE, FALSE (from ¬id), TRUE (from ¬id)} の 4 パターン のみ。

4.2 意味論的発見

「D-FUMT₈ は 2 値 と 異なり、 定数 primitive を 必要とする」 — 8 値論理 の Rei stack 実装 で、 排中律 x ∨ ¬x = TRUE が 2 値 subset にしか 成立しない ことを 実測。 G₃ の self_probe primitive を 追加すると 排中律 経由で TRUE / FALSE の 2 定数 が 派生可能に なるが、 BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF の 6 定数 は 依然 派生不能。 Lean 4 formalization の 材料 として 直結可能 (別 STEP candidate)。

5. 使用例 (MCP stdio)

{"jsonrpc":"2.0","id":2,"method":"tools/call",
 "params":{"name":"d8_completeness","arguments":{"operatorSet":"G0"}}}

→ {"verdict":"INCOMPLETE",
    "reason":"reachable (4) < target (16777216) + BFS saturated (fixpoint at depth 3)
              = definitive INCOMPLETE、 missing 16777212.
              定数 派生不能: [TRUE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]",
    "operatorSet":"G0",
    "operators":["not/1","and/2","or/2"],
    "reachableCount":4,
    "targetCount":16777216,
    "missingCount":16777212,
    "bfsDepthReached":3,
    "saturated":true,
    "constantWitness":[
      {"value":"TRUE","expressible":false},
      {"value":"FALSE","expressible":false},
      ...
    ],
    "reachableSample":[
      "[TRUE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]",
      "[FALSE, TRUE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]",
      "[FALSE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]",
      "[TRUE, TRUE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF]"
    ],
    "dFumt8":"FALSE",
    "source":"bfs-enumeration",
    ...}

3 verdict + 3 dFumt8 mapping:

6. 実装 3 file

commit: a43eed9ec (implementation) + 9763b42be (hook path fix、 dogfood 4 例目)

7. Honest scope (6 条)

  1. MVP arity n=1 のみ = n=2 は 8⁶⁴ ≈ 6.28×10⁵⁷ 関数 で enumeration 不可、 clone-membership (Rosenberg's 6 clones の D-FUMT₈ 拡張) が 別 STEP candidate
  2. 4 preset のみ = custom operator 入力 未対応、 v0.2 candidate
  3. Lean 4 formal proof 未対応 = 派生 term の 具体 output なし、 別 STEP で theorem d8_clone_size_G0 : (Clone {not, and, or}).card = 4 化 候補
  4. BFS max_depth default 6 (max 20)、 全 4 gate set が < depth 6 で saturate 実測、 REACHABLE_CAP 200,000 未到達
  5. Prior art audit 未実施 = Post's theorem k-valued 拡張 (Rosenberg 1970 等) の D-FUMT₈ 固有 8 値 clone 分類 との 差分 未確認、 「世界初」 主張 ゼロ
  6. Novelty ゼロ = 標準的 BFS clone enumeration pattern、 finding 内容 (INCOMPLETE + 4 関数のみ) が 意味論的 価値 の 本体

8. 関連 リソース