D-FUMT₈ は 単一実装ではない

📋 STEP 1775 corrigendum (2026-09-06)

藤本さん指摘に基づく 訂正 2 点 + d8_verify 現状報告 1 点:

1. 「Belnap 1977 information-order 確定」 は 不正確 — STEP 1772 audit 実測で Verilog は 4-value subset で 28/32 は knowledge order + 4/32 (T×F pair) は classical Boolean pass-through の hybrid。 純粋な info-order ではなく、 「Dfumt8InfoHybrid」 と呼ぶのが正確 (T×F classical carve-out が唯一 audit で構造的に予測できた部分、 情報損失禁止)
2. 「両者意図的 design (defect ではない)」 の scope 訂正 — 4-value subset の 12 差分 (T×B, F×N, B×N の 3 pair) には 適用可 (Ginsberg-Fitting bilattice の 2 順序 対応)。 8-value 拡張領域の 66/104 差分 (∞/〇/～/⟲ 関連) は 未診断、 「意図的 design」 と 断定するには 追加 audit 必要 (現状 「両者意図的」 と 記録すると 未来 の 真の defect 探索を 止める 側 に 働く risk)
3. d8_verify 現状 は cross-implementation drift を 検出しない — 詳細 は 下記 「d8_verify 現状報告」 section

3 実装名候補: Dfumt8Truth (seven-logic.ts) / Dfumt8InfoHybrid (Verilog + Lean 4) / (将来) Dfumt8InfoPure (純粋 Belnap knowledge order、 未実装、 学術 reference 用)

TL;DR (STEP 1775 訂正後)

Rei 内 に 「D-FUMT₈」 と 呼ばれる 実装が 2 つ 並存 しており、 136 entry 中 78 差分 (57%) で 別の代数を 実装している。 4-value subset の 12 差分は 両者 意図的 design (Ginsberg-Fitting bilattice の 2 順序 対応)、 8-value 拡張領域の 66 差分は 未診断。 単一 名前 「D-FUMT₈」 で 参照する 過去 STEP claim は 「どちらの 代数を 指すか」 を 明示していない (naming discipline gap)。

Route C 採択: 2 実装 併存 + 別名 discipline (code 変更なし、 documentation only)。 未来 の 発話・記憶・論文で 「D-FUMT₈」 単独名 を 使う時は どちらの 代数か 明示 必須。

2 つの実装 (両方 意図的 design)

優先順位（情報量の低い値が吸収する）:
  〇 < ⊥ < N < ∞ < ～ < B < ⟲ < ⊤

⊤ は AND の単位元（⊤ ∧ x = x）
⊥ は AND の零元  （⊥ ∧ x = ⊥）（ただし〇が最優先）

On the {FALSE, TRUE, BOTH, NEITHER} sub-lattice (Belnap), we use:
  NEITHER ≼ FALSE ≼ BOTH ;  NEITHER ≼ TRUE ≼ BOTH
  AND = greatest lower bound, OR = least upper bound.

両者は Fitting 1990 bilattice framework の 2 軸 のうち 各 1 つ を 別々に 選択 した状態 (どちらも bilattice full 実装ではない、 特に Verilog は T×F carve-out で 純粋 knowledge order でもない)。 「classical truth を 問う」 (Dfumt8Truth) と 「information content + T×F classical pass-through」 (Dfumt8InfoHybrid) の 別の 問いに 対する 別の 実装。

d8_verify 現状報告 (STEP 1775 追加、 藤本さん要求)

STEP 1397 (2026-08-23) で 実装された d8_verify は 6 claim (self-*-fixpoint 3 種 + demorgan + idempotent + zero-absorption) を verify するが、 実質は seven-logic.ts 内部の property を self-check しているだけで、 Lean 4 refinement / Verilog dfumt8_alu.v との cross-implementation 比較は 一切していない。

実装確認 (src/mcp/d8-connectors.ts L596-616 checkDemorgan)

function checkDemorgan(): D8VerifyCheck {
  for (const a of EIGHT_VALUES) {
    for (const b of EIGHT_VALUES) {
      const lhs = not(and(a, b));  // ← seven-logic.ts の not, and
      const rhs = or(not(a), not(b));  // ← seven-logic.ts の or, not
      if (lhs !== rhs) failures.push(...);
    }
  }
  // ...
  lean4Reference: LEAN4_REF_DEMORGAN,  // ← 単なる metadata 文字列
}

Lean 4 reference (LEAN4_REF_DEMORGAN 等) は payload の metadata 文字列 であり、 verify logic 内で 実際に Lean 4 file を parse したり Verilog dump と 比較したり する 経路は ゼロ。

結果: 全 6 claim が seven-logic 内で 内部整合するので 常に PASS

• demorgan: seven-logic は 4 値領域で De Morgan 完全成立 → PASS (Verilog は 22/64 破れ、 だが d8_verify は Verilog を 見ない)
• idempotent: seven-logic は 8 値全 idempotent → PASS
• self-*-fixpoint: seven-logic の SELF 定義通り → PASS
• zero-absorption: seven-logic の ZERO row/col 直接参照 → PASS

影響

• 過去 STEP claim 「d8_verify で drift なし 確認済」 は 「seven-logic 内部整合」 の意味であり、 seven-logic vs Verilog+Lean 4 の 78 差分は 検出範囲外
• docstring (L522-523) には 「TS 実装 と Lean 4 定理 hard-code reference の 一致検証」 と 記述されているが、 実装 と 一致していない (「hard-code reference」 の 実 comparison が 未実装)
• chat-Claude 2026-08-23 訂正 (STEP 1397) が 「記憶再生 vs 導出 区別ではない」 と 目的絞込 したが、 「Lean 4 定理 との drift 検出」 部分も 未実装 と 明確化 必要

対応

• 本 STEP (1775) は 現状 documentation-only 報告 のみ (docstring 訂正は seven-logic.ts と Lean 4 file の header で 別途 完了)
• 実装拡張 (真の cross-impl drift detector) は STEP 1776+ candidate、 藤本さん判断 待ち
• 拡張案: (a) Verilog table dump (`data/tabs/rei-aios-f4/d8-algebra-corrigendum/scratch/dump_verilog_tables.py`) を CI で 実行し、 seven-logic vs Verilog の diff を verify claim として 追加 / (b) Lean 4 theorem 文本 (aluAnd_refines / aluOr_refines) を parse して expected value を 抽出 (v0.3、 STEP 1397 で defer 済) / (c) 4-value subset 12/32 vs 8-value 拡張 66/104 の 差分 分類 を verify output に 含める

差分 数値 (frozen、 STEP 1775 訂正済)

136 entry (AND 64 + OR 64 + NOT 8) 中 78 差分 (57.4%) — audit-results/01_defect-report.md + ROUTE_D_AUDIT.md 実測。

4-value subset 差分 example (12 entry のうち 4 個 代表)

T×F carve-out (Verilog 側 hybrid 部分、 4 entry): AND[TRUE][FALSE] = FALSE、 OR[TRUE][FALSE] = TRUE (両方 seven-logic と 一致、 classical Boolean pass-through)。 純粋 knowledge order なら AND[T,F] = NEITHER、 OR[T,F] = BOTH のはず。

代数則 差 (実測)

Note: 「truth-order / info-order」 用語 (Ginsberg / Fitting bilattice) は 精密には 適切でない — bilattice は 同じ台集合上 の 2 束順序 を 要求するが、 seven-logic は 8 値上 束ですらなく、 Verilog は 4 値束 の 直和 (8 値上 の 2 順序 ではない)。 一段弱い記述 「Boolean truth-order」 vs 「Belnap info-order」 を採用。

Route C 決定 (2 algebra 併存 + naming discipline)

なぜ Route (A) (seven-logic → Verilog) 却下

• 342 file が seven-logic を import — blast radius 大
• MCP 16 tool 全体 semantics 変化 — 58 site page + 15+ STEP memory retroactive drift
• seven-logic の design 意図 (classical Boolean) は 意図的、 「合わせる」 の 前提が 崩れる

なぜ Route (B) (Verilog → seven-logic) 却下

• Silicon (Tang Console + Tang Nano 9K + IBM Heron r2) の 実測 fidelity 崩壊
• Paper 145 §B.5.4 unary refinement + §C.9 F.1 binary 64-entry refinement (18 axiom-free theorem) 全 破綻
• Belnap 1977 は 情報論的 canonical、 変更する 学術的 justification なし

Route (C) 採択理由 (STEP 1775 訂正: scope 限定明示)

• 4-value subset 12 差分は 両者 意図的 design (Ginsberg-Fitting bilattice の 2 順序 対応、 STEP 1772 audit で 実測確認)
• 8-value 拡張領域 66 差分は 未診断 — 「意図的 design」 と 断定せず、 STEP 1776+ で 追加 audit 対象 候補
• Fitting bilattice framework 内で 4-value subset のみ 位置づけ可能 (完全 bilattice 実装 は なし)
• Blast radius ゼロ (code 変更なし、 documentation のみ)
• Paper 145 無傷 (Verilog + Lean 4 refinement 側 = Dfumt8InfoHybrid に 依存する 全 claim 保持)
• MCP output も 無傷 (seven-logic 経由 = Dfumt8Truth の 全 tool 保持)

3 実装名候補 (STEP 1775 追加、 藤本さん指摘)

• Dfumt8Truth = seven-logic.ts の 代数 (classical Boolean truth-order + 拡張 4 値 束外)
• Dfumt8InfoHybrid = Verilog + Lean 4 の 代数 (Belnap knowledge order + T×F classical Boolean carve-out + 拡張 4 値 直和)
• (将来 candidate) Dfumt8InfoPure = 純粋 Belnap knowledge order (T×F carve-out なし、 32/32 一致)、 未実装、 学術 reference / 比較用 の 3 実装目 として 検討候補

STEP 1773 で 実施

1. Cross-reference header 追加 (3 files)

• src/axiom-os/seven-logic.ts: 冒頭 に corrigendum block、 「Boolean truth-order edition」 明示、 Verilog 側 cross-ref、 「defect ではない」 明記
• data/verilog/dfumt8_alu.v: 冒頭 に corrigendum block、 「Belnap information-order edition」 明示、 seven-logic 側 cross-ref、 「Paper 145 は Verilog 側 のみ 依存」 明記
• data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean: module doc 冒頭 に corrigendum block 追加、 lake env lean で clean build 確認

2. 命名 discipline 提案 (documentation only)

• seven-logic.ts の 代数 → 「D-FUMT₈ Boolean truth-order」
• Verilog + Lean 4 の 代数 → 「D-FUMT₈ Belnap info-order」
• 未来 の 会話・記憶・論文 で 「D-FUMT₈」 単独名 を 使う時は どちらの 代数か 明示 必須

3. 未実施 (別 STEP candidate、 defer)

• 1774 MCP tool 名前 分割 (d8_apply_boolean / d8_apply_belnap) — breaking change
• 1775 d8_verify 拡張 — cross-implementation drift detector として 拡張
• 1776+ 58 site page の 各 個別 note 追加 — bulk edit
• Fitting bilattice framework の 完全実装 (2 order 同時 保有) — phase 2 candidate
• 15+ STEP memory の 該当箇所 に corrigendum reference 追記 — 「memory grep 時に 認知」 効果、 optional

Honest scope

参照

• 前身 audit: data/tabs/rei-aios-f4/d8-algebra-corrigendum/ (2026-09-04 rei-aios-f4 tab)
• Route decision doc: audit-results/05_route_decision_step1773.md
• Defect report: audit-results/01_defect-report.md
• Blast radius: audit-results/03_blast-radius-scan.md
• Paper 145 影響 audit: audit-results/02_paper145_c9_f1_audit.md
• Reproducibility: audit-results/01_defect-report.md §引用可能な reproducibility
• Belnap 1977: "A Useful Four-Valued Logic", Modern Uses of Multiple-Valued Logic
• Fitting 1990: "Bilattices in Logic Programming", Proceedings of the 20th International Symposium on Multiple-Valued Logic