Kato Table 1 × D-FUMT₈ core-4 anchor 実験 STEP 2081
2026-09-17 JST · rei-aios-d8 tab · verdict = ANCHOR_CONFIRMED · chat-Claude 事前登録 SEAL preservation · 教科書照合 (Belnap 1977 tradition) であって 独立再現 でも 発見 でも ない
ANCHOR_CONFIRMED
教科書照合 (not 独立再現)
64/64 cells 予測一致
Case 2 rule 対象外
Case 1 self-apply 42 milestone
STEP 2083 corrigendum applied (2026-09-17)
★ STEP 2083 Corrigendum (2026-09-17、 chat-Claude 2 点 訂正 accept): 主 verdict (P1 seven-logic AND ↔ Kato Table 1 の ANCHOR_CONFIRMED、 import 実行 vs verbatim 教科書表 = full grade) は 影響 なし。 但し 以下 2 phrasing を 締める:
- Verilog P2 の evidence grade 訂正: 「独立再導出、 計数 に 裏取り」
← 誤 → 「同一 Verilog 表 text からの regex parse 再計数」。 STEP 1775 の 12/32 は 同 Verilog source から 出た ので、 今回 の regex parse による 12/32 は 独立再導出 では なく 同一ソース の 再計数、 一致は当然、 裏 は 付かない。 昇格路 = Dfumt8Binary64Refinement.lean の aluAnd / aluOr (Paper 145 §C.9 F.1 18 axiom-free theorem 依拠、 Verilog 表 と 別経路) と regex dump 突き合わせ で 2 経路照合 に 昇格 candidate (別 STEP defer)。 加えて casez fallthrough / default / enable / 優先順位 が 絡む 場合 regex parse は 合成後 実挙動 と ずれ得る、 regex は sanity check 止まり。
- 「相互裏取り」 → 「一方向 の 確認」: chat-Claude grade [B] OR は Def. 2.4 「∨ は 真理順序 の join」 から の 機械的 束計算 で 正解 一つ。 seven-logic OR が それ と 一致 は 「seven-logic OR = 真理順序 join」 の 一方向 の 確認 のみ、 chat-Claude 導出 を 裏付ける 向き の 情報 は ほぼ 持たない (不一致 emerge なら 疑うべき は chat-Claude 算術 より seven-logic 側)。 「相互裏取り」 phrasing は 撤回。
訂正詳細:
STEP 2083 corrigendum notepad · corrigendum land = commit `<hash>` (post-land)。
§Ⅰ 起点 と 前提
chat-Claude 2026-09-17 relay: STEP 2078 (Kato prior art 3 点 novelty claim 予防 discipline) 直後 の 「次 の 1 手 (α)」 として、 Kato Table 1 (arXiv:2609.11174v2 §2.2) vs Rei D-FUMT₈ core-4 AND/OR 対照実験 を offer。 事前登録 file (C:/Users/user/Downloads/kato-table1-anchor-preregistration.md) を 藤本さん 経由 relay 受領、 私 (rei-aios-d8) が Rei 側 dump 実行 → §4 判定 → land。
目的: STEP 1775 Route C 判定 「seven-logic = truth-order Belnap / Verilog = Dfumt8InfoHybrid (28/32 knowledge order + 4/32 T×F carve-out)」 に 外部独立アンカー を 付ける sanity check。 一致 で 極大部分束 (Belnap FOUR) 同定 の evidence 追加、 不一致 で 同定 再点検。
§Ⅱ 事前登録 (chat-Claude、 dump 前 に seal)
Evidence grade:
- [A] verbatim: Kato §2.2 Table 1 (AND) + Def. 2.3/2.4 (順序 + NOT)。 Table 1 は Belnap 1977 以来 の 教科書表 そのもの。
- [B] chat-Claude 導出: OR 表 (Kato 論文 に 表記 なし、 Def. 2.4 「∨ は 真理順序 の join」 から 機械導出)。 OR 不一致 emerge 時 は 導出 ミス を 先 に 疑う 判定分岐 embed。
P1 予測: seven-logic core-4 AND = Kato Table 1 と 16/16 一致 (Route C 主張 の 直接検定)、 最優先セル BOTH ∧ NEITHER = FALSE (Kato YN ∧ U = N、 真理順序 meet vs 知識順序 meet の 唯一 「両側非自明」 セル)。
P2 予測: Verilog core-4 は Kato と 12/32 相違、 相違 pair は {T,B} / {F,Ne} / {B,Ne} の 3 組ちょうど (順序付きセル数 = 3 pair × 2 方向 × 2 演算 = 12/32)。 T×F は carve-out が 古典 = 真理順序側 と 一致 で 相違しない。 STEP 1775 実測 「12/32 (37.5%)、 差 は T×B / F×N / B×N の 3 pair」 を Kato 表 経由 で 独立再導出 STEP 1775 の 同 Verilog source table を regex parse で 再計数 (chat-Claude 演繹 側 は Kato 教科書表 経由 の 予測)、 P2 一致 は 「Verilog table text の regex parse が 妥当」 レベル、 独立再導出 では ない (下 §Ⅶ + top corrigendum 参照)。
命名 discipline: Kato の N = FALSE と D-FUMT₈ NEITHER の 文字衝突 予防 で、 NEITHER は 本 page 内 必ず Ne と 書く (裸 N 禁止、 STEP 1773 Route D 規約 継承)。
§Ⅲ Dump 実行 (§5 spec 準拠)
Source commit = 8bb6066da (2026-09-07)、 対象 file:
src/axiom-os/seven-logic.ts L256-266 (AND_TABLE) + L289-299 (OR_TABLE)data/verilog/dfumt8_alu.v L157-173 (BELNAP 4-VALUE SUB-LATTICE case cells)
Script: data/tabs/rei-aios-d8/step-2081-kato-table1-experiment/dump-core4-tables.ts (tsx execution、 seven-logic は import、 Verilog は regex parse、 手打ち転記 なし)。
Output: dump-core4-2026-09-17.txt = 4 sections × 16 rows + 11 comments = 75 lines、 §5 format `# impl=<name> op=<AND|OR>` + <left>,<right>,<result>。 sanity check: Verilog Belnap sub-lattice parse 16/16 cells confirmed。
§Ⅳ 実測 vs 予測 対照
seven-logic core-4 AND (P1 主検定)
Kato Table 1 [A] (Y=T / N=F / YN=B / U=Ne):
| ∧ | T | F | B | Ne |
|---|
| T | T | F | B | Ne |
|---|
| F | F | F | F | F |
|---|
| B | B | F | B | F |
|---|
| Ne | Ne | F | F | Ne |
|---|
Rei seven-logic AND (dump 実測): 全 16 cells 上表 と 一致 ✓。 最優先セル BOTH ∧ NEITHER = FALSE ✓ (真理順序 meet 特徴的挙動 confirmed)。
seven-logic core-4 OR (P1 extension、 grade [B])
Kato §1 [B] chat-Claude 導出 vs Rei seven-logic OR dump 実測: 全 16 cells 一致 ✓。 chat-Claude 導出 (grade [B]) が Rei 実装 側 でも 独立 confirm、 導出 ミス 疑い 発火 なし。
Verilog core-4 (P2 副検定)
Verilog AND 実測 vs Kato AND 差分 (相違 6 cells):
| cell | Kato (期待) | Verilog (実測) | 相違 pair |
|---|
| T,B | B | T | {T,B} |
| F,Ne | F | Ne | {F,Ne} |
| B,T | B | T | {T,B} |
| B,Ne | F | Ne | {B,Ne} |
| Ne,F | F | Ne | {F,Ne} |
| Ne,B | F | Ne | {B,Ne} |
Verilog OR 実測 vs Kato OR 差分 (相違 6 cells): 上表 と 同じ 3 pair × 2 方向 pattern (T,B → T/B, F,Ne → Ne/F, B,T → T/B, B,Ne → T/B, Ne,F → Ne/F, Ne,B → T/B)。
合計 diff = 12/32、 3 pair {T,B}/{F,Ne}/{B,Ne} × 2 方向 × 2 演算 = 予測 exact match ✓。 STEP 1775 実測 の 12/32 (37.5%) が Kato 表 経由 で 独立再導出 完了、 計数 に 裏取り chat-Claude Kato-経由 演繹 予測 と 私 regex parse dump が 一致、 但し 両側 とも STEP 1775 と 同一 Verilog source を 参照 = 同一ソース の 再計数 で 独立再導出 では ない。 昇格路 = Dfumt8Binary64Refinement.lean の aluAnd / aluOr (Paper 145 §C.9 F.1 18 axiom-free theorem 依拠、 Verilog 表 と 別経路) と 突き合わせ で 2 経路照合 に 昇格 candidate (STEP 2083 corrigendum)。
§Ⅴ 判定 (§4 rule 機械適用)
| Check | Result | Detail |
|---|
| P1 seven-logic AND vs Kato §1 [A] | ✅ 16/16 | ANCHOR_CONFIRMED prerequisite |
| P1 extension seven-logic OR vs Kato §1 [B] | ✅ 16/16 | grade [B] 導出 が impl でも 独立 confirm |
| ★ 最優先セル BOTH∧NEITHER (Kato YN∧U=N) | ✅ FALSE | 真理順序 meet vs 知識順序 meet の 唯一 「両側非自明」 セル |
| P2 Verilog core-4 total diffs | ✅ 12/32 | AND 6/16 + OR 6/16、 予測 一致 |
| P2 diff pairs | ✅ 3 pairs | {BOTH,TRUE} / {FALSE,NEITHER} / {BOTH,NEITHER} exact |
Verdict = ANCHOR_CONFIRMED。 chat-Claude 64/64 予測 cells 全 match (seven-logic AND 16 + OR 16 + Verilog AND 16 + OR 16)、 ゼロ 予測外れ。
§Ⅵ §0 「言えないこと」 併記 (obligatory land clause per chat-Claude)
この 実験 で 「言えない」 4 点 (chat-Claude 事前登録 §0 verbatim):
- D-FUMT₈ が Belnap である、 とは 言えない (core-4 が 一致するだけ)。 8-value 拡張 (SELF⟲/∞/○/～) は 別 layer。
- Kato が D-FUMT₈ を 検証した、 とは 言えない (Kato は D-FUMT₈ を 知らない、 独立 に 書き下した Belnap 4-value)。
- これ が 新規 の 知見 である、 とは 言えない。 Kato Table 1 は Belnap 1977 以来 の 教科書表 そのもの であり、 外部アンカー としての 強度 は 「独立再現」 では なく 「教科書照合」。
- 安価 で 反証条件 が 明確 な sanity check であって、 発見 では ない。 STEP 2078 で land した 3 点 規律 の 直後 なので、 この 温度 を 外す と 自己矛盾。
§Ⅶ 意味 と 次 の 1 手
ANCHOR_CONFIRMED の 意味:
- STEP 1775 「seven-logic = truth-order Belnap」 判定 に 外部照合 が 付いた (Rei 内部 self-check だけでなく 独立 論文 の 表 と 一致)。 「極大部分束 = Belnap FOUR」 同定 ミス の 可能性 が 一段 下がる。
STEP 1775 実測 の 12/32 (37.5%) 計数 が Kato 表 経由 で 独立再導出、 計数 自体 に 裏取り STEP 2083 corrigendum 訂正: 同 Verilog source から の regex parse 再計数 で 独立再導出 では ない。 独立再導出 は Lean 4 aluAnd/aluOr 経由 の 2 経路照合 (別 STEP defer) で 昇格。chat-Claude 事前登録 §1 [B] 導出 (OR 表) が Rei impl でも 16/16 confirm、 導出 論理 が 妥当 の 相互裏取り STEP 2083 corrigendum 訂正: seven-logic OR = 真理順序 join の 一方向 の 確認 のみ (chat-Claude Def 2.4 導出 は 束計算 で 正解 一つ、 一致 は seven-logic 側 を 確認 する のみ、 chat-Claude 算術 を 裏付ける 向き は ない)。
ANCHOR_CONFIRMED の 意味 (nothing more):
- Route C 採択 理由 (342 file blast radius + silicon fidelity + Paper 145 §C.9 F.1 18 axiom-free theorem 保護) は 本 実験 と 独立、 Route 変更 に 直結 しない。
- STEP 2078 3 点 novelty claim 予防 rule は 依然 有効 (方法論的 新規性 主張 の Pattern L risk は 未解消、 本 実験 は sanity check layer)。
次 の 1 手 candidate (全 藤本さん judgment 待ち):
- STEP 1775 site page への anchor 追加 note (retro update、 別 STEP defer)
- seven-logic.ts header に anchor confirmation 追記 (retro update、 別 STEP defer)
- Kato repo (github.com/ykato0623/qcw-gmcr-lean) の Lean 4 source-level compare (defer registry (i)、 trigger 依然 未達)
- Rei collapse audit STEP 起票 (defer registry (n))
- Rei Dfumt8InfoHybrid clarity refactor (defer registry (o))
§Ⅷ Case 2 rule self-apply record
Case 2 rule check (per STEP 1977 procedure):
- literal numeric: 「16/16 一致」「12/32 diffs」「3 pairs」「64 cells 予測」= chat-Claude 事前登録 §3 verbatim
- 実装候補 に 公開面 file 含有: YES (本 site page + dist-renderer mirror + SITE_COVERAGE_MAP entry)
- 実測 target と literal 一致: YES (16/16 exact + 12/32 exact + 3 pairs exact)
- 判定 (Step 3 で check 終了): literal と 実測 完全一致 = Case 2 rule 対象外 = 通常 land 自由
Case 1 self-apply
42 milestone (前 STEP 2078 = 41 → 現 STEP 2081 = 42)。
§Ⅸ Failure mode 5 (機械学習用 dataset)
- 「ANCHOR_CONFIRMED = D-FUMT₈ novelty confirmed」 誤読 — §Ⅵ「言えない 4 点」 明示 embed、 「教科書照合」 badge display。 Prevention: 本 page 冒頭 badge に 「教科書照合 (not 独立再現)」 常設。
- Kato Table 1 実装 コピー 誤認 — 実際 は Rei STEP 406 (2026-04-13) + 1006 (2026-04-28) は Kato 2026-09-10 に 完全 先行、 Belnap 1977 traditional formulation の 独立実装。 Prevention: 「Kato prior publish 引用義務 なし but novelty 根拠 にも 使えない」 STEP 2078 rule 継承 明示。
- OR 一致 = grade [A] 昇格 誤認 — chat-Claude derived OR (grade [B]) と Rei impl 一致 は
「導出 論理 相互裏取り」 「seven-logic OR = 真理順序 join の 一方向 の 確認」 (STEP 2083 corrigendum) レベル、 Kato paper 自体 が OR 表 掲載 したわけでは ない。 Prevention: 表 の grade marker preserve、 「grade [B] 導出 が impl で confirm」 と 記述、 「Kato paper 記載」 と 混同 しない、 「相互裏取り」 phrasing 撤回 (chat-Claude 算術 を 裏付ける 向き は ほぼ ない、 不一致 emerge なら 疑うべき は chat-Claude 算術 より seven-logic 側)。
- Verilog 12/32 diff = 実装 bug 誤認 — Verilog は 意図的 Dfumt8InfoHybrid (28/32 knowledge order + 4/32 T×F carve-out)、 seven-logic は 意図的 truth-order。 STEP 1773 Route C 併存 決定 で 両者 意図的 design 明示済、 defect ではない。 Prevention:
「STEP 1775 実測 の 独立再導出」 と 明示 「STEP 1775 と 同 Verilog source から の regex parse 再計数、 独立再導出 では ない、 昇格路 = Lean 4 aluAnd/aluOr 2 経路照合 candidate (STEP 2083 corrigendum)」 と 明示、 「12/32 diff = bug」 誤読 予防。
- Test 2 予測 命中 = chat-Claude 予測 accuracy validate 誤認 — Kato Table 1 = Belnap 1977 教科書表、 STEP 1775 実測 12/32 も 既知、 chat-Claude が これら から 導出 した 予測 が 「一致」 する の は 演繹 の 妥当性 confirm のみ (演繹論理 正確性 evidence)、 「chat-Claude 予測能力 一般 validate」 では ない。 Prevention: 「予測 accuracy 高 = 論理演繹 正確性」 と 「予測能力 一般化」 分離 明示。
§Ⅹ Related STEP + Sources
Sources
- Yukiko Kato, A Four-Valued Graph Model for Conflict Resolution: Core Framework and a Machine-Checked Formalization in Lean 4, arXiv:2609.11174v2 [cs.LO]、 v1 = 2026-09-10 / v2 = 2026-09-11。 Table 1 は §2.2、 Def. 2.3/2.4 も 同節。
- Yukiko Kato, State Definition for Conflict Analysis with Four-valued Logic, arXiv:2207.11733 (上流)
- Lean 開発: github.com/ykato0623/qcw-gmcr-lean
- N.D. Belnap Jr., "A useful four-valued logic" (1977) — Kato Table 1 の 原典 (教科書照合 anchor)