Silent Visual Verifier v0.2 — D-FUMT₈ ALU × Verilog × Lean 4 refinement

STEP 1308 (v0.1 Collatz orbit の拡張、 Verilog implementation × Lean 4 axiom-free refinement 対応視覚化) / 藤本伸樹 / 2026-08-08

Interactive verifier

op と入力 a, b を選択 → dfumt8_alu.v の case 分岐で決定的計算 → 結果を D-FUMT₈ 8 値で表示 → STEP 1264 Lean 4 refinement (aluAnd_refines / aluOr_refines) と一致するかの verified marker (Belnap 16 entries + cross-tier 32 entries は Lean 4 axiom-free で verify 済 = ✓)。

op: a = b =

Full 8×8 truth table (op で切替)

緑 outline = Belnap 4-value sub-lattice (16 entries) / 橙 dashed outline = higher tier {ZERO, FLOWING, SELF, INFINITY} (16 entries) / 灰 dotted outline = cross-tier (32 entries)。全 cell で dfumt8_alu.v Verilog 実装値 = Lean 4 refinement 予想値 (STEP 1264 aluAnd_refines / aluOr_refines axiom-free で一致 verify 済)。 hover で座標 highlight。

D-FUMT₈ 8 値 legend

TRUE (⊤) FALSE (⊥) BOTH (⊤⊥) NEITHER (～) INFINITY (∞) ZERO (〇) FLOWING (～→) SELF (⟲)

Reference (data/verilog/dfumt8_alu.v excerpt)

-- select an op + operands above and press verify to see the matching Verilog case --

Rei stack backend (「床」 verification layer)

Verilog source: data/verilog/dfumt8_alu.v (~200 行、 200-entry lookup table for AND/OR/OMEGA/PHI/PSI/NOT/XOR/RESET/NOP)
Lean 4 refinement: data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean (STEP 1264、 Paper 145 v0.9-c F3/§C.9 F.1 CLOSURE)
Axiom profile: 18 theorem 中 16 完全 zero-axiom (「does not depend on any axioms」) + 2 [propext] のみ = Mathlib base [propext, Classical.choice, Quot.sound] より更に強い状態、 sorryAx / native_decide / user axiom 全 0
Substrate cross-verification: Tang Nano 9K + Tang Console 138K + Aer simulator + IBM Heron r2 (fidelity 0.954) の 4 substrate 経由 (Paper 145 v0.9-c methodology)
「実装しない、包む」: v0.2 は完全 client-side computation (Verilog table lookup を JavaScript で reproduce)、 Rei-Solver v0.4 backend は未接続。 SaaS integration は v0.4 candidate

Concept + roadmap (v0.1 → v0.4)

Version	追加内容	状態
v0.1	Collatz orbit visualizer × D-FUMT₈ 8 値 output (STEP 622-624 「t₁ < 4」 threshold)	✅ deployed
v0.2 (本 page)	Verilog D-FUMT₈ ALU (aluAnd / aluOr) 64-entry truth table × Lean 4 refinement (STEP 1264) 対応視覚化	✅ 本日 deployed
v0.3	PDF/Excel 拡張子対応 (LLM 構造抽出 + Rei-Solver assurance verify pipeline stub)	⏳ 未着手
v0.4	Rei-Solver v0.4 6 engine full integration + Peace API SaaS backend 統合 (STEP 1307 と連携)	⏳ 未着手 (Peace API SaaS Phase 2+ と連動)
v1.0	Production form: general Verilog synthesis + 4-substrate cross-verification + Lean 4 export + assurance taxonomy 出力	⏳ 未着手 (Peace API SaaS Phase 3 と連動)

Honest scope

本 v0.2 は concept demonstrator。 aluAnd / aluOr 64-entry lookup を JavaScript で reproduce (Verilog case 分岐を dictionary literal に移植)、 Yosys 合成 / Verilator 実行 / 実 silicon programming は呼んでいない。
「verified ✓」 marker は STEP 1264 axiom-free proof 由来: aluAnd_refines / aluOr_refines theorem が Lean 4 mathlib base で proven、各 cell の予想値は数学的に確定。 v0.2 client-side computation はそのまま予想値を表示。
D-FUMT₈ 8 値 semantics は藤本さん design choice: Belnap sub-lattice + higher tier + cross-tier rule (classical operand "absorbs" non-classical-tier) は dfumt8_alu.v の documented choice、 alternative encoding 可能。
「4-substrate cross-verification」は Paper 145 v0.9-c methodology 参照: v0.2 では実 substrate 実行 (Tang / Aer / IBM Heron) は呼んでいない、 methodology の existence を明示のみ。
v0.3 / v0.4 / v1.0 は未実装、藤本さん stance shift + Peace API SaaS Phase 2+ progression 後の別 STEP。