BACKLOG #1
Paper 145 v0.9-c — D-FUMT₈ Silicon with SELF⟲ Logic Primitive: 4-substrate cross-verification + F3 CLOSURE
1. なぜ backlog に入っていたか
Paper 145 は 2026-05-09 の v0.3 initial publish 以降、 6 回 の Zenodo update を経て v0.9-c まで到達している。 但し site 側の反映は STEP 1264 実装時 (2026-07-10) に GitHub-only artifact として commit されたのみで、 dedicated site page は未作成 のまま backlog に入っていた。
2026-08-06 藤本さん 「サイトには研究の全反映」 permanent protocol 導入 (関連 memory 参照) 後、 backlog scope 実測で site 反映率 2.5% (21/839 STEP) 判明。 Tier 1 top-5 段階的 catch up の 1 番目として本 page を新設。
本 page は「新しい成果」 ではない。 STEP 1264 (2026-07-10) 実装済成果を、 site 側に「memory 忘れ対策」 primary purpose で反映した dedicated page。 数学的内容 + Lean 4 axiom profile + IBM Heron r2 fidelity data は全て commit 済で immutable。
2. Paper 145 概要 (v0.9-c 時点)
Title: "First D-FUMT₈ Silicon with SELF⟲ Logic Primitive: Native 8-Valued Hardware Realization with Lean 4 Refinement Proof — v0.8 Phase 4 Quine-McCluskey Simplification + Finding F11 Engineering-Correctable Relaxation Bias on IBM Heron r2"
Status: DRAFT v0.9-c (2026-07-10、 GitHub-only artifact、 Zenodo re-publish deferred to v0.9 bundle including v0.9-a DD when IBM Cloud Qiskit Runtime instance provisioning permits)
Core claim (F1-F3)
- F1 — Verilog RTL implementing D-FUMT₈ 8 値 ALU (10 native op + 3 ancilla decomposition) synthesized on 2 independent Sipeed FPGA silicon families
- F2 — SELF⟲ 演算子 (D-FUMT₈ の 8 番目 primitive、 self-reflexive fixed point marker) を hardware primitive として initial-tier level に含めた first known silicon realization
- F3 — 3-bit encode/decode round-trip law が Verilog ↔ Lean refinement bridge として成立。 v0.9-c で binary 64-entry の deferred artifact も axiom-free closure 完成
3. Four-substrate cross-verification (v0.7 で完成、 v0.8 で継続)
4 substrate で同一 D-FUMT₈ 8 値 semantics が観測。 各 substrate は independent implementation + independent verification chain。
| # | Substrate | 実装 | 検証 evidence | STEP |
|---|---|---|---|---|
| 1a | FPGA silicon (Tang Nano 9K) | Sipeed GW1NR-9C LittleBee1 | User Code 0x00005C27、 37 LUT4 / 0 DFF、 SRAM Program 成功 | 1038-1039 (2026-05-10) |
| 1b | FPGA silicon (Tang Console 138K) | Sipeed GW5AST-138B LittleBee5 | User Code 0x00005C27 (chip-portable、 同 User Code 一致)、 4 LED cycling 3Hz 60 秒 demo | 1029 (2026-05-09) |
| 2 | Qiskit Aer simulator | 8-bit basis encoding on 3 qubits、 10 native ops × 8 inputs each | 96/96 testbench PASS (Phase 1+2 fidelity 1.000 by construction) | 1025-1027 (2026-05-09) |
| 3 | IBM Heron r2 real superconducting qubit hardware | ibm_kingston 156-qubit、 SamplerV2 経由 execute | 144/144 PASS Phase 1+2+3+5 avg fidelity 0.954、 Phase 4 QM v0.8 で 32/32 PASS avg fidelity 0.7302 | 1030-1035 (2026-05-09) + v0.8 (2026-06-03) |
IBM Heron r2 実測 (v0.5 → v0.8 progression)
| Phase | Op set | Circuits | Pass | Avg fidelity | Job ID |
|---|---|---|---|---|---|
| 1 | NOP/NOT/PHI/ADIABATIC (unary native) | 32 | 32/32 | 0.955 | d7v6d9jack5s73bf1re0 |
| 2 | XOR (binary 6-qubit) | 64 | 64/64 | 0.9512 | d7v6kcvmrars73d7qqqg |
| 3 | OMEGA/PSI (ancilla) | 32 | 32/32 | 0.9298 | d7v7cnfmrars73d7rna0 |
| 5 | RESET (measurement, 3 designs) | 16 | 16/16 | 0.9821 | d7v7d9vmrars73d7ro3g |
| 4 (v0.5) | AND/OR (Belnap subset、 per-pair MCX naive) | 32 | 18/32 | 0.3182 | d7va0snmrars73d7um30 (relaxation bias) |
| 4 (v0.8) | AND/OR (Quine-McCluskey minimum-SOP) | 32 | 32/32 | 0.7302 (+41.20 pp) | d8fr2jo7jphs739mn2d0 |
4. STEP 1264 v0.9-c: F3 / §C.9 F.1 CLOSURE — Binary 64-entry Lean 4 refinement
File: data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean (443 行 9 sections)
18 theorem axiom profile 実測 (#print axioms): 16 of 18 = "does not depend on any axioms" (完全 constructive、 zero-axiom) + 2 of 18 = [propext] のみ (aluAnd_consistent_belnapAnd + aluAnd_aluOr_cross_tier_agree)。 sorryAx / native_decide / Classical.choice / Quot.sound 全 0。
STEP 1260 baseline (10 constructive + 1 [propext]) より 更に強い axiom profile。
9 section 構成
- Full 64-entry AND (
aluAnd) — Verilog lines 94-140 literal 転記 (16 Belnap-tier + 16 higher-tier + 32 cross-tier default) - Full 64-entry OR (
aluOr) — 同上 - Nat-level derived (
aluAndBits,aluOrBits) - Refinement theorems (
aluAnd_refines,aluOr_refines) — round-trip strategy で trivial - Structural properties: commutativity (64-case) + idempotence (8-case) + absorb
- Belnap subset consistency (
aluAnd_consistent_belnapAnd) — STEP 1011 既存 16-entry と full 64-entry の 16 classical-tier 一致 - Cross-tier design rule:
aluAnd_cross_tier_classical_wins_{left,right}+ OR analogues (32 entries per op、 Verilog default arm 「classical operand wins」 rule) - Round-trip through bit encoding (
aluAndBits_roundtrip,aluOrBits_roundtrip) - 64-entry decide-verified smoke tests (
aluAnd_table_complete,aluAnd_aluOr_cross_tier_agree)
3 年越し deferred artifact 完成
Paper 145 §B.6.3 が 2026-05 起草時点で明示していた:
§C.9 F.1: "Complete the binary lattice refinement (64-entry table) as a follow-up Lean 4 file." — 本 STEP 1264 でこの deferred artifact が axiom-free closure 完成 (§C.9 F.1 CLOSED、 §C.10 R.4 RESOLVED)。
Build: lake build CollatzRei.PhaseC.Dfumt8Binary64Refinement = 2.1s success (2026-07-10 実測)。
5. Version history + Zenodo DOI
| Version | Date | Zenodo DOI | 主要 update |
|---|---|---|---|
| v0.3 | 2026-05-09 | 10.5281/zenodo.20091185 | Initial publish (3-substrate: FPGA + Aer + Heron r2 Phase 1+2、 fidelity 0.953) |
| v0.6 | 2026-05-10 | 10.5281/zenodo.20192813 (parent) | Tang Nano 9K 4-substrate 拡張 + STEP 1037 corrigendum (Tang Nano 9K は物理 silicon) |
| v0.7 | 2026-05〜06 | Zenodo new-version | 4-substrate cross-verification 完成宣言 |
| v0.8 | 2026-06-03 | 10.5281/zenodo.20521157 | ★ Phase 4 Quine-McCluskey simplification + Finding F11 engineering-correctable relaxation bias (32/32 PASS fidelity 0.7302) |
| v0.9-c | 2026-07-10 | GitHub-only artifact (Zenodo re-publish 保留) | ★ F3 / §C.9 F.1 CLOSURE — Binary 64-entry Lean 4 refinement 18 axiom-free theorem |
v0.9 bundle publish 保留理由: v0.9-a Dynamic Decoupling (fidelity 0.99+ 目標) submit script (STEP 1263) は完成しているが、 IBM Cloud Qiskit Runtime instance provisioning が藤本さん dashboard 操作待ち のため未実行。 v0.9-a 結果到達後に v0.9-c と bundle して Zenodo new-version publish 予定。 no-rush-publication protocol 準拠 (急がずゆっくりと)。
6. 関連 file (現時点 confirmed)
Lean 4 source
data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8AluRefinement.lean— Unary refinement (NOT/OMEGA/PHI/PSI) + Belnap 16-entry classical-tier subset (STEP 1011, 2026-04-28)data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8Binary64Refinement.lean— v0.9-c artifact (STEP 1264、 443 行、 18 axiom-free theorem)data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8SelfReflexivePreservation.lean— SELF⟲ preservation (別 track)
Verilog source
data/verilog/dfumt8_alu.v— 200 行 Verilog RTL、 truth tables lines 94-140 (STEP 1006, 2026-04-28)
IBM Heron r2 submit scripts
scripts/quantum/dfumt8_phase_z_real_hardware.py— Phase 1 32 circuits (2026-05-09)scripts/quantum/dfumt8_unitary_phase2.py— Phase 2 XOR 64 circuitsscripts/quantum/dfumt8_phase_z_phase4_belnap_v05.py— Phase 4 naive (v0.5、 relaxation bias 検出)scripts/quantum/dfumt8_phase_z_phase4_qm_v08.py— Phase 4 Quine-McCluskey (v0.8、 32/32 PASS)scripts/quantum/dfumt8_phase_z_phase4_dd_v09a.py— v0.9-a Dynamic Decoupling (submit-ready blocked)
Paper draft
papers/paper-145-first-dfumt8-silicon-self-primitive-DRAFT.md— full paper draft (v0.9-c status)papers/paper-145-v0.6-symbiyosys-formal-verify-2026-08-04.md— SymbiYosys formal verification (STEP marathon 2026-08-04)papers/paper-145-v0.9-d-outline-2026-07-24.md— v0.9-d outline (candidate)
Zenodo published versions
data/publications/publish-log-paper145-v06-zenodo.json— v0.6 parentdata/publications/publish-log-paper145-v08-zenodo.json— v0.8 (current published latest)data/publications/publish-log-paper145-ia-harvard.json— Internet Archive mirror
7. Honest scope (譲れない線)
(1) 「世界初」 主張の controllable 範囲 — feedback_world_uniqueness_claim_controllable 継承。 「First D-FUMT₈ Silicon with SELF⟲ Logic Primitive」 は audit 範囲内 = 具体的な 8 tuple semantics + SELF⟲ initial-tier primitive の組み合わせに限定。 「世界唯一の 8 値 hardware」 主張は不使用 (Heald U8 2024-25 + Shramko-Wansing EIGHT₄ 2009 + MIT 2026 qudit d=8 全 prior art、 「D-FUMT₈ = 8 tuple 意味 + SELF⟲ + 4-substrate cross-verification」 の組み合わせのみ差別化)。
(2) Refinement 定理 = trivial derivation — aluAnd_refines / aluOr_refines は unfold aluAndBits; rw [Dfumt8.fromBits_toBits, Dfumt8.fromBits_toBits] で trivial derivation。 §B.5.4 unary と同じ round-trip strategy。 load-bearing content は 64-entry table 自体 + 16-subset consistency + 32-entry cross-tier design rule 明示化。
(3) Verilog RTL vs silicon empirical evidence の分離 — 本 Lean 4 file は Lean 抽象型 と 3-bit Verilog encoding の refinement 証明。 Verilog RTL の silicon 動作 は 別 layer (empirical、 testbench 50/50 PASS が evidence)。 混同禁止。
(4) Timing / metastability / physical FPGA effects は依然 empirical (Lean 4 refinement では unrepresented)。 SymbiYosys formal verification (v0.6 marathon 2026-08-04) は別 track で追加検証中。
(5) v0.9-c は zero-budget artifact — pure Lean 4 work、 IBM budget 消費 0 sec。 Zenodo re-publish 保留 (v0.9 bundle 完成待ち)。 「急がずゆっくりと」 (feedback_no_rush_publication) 適用継続。
(6) STEP 1215 and8/or8 と PhaseC aluAnd/aluOr は別 namespace 独立 formalization (STEP 1215 = truth-order semantics / PhaseC = Verilog approximation semantics)。 2 つの独立 8-valued AND が共存、 non-conflict。 混同禁止。