src/axiom-os/seven-logic.ts の collapse 関数、 および data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean の Dfumt8InfoHybrid に 対する コード変更は 一切 行わない。 Kato 2026 paper (arXiv:2609.11174) の formal work との 整合性 を 明示 mapping し、 未解決 marker (T×F carve-out UNDETERMINED、 collapse axiomatization なし) の resolution 方針 を 二択で 藤本さん judgment に 差し戻す。
主要 finding:
collapse の T→T / F→F preservation で 表面上 satisfies、 但し 「4-value canonical operator (cons/prec/opt/cont) との compatibility」 は 未検証。collapse は 意図的 に 満たさない (INFINITY→NEITHER + ZERO→NEITHER + FLOWING→BOTH + SELF→BOTH の 非単調 many-to-one map)。 これは 「拡張値 3 (∞/〇/～) + SELF⟲」 が Belnap 4-value に truth-order で ordered ではない ため、 monotonicity 定義 自体 が 拡張域 で 意味不明。Dfumt8InfoHybrid の T×F carve-out (4/32 entries、 classical Boolean pass-through) は Kato の cleaner inductive Val4 approach と 対照的、 STEP 1866 (2026-09-07) audit で 意図 = UNDETERMINED と 確定。 Kato-style adopt する か Rei 独自 hybrid design intent を 明文化する か の 二択 は 未 decision。A0 (classical extension): 4-value semantics は 2-value classical logic を extend、 T/F の 挙動 は classical と 一致。
A1 (truth monotonicity): reduction operator ρ が truth order 保存 (ρ(v₁) ≤ₜ ρ(v₂) if v₁ ≤ₜ v₂)。 Correction note: v1 → v2 abstract で 「earlier formulation of A1 demanded knowledge order, refuted by Lean, replaced with truth monotonicity」 と 明記 = Kato 自身 の Lean-driven 訂正 (Remark 5.4 v1 body に discussion 既存)。
4-value system 上の A0 + A1 を 満たす reduction operator は 4 個 canonical operator (cons / prec / opt / cont) で 網羅、 それ以外 は 存在しない。 exhaustiveness 証明 は Lean 4 machine-checked (mathlib heavy dependency)。
Kato 独自 primitive (Y ⋅w N = N / N ⋅w * = Y / etc.、 FDE-inspired transition-specific)、 Rei D-FUMT₈ の Ψ/Φ/Ω operators と 直接対応 operator は 存在しない。 STEP 1993 corrigendum #7 arc の verdict C 根拠 の 一つ (「Kato operators subset of Rei = 不成立」)。
STEP 1866 (2026-09-07) audit で 確定した 通り、 Rei D-FUMT₈ は 単一実装ではなく、 2 代数 併存:
| 代数名 | 実装 file | 4-value 部分 | 8-value 拡張 | Kato との 関係 |
|---|---|---|---|---|
Dfumt8Truth |
src/axiom-os/seven-logic.ts |
100% Belnap FOUR truth order (0/32 mismatch) | 4-value 束 外 (拡張値 が 束構造外、 極大部分束 1 個) | 4-value slice = Kato の Def 2.3 truth order と 順序同型 |
Dfumt8InfoHybrid |
data/verilog/dfumt8_alu.v + data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean |
28/32 Belnap knowledge order + 4/32 T×F classical Boolean carve-out (UNDETERMINED) | 4 値束 直和 + cross-tier "classical wins" rule | knowledge order は Kato bilattice の k-order と mapping 可、 T×F carve-out は Kato に 対応 なし |
// src/axiom-os/seven-logic.ts:313-324
export function collapse(v: EightLogicValue): FourLogicValue {
switch (v) {
case 'TRUE': return 'TRUE'; // classical preserve
case 'FALSE': return 'FALSE'; // classical preserve
case 'BOTH': return 'BOTH'; // identity
case 'NEITHER': return 'NEITHER'; // identity
case 'INFINITY': return 'NEITHER'; // ad-hoc many-to-one
case 'ZERO': return 'NEITHER'; // ad-hoc many-to-one
case 'FLOWING': return 'BOTH'; // ad-hoc many-to-one
case 'SELF': return 'BOTH'; // ad-hoc many-to-one
}
}
特徴: 8-value → 4-value projection、 axiomatic characterization なし、 exhaustiveness 証明 なし、 ∞→NEITHER / 〇→NEITHER / ～→BOTH / ⟲→BOTH の 4 拡張値 の mapping は 意味論 comment のみ で justification (comment: 「情報の損失を伴うが互換性を保つ」)。
Verilog dfumt8_alu.v L109-111 + README L45-46 の stated intent は 「Belnap meet/join」 だが、 実装 は 4/32 entries (T×F pair) で classical Boolean pass-through を 採用。 STEP 1866 audit 結果:
Route C 累積 evidence: STEP 1874 で Region A (T×F 12 diff) UNDETERMINED / Region B (higher tier 14 diff) INTENTIONAL / Region C (cross-tier 52 diff) INTENTIONAL = 78 total diff の 66/66 (85%) が INTENTIONAL 確定、 但し T×F 12 diff は 依然 UNDETERMINED marker preserve。
| Kato 側 | Rei Dfumt8Truth |
Rei Dfumt8InfoHybrid |
gap |
|---|---|---|---|
| A0 (classical extension) T/F は classical と 一致 |
△ partial collapse の T→T / F→F は satisfies。 但し 4-value 内 で operator 側 の classical 対応 は 未検証。 | △ partial T×F carve-out は classical Boolean pass-through で 過剰 満足 (実装 が axiom より 強い)。 | Rei operators (Ψ/Φ/Ω) が A0 の 「classical extension」 sense で 4-value 内 で どう 挙動する か、 Kato Table 1 conjunction と literal 一致 verify は 別 phase。 |
| A1 (truth monotonicity) ρ(v₁) ≤ₜ ρ(v₂) if v₁ ≤ₜ v₂ |
✗ 拡張域 未定義 4-value 内 (T/F/B/N) は identity で trivially satisfies。 拡張値 (∞/〇/～/⟲) が truth-order で ordered ではない ため、 A1 の 前提 (v₁ ≤ₜ v₂) 自体 が 拡張域 で 意味不明。 | ? 要検証 Dfumt8InfoHybrid は knowledge order 主体 で 定義、 truth order 定義 と の 関係 は Ginsberg-Fitting bilattice 2 順序 で 区別。 A1 (truth monotonicity) を hybrid で どう 解釈 するか は 未検討。 | 両実装 とも 「truth order 拡張域 未定義」 問題 を 抱える。 Kato-style adopt する場合、 拡張域 に truth order を 何らか定義 する か、 Kato の scope 外 に defer する か の 判断 が 必要。 |
| Thm 5.5 (exhaustiveness) 4-value 上 の A0+A1 満たす reduction operator は cons/prec/opt/cont 4 個 のみ |
✗ direction 違い Kato Thm 5.5 は 4-value 内 operator の 網羅、 Rei collapse は 8→4 projection、 direction が 異なる。 Kato 定理 は Rei collapse を 「Kato canonical operator の 合成 で 表現可能か」 を 未答。 | ✗ scope 外 Dfumt8InfoHybrid は k-order 主体、 t-order 内 reduction operator 対応 は 直接 mapping 不能。 | Rei 8→4 collapse の 「Kato canonical operator (cons/prec/opt/cont) 合成 で 表現可能」 verify or 「Kato scope 外 の new reduction operator」 明示 の どちらか が 必要。 |
| ⋅w transition-warrant connective Kato Table 2、 game-theoretic reachability specific |
— 対応 なし Rei Ψ/Φ/Ω は 8-value operate、 Kato ⋅w は 4-value transition-specific = 対応 operator 不在。 STEP 1993 verdict C 根拠 の 一つ。 | — 対応 なし Dfumt8InfoHybrid は cross-tier "classical wins" rule、 Kato ⋅w の transition semantics と 別軸。 | Kato ⋅w は Kato-specific primitive、 Rei-side に adopt する必要性 は 未検討 (QCW-GMCR domain specific)。 Rei 側 で 対応 operator 定義 する か、 「Rei scope 外」 と 明示 する か。 |
内容: Dfumt8InfoHybrid の T×F carve-out (4/32 entries classical Boolean pass-through) を 削除、 Kato の clean inductive Val4 approach に refactor。 4-value 全 entries を Belnap knowledge order 一貫、 hybrid design 廃止。
Pros: (a) Kato paper の A0 + A1 axiomatic characterization と 直接 alignment、 (b) UNDETERMINED marker resolve (「意図 = clean Belnap」 と 明確化)、 (c) 4-value slice formalization の rigor 到達、 (d) 未来 Rei paper 145 v0.8 で Kato prior art alignment 主張 可能。
Cons: (a) Verilog silicon dfumt8_alu.v (4-substrate verification 済、 Paper 145 F3 CLOSURE) の 実装変更 が 必要 (T×F carve-out は Verilog 側 で 実装、 refactor は Verilog rewrite + Tang Console NEO 再 program + Aer + IBM Heron 再 submit = 大規模 arc)、 (b) 過去 STEP 1264 (Paper 145 F3 CLOSURE) + STEP 1866 (γ 選択 = documentation only) との 一貫性 損失、 (c) 「silicon 慣性 unconscious intentional」 hypothesis が 正しかった 場合、 Kato-style adopt は silicon design intent の 消去 になる、 (d) Route C 累積 evidence (78 diff の 85% INTENTIONAL confirm) と 若干 tension (Region A T×F 12 diff は UNDETERMINED のまま で resolve、 但し Region B/C 66 diff は INTENTIONAL keep)。
Effort estimate: 大 (2-4 weeks、 Verilog rewrite + 4-substrate re-verification + Lean 4 refinement update + Paper 145 v0.8 patch)
内容: Dfumt8InfoHybrid の T×F carve-out を preserve、 「silicon Boolean 慣性 との pragmatic alignment for hardware efficiency」 を 明示 design intent として 文書化。 Kato-style と Rei-hybrid の 2 代数 併存 を 意識的採択 として 記録。
Pros: (a) Verilog silicon + 4-substrate verification (STEP 1264 F3 CLOSURE) の 実装保存、 (b) 過去 arc (STEP 1866 γ 選択、 STEP 1874 Route C) との 一貫性 preserve、 (c) 「hybrid = intentional silicon-aware design」 の 明示化 で UNDETERMINED marker resolve (「意図 = pragmatic hybrid」 と 明確化)、 (d) implementation cost 極小 (documentation update のみ)、 (e) Kato-style vs Rei-hybrid の 2 代数 併存 は 「4-value formalization の 2 track」 として 独立 novel。
Cons: (a) Kato axiomatic rigor 到達 は 部分的 (A0 は 過剰 満足、 A1 は 拡張域 未定義 のまま)、 (b) Rei paper 145 v0.8 で Kato prior art との alignment 主張 は 「hybrid 独自」 として 明示 必要 (「Kato-aligned」 とは 言えない)、 (c) 「silicon 慣性 unconscious bug」 hypothesis が 正しかった 場合、 Option B は bug の post-hoc rationalization risk。
Effort estimate: 小 (2-4 hours、 documentation update のみ、 Verilog + Lean 4 refinement は 現状維持)
Gap 1: Rei collapse function (seven-logic.ts:313-324) は axiomatic characterization なし、 「情報の損失を伴うが互換性を保つ」 という semantic comment のみ で justification。 Kato Def 5.3 A0/A1 相当 の formal axioms を Rei 側 で 定義 する 必要 が emerge。
Gap 2: Rei collapse の exhaustiveness 証明 なし。 「8-value → 4-value projection の 意味論的正当性」 を Kato Thm 5.5 相当 の uniqueness/canonicity theorem で 補強 する 余地 が ある。 但し direction が 異なる (Kato = 4-value 内 operator 網羅、 Rei = 8→4 projection)、 直接 apply は 不能。
Gap 3: 拡張値 4 (∞/〇/～/⟲) を Belnap 4-value に truth-order で 位置付ける order 定義 が Rei 側 で 存在しない。 Kato A1 (truth monotonicity) を collapse に apply する 前提 が 拡張域 で 意味不明。 「拡張値 は Belnap 4-value と truth-order で 比較不能」 と 明示宣言 するか、 何らか の partial order を 定義 するか の 判断 が 必要。
Option α: Rei collapse に Kato-style A0'/A1' axiomatization を 追加 (拡張域 の truth-order 定義 + monotonicity 主張 + exhaustiveness proof sketch)、 seven-logic.ts に axiomatic layer 追加。 Effort: 中 (2-4 days、 Lean 4 formal proof + TS source-level annotation)
Option β: Rei collapse の 「ad-hoc many-to-one projection」 を 意識的 design choice として 明示宣言、 「拡張値 は Kato scope 外 = D-FUMT₈ 独自」 と documentation 明記。 Effort: 小 (2-4 hours、 documentation update のみ)
本 audit の 提案 = defer only。 コード変更 (Verilog、 Lean 4、 TypeScript) は 一切 提案せず、 以下 2 判断 を 藤本さん explicit judgment に 差し戻す:
私 の 私見 (参考、 judgment override 可):
両判断 とも 「急がずゆっくりと」 に 従い、 藤本さん explicit go 待ち。 本 audit で は 判断 material の 提供 のみ、 実 refactor は 別 STEP + 藤本さん explicit direction 待ち。
collapse function の 「Kato canonical operator (cons/prec/opt/cont) 合成 で 表現可能か」 の 実 verify は 未実施 (Option α 選択時 の 別 phase candidate)。dfumt8_alu.v の testbench + FV re-verification は 未実施 (T×F carve-out unconscious bug/intentional 区別 の direct evidence 取得は Option A 選択時 の 別 phase)。src/axiom-os/seven-logic.ts:313-324 — collapse function 実装data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean — Dfumt8InfoHybrid Lean 4 refinement (Paper 145 F3 CLOSURE)data/verilog/dfumt8_alu.v — Verilog ALU (Tang Console NEO silicon)