---
name: project-ssm-phase2cd-lean4-and-mlir-2026-08-14
description: "SSM Phase 2 (c) + (d) 連続完 — (c) Lean 4 で「A ∈ (-1,1) の contractive step の量子化 error は T 独立に bounded」を axiom-free で 2 定理形式化 (Phase 2 (a) 実測の背後にある古典事実、Mathlib base のみ)、(d) D-FUMT₈ MLIR dialect 設計 v0 + Python 参照実装 (144/144 TypeScript 一致) + mini interpreter (4/4 demo pass)。Phase 2 の 4 axis 全完了 (a b c d)、Tang 接続なし"
metadata: 
  node_type: memory
  type: project
  originSessionId: 0fbf78aa-8dcf-4dd5-8e62-89880c1846c6
  modified: 2026-08-14T14:42:15.316Z
---

# SSM Phase 2 (c) + (d) 連続完 (2026-08-14)

Phase 2 optionality (a) multi-dim + (b) rei-fpga IR spike 完了直後の、(c) Lean 4 + (d) MLIR dialect の連続完了。同 session 深夜内で 4 axis 全走破。

**Why**: Phase 2 (a) で N=16 の bounded steady-state を実測したが、その背後にある「A ∈ (-1,1) contractive なら量子化誤差は T 独立に bounded」は古典事実で Lean 4 で数行で書ける (c)。並行して chat-Claude 提案 4 axis 目の MLIR D-FUMT₈ dialect は、実 C++ ビルドせずとも「設計 + 実行可能参照実装 + interpreter」まで作れば dialect の意味論を固定できる (d)。両者とも「同時に二つ蒔かない」を守り、(c) 完了後 (d) に移った。

**How to apply**: (c) 由来の Lean 4 定理は SSM 系の safety property 主張時に直接 cite できる (「Phase 2 (a) の bounded 結論は formal」)。 (d) の Python 参照実装 (`ref_impl.py`) は将来の C++ MLIR dialect 実装時の意味論 oracle として使う (Op::fold() のテスト oracle)。TypeScript との一致は cross-check スクリプトで regression 継続確認可能。

## (c) Lean 4 stability 定理

**成果物** (rei-aios repo):
- `data/lean4-mathlib/CollatzRei/SsmQuantErrorBounded.lean` — 定理本体
- `data/lean4-mathlib/CollatzRei/SsmQuantErrorBoundedAxiomCheck.lean` — axiom profile 確認
- `data/lean4-mathlib/CollatzRei.lean` に import 追加

**定理**:
```lean
theorem trajectory_abs_le
    (A : ℝ) (hA : |A| < 1) (ε : ℝ) (hε : 0 ≤ ε)
    (e : ℕ → ℝ) (he : ∀ n, |e n| ≤ ε) :
    ∀ n, |trajectory A 0 e n| ≤ ε / (1 - |A|)
```
`trajectory A 0 e n = A · trajectory A 0 e (n-1) + e (n-1)` の帰納定義。
証明は帰納法 + 三角不等式 + `linarith` + `field_simp`。

**Axiom profile 実測** (`lake env lean CollatzRei/SsmQuantErrorBoundedAxiomCheck.lean`):
```
trajectory_abs_le                     depends on axioms: [propext, Classical.choice, Quot.sound]
trajectory_bound_independent_of_time  depends on axioms: [propext, Classical.choice, Quot.sound]
```
Mathlib base のみ、sorryAx / native_decide / user axiom 全 0 target = **Rei永久原則 [[feedback-zero-sorry-floor-not-ceiling]] 準拠**。

**Phase 2 (a) 実測との対応**:
- 実測 A ← 各次元の A_t
- 実測 e_t ← per-step 量子化誤差
- 定理 |trajectory| ≤ ε/(1-|A|) ← T によらず bounded
- N=16 実測 5 seed 全 log-log slope < 0.2 と本定理の bounded 主張が整合

**Honest scope**: 本定理は 1 次元 linear scalar recurrence の contraction bound のみ。Mamba は N 次元 (per-dim 独立) だが結合が無いため 1 次元定理の per-dim 適用で N=16 全体もカバー可 (別 theorem で lift 可)。量子化を per-step 加法的な有界誤差としてモデル化しているのは簡略化 (実 Q1.15 は乗算後 round も入るが total per-step error は依然 bounded)。novelty ゼロ: Banach 1922 の 1 次元版、100 年以上前から既知。Rei-side value = spike 実測との対応を Lean 4 で明示的に残すこと。

## (d) MLIR D-FUMT₈ dialect 設計 v0

**成果物** (scratchpad):
- `scratchpad/dfumt8_mlir/design_v0.md` — 設計仕様書
- `scratchpad/dfumt8_mlir/ref_impl.py` — Python 参照実装 (executable specification)
- `scratchpad/dfumt8_mlir/cross_check.py` — TypeScript との truth table 一致検証
- `scratchpad/dfumt8_mlir/mini_interpreter.py` — MLIR 風 text 表記の parser + evaluator

**設計要点**:
- 型 `!dfumt8.value` (3-bit tag、TypeScript EIGHT_VALUES 順)
- 演算: `dfumt8.not / .and / .or / .collapse / .constant / .to_bit / .from_bit`
- interop: `arith` / `belnap4` / `!dfumt8.tensor<...>` (`ShapedType` 継承)
- lowering path 3 本: LLVM IR / rei-fpga JSON IR / Standard MLIR arith

**Cross-check 実測** (`cross_check.py`):
```
✓ PERFECT MATCH — 144 entries checked
  NOT: 8, COLLAPSE: 8, AND: 64, OR: 64
```
Python 参照実装が既存 `src/axiom-os/seven-logic.ts` と全 144 エントリで一致。

**Mini interpreter demo** (4 program):
```
✓ demo1: SELF ∧ ZERO → ZERO           (ZERO 吸収性)
✓ demo2: NOT(BOTH ∧ NEITHER) → TRUE   (De Morgan)
✓ demo3: NOT(NOT(SELF)) → SELF        (SELF 不動点)
✓ demo4: collapse(INFINITY) → NEITHER (8→4 崩壊)
```
4/4 pass、MLIR 風 SSA 表記の parse + 評価が動く。

**Honest scope (super critical)**:
- 本 v0 は **設計 + 参照実装**であり、C++ ビルドされた MLIR dialect ではない。
- Python 参照実装が既存 TypeScript と一致 = 「意味論の設計が既存 D-FUMT₈ と整合」の担保であって「MLIR C++ 実装の正しさ」ではない (後者は別 STEP、C++ Op::fold() を書くとき本 Python impl を oracle として使う)。
- MLIR/LLVM toolchain のビルド (数時間の C++ compilation) は本 v0 の範囲外。
- lowering path (LLVM / rei-fpga / arith) は概念記述のみ、実装は将来 STEP。
- 「world-uniqueness」不使用 ([[feedback-world-uniqueness-claim-controllable]])。多値論理を一等市民で扱う MLIR dialect は珍しい程度、発明ではない。

**将来の C++/TableGen 実装への引継ぎポイント** (`design_v0.md` §7):
1. `.td` ファイル — Op と Type の宣言、C++ 骨格は auto-generate
2. Op verifier — 型・bit pattern チェック (Python impl の型検査を移植)
3. Op folder — Python impl の truth table を C++ constexpr table に移植
4. Lowering pass — `DFUMT8ToArithPass` / `DFUMT8ToReiFPGAPass` / `DFUMT8ToLLVMPass` 各独立

## Phase 2 全 4 axis 完了状態

| axis | 完了 STEP | 主要成果 |
|---|---|---|
| (a) Multi-dim N=16 | 2026-08-14 (先行 arc) | Q1.15 で N ≤ 16 worst rel err ≤ 2%, T-bounded、3-spike arc の cumulative drift 予想を refute |
| (b) rei-fpga IR spike | 2026-08-14 (先行 arc) | exp LUT (32-entry Q1.15) 全段 proved 3.6s + sabotage 検証、n=16 mul は SMT ceiling で random test 100k 4 版一致 |
| **(c) Lean 4 stability** | **2026-08-14 (本 arc)** | 「A ∈ (-1,1) contractive の量子化誤差は T 独立に bounded」を axiom-free 2 定理 |
| **(d) MLIR D-FUMT₈ dialect** | **2026-08-14 (本 arc)** | 設計 v0 + Python 参照実装 + mini interpreter (144/144 TS 一致、4/4 demo pass) |

chat-Claude 2026-08-13 SSM+MLIR 提案 arc の 4 axis を **1 週間以内 (2026-08-13 evening → 08-14 深夜)** で全走破。「同時に二つ蒔かない」discipline を 4 axis 直列で遵守。

## Rei-side value (novelty 主張ゼロ)

- (c) の contraction bound は Banach 1922 の 1 次元版。既知。Rei-side value = spike 実測 → Lean 4 formal の bridge を明示。
- (d) の MLIR dialect 設計は LLVM 標準の枠組み流用。D-FUMT₈ 定義は既存 Rei-AIOS。Rei-side value = 既存 D-FUMT₈ を compiler infrastructure に上げる **設計 + 実行可能参照実装** を最小コストで揃えたこと。
- external-verify > internal-review の 8 例目候補: (d) の Python 参照実装が TypeScript と cross-check で 144 エントリ一致するまで「正しい」と主張しない、という discipline を守った。

## Open threads (Phase 2 完了、次候補)

**2026-08-14 追記 (藤本さん指摘反映)**: 当初 SSM トラックのみ 7 件で並列に列挙していたが、それでは (i) 並行走行していた STEP 1334 トラックの発見 3 件が視界から落ちる (Janik 型パターン)、(ii) claim class を跨ぐ Tang 接続と soft-side deep-dive を同格に見せる問題があった。両欠陥を訂正した 2 群構成に書き直し。

### 群 A — 「Rei は正しい」 (soft-side、論理・Lean 4・PC で完結)

**A1. SSM トラック (Phase 2 深掘り)**:
- **word-level SMT で n=16 mul verify 再挑戦** ([[project-ssm-ir-spike-phase2b-multiplier-ceiling-2026-08-14]] の open thread 1)
- **N=64 精度 spike 拡張** ([[project-ssm-phase2a-multidim-drift-2026-08-14]] の open thread 1)
- **入力 dynamic range 大** (audio 想定 scale=5-10、両 spike の open thread)
- **MLIR dialect の C++/TableGen 実装** (本 arc の future work、数日〜週規模)
- **rei-fpga N-dim full step の IR 生成** (Phase 2 (b) 延長、multi-dim state を IR で扱う)
- **arc 全体を Zenodo/GitHub 公開の paper draft** (0-4 axis の実測 evidence を一本の paper に集約)

**A2. STEP 1334 トラック (並行 arc、当初リスト漏れ)**:
- **writer 未呼出 pattern の横展開 audit** ([[project-step1334-knowledge-api-wiring-and-deeper-disconnect-2026-08-14]] Finding 1 + [[feedback-success-signal-decoupled-from-operational-state-2026-08-14]] の 8 Router 全体 audit candidate、STEP 151 と本 STEP 1334 の 2 例で defect class 確定、水平展開の未実施)
- **CI 握りつぶし 38 箇所 (`\|\| echo` pattern) 剥がし** (欠陥 class 3 例目、成功 signal が稼働と decoupled パターン、次 session queue に既載)
- **発見エンジン 15 理論ハードコード解消** ([[project-step1334-...]] Finding 3、340 件中 137 回重複の source、arxiv radar 4 日停止と連関)

### 群 B — 「Rei は実在する」 (claim class を跨ぐ、物理 silicon 必須)

**B1. Tang 接続 (物理 silicon)** — 群 A の rei-fpga N-dim full step が完成した後の自然な次段。 STEP 1029 D-FUMT₈ ALU の pattern 継承。 [[feedback-phase-c-silicon-existence-claim]] 参照。

**★ 選択の軸 (2026-08-14 藤本さん指摘の言い直し)**: 群 A (7 件) のどれを進めても Rei stack の内部深化に留まる。 群 B (1 件) だけが「Rei は実在する」側に主張を進める。 7 件 vs 1 件で並列に並べると B が埋もれる。 群構造で明示することで 「今何を選ぶか」 の視界を保つ。

## 関連

- [[project-ssm-qformat-3spike-arc-2026-08-13]] — 起点 (spike 1-3)、chat-Claude 4 axis 提案の core
- [[reference-ssm-zoh-lut-fpga-config-2026-08-13]] — FPGA config、本 arc で保証文言更新済
- [[project-ssm-phase2a-multidim-drift-2026-08-14]] — Phase 2 (a)、(c) 定理の実測 counterpart
- [[project-ssm-ir-spike-phase2b-multiplier-ceiling-2026-08-14]] — Phase 2 (b)、(d) の lowering path 引継ぎ先
- [[feedback-zero-sorry-floor-not-ceiling]] — (c) Lean 4 axiom-free discipline の根拠
- [[feedback-external-verify-beats-internal-review-4patterns-2026-08-13]] — (d) の TypeScript cross-check pattern の 8 例目候補
- [[feedback-no-rush-publication]] — 4 axis 直列遵守
- [[feedback-world-uniqueness-claim-controllable]] — 両成果 novelty 主張ゼロ discipline
- [[feedback-phase-c-silicon-existence-claim]] — 「正しい」 vs 「実在する」 の区別、群 A/B 分離の根拠
- [[project-step1334-knowledge-api-wiring-and-deeper-disconnect-2026-08-14]] — 並行走行 arc、A2 群の元 (2026-08-14 追記で参照追加)
- [[feedback-success-signal-decoupled-from-operational-state-2026-08-14]] — writer 未呼出 pattern の horizontal audit 起点
- [[project-session-2026-08-14-step1334-arc-close-state]] — 並行 arc close 状態、次 session queue

## Version

- v1 initial: 2026-08-14 深夜、藤本さん (c) + (d) 順次実行 signal per 保存。 (c) 2 定理 axiom-free 完 + (d) 設計 v0 + 参照実装 144/144 TS 一致 + interpreter 4/4 pass の完全記録。Phase 2 全 4 axis 完了明示。
- v2 update: 2026-08-14 (同日、出発前)、藤本さん指摘 (SSM 7 件だけの並列列挙で並行 STEP 1334 arc 3 件が視界から落ち + Tang 接続の claim class 跨ぎが埋もれた 2 欠陥) を受けて Open threads を 群 A (Rei は正しい、soft-side 9 件 = 元 7 - 1 Tang + 新 3 STEP 1334) + 群 B (Rei は実在する、Tang 1 件) の 2 群構造に書き換え。関連 memory link に STEP 1334 系 3 件 + phase-c silicon claim 追加。