---
name: project-step1401-rei-checker-mcp-v03-lean-repl-d8-2026-08-24
description: STEP 1401 rei-checker-mcp v0.3.0a1 = LeanBackend Stage 1 wired + D-FUMT₈ ledger projection (Option X spec §1.3 preservation)、pending-lean4-neither-mcp-connector (b) pickup 完了
metadata: 
  node_type: memory
  type: project
  originSessionId: dadb5340-3a5e-41c6-a6ea-a557191d9c84
  modified: 2026-08-23T22:13:04.676Z
---

# STEP 1401 — rei-checker-mcp v0.3.0a1 (LeanBackend + D-FUMT₈ ledger)

**Date**: 2026-08-24
**Repo**: fc0web/rei-checker-mcp
**Commit**: `107a33c` (push 済 `13b653b..107a33c main -> main`)
**Version**: 0.2.0a1 → 0.3.0a1

## 経緯

- 2026-08-23 chat-Claude 2-turn arc: 「Lean 4 sorry-zero 実在 + NEITHER 意味論完成 + **接続 gap** 指摘」
- [[pending-lean4-neither-mcp-connector-2026-08-23]] 帰宅後 pickup 待機、5 選択肢 (a)-(e)
- 藤本さん directive 「(b) でお願い致します」 = rei-checker-mcp v0.3 拡張 選択
- 私 spec §1.3 tension 検出 → 3 択 (X ledger only / Y 別 tool / Z opt-in flag) → 藤本さん 「推奨は?」 → 私 **Option X 推奨** (spec §1.3 100% preserve、 rei-aios MCP に D-FUMT₈ surface 既完備、 chat-Claude 接続 gap は ledger 経路で 埋まる) → 藤本さん 「Option X で 実行」 承認

## 実装 (Option X = spec §1.3 保護 の operational form)

**5 file 修正 + 1 file 新規**:

| file | 変更内容 |
|---|---|
| **`rei_checker/d_fumt8.py`** (NEW、 ~230 行) | mapping table + `D8Value` enum + `map_verdict_to_d8()` + `d8_payload()` + `spec_table()` 9 entry |
| `rei_checker/backend.py` | `LeanBackend` v0.3 subprocess REPL wire (persistent process、 threading.Queue、 timeout hard-kill、 graceful degradation) |
| `rei_checker/schema.py` | `LedgerEntry.d_fumt8` Optional + `StatsResult.d_fumt8_breakdown` Optional (両方 default None、 backward compat) |
| `rei_checker/verify.py` | `map_verdict_to_d8()` call → LedgerEntry.d_fumt8 populate |
| `rei_checker/stats.py` | `include_d_fumt8: bool = False` opt-in param |
| `rei_checker/ledger.py` | read `d_fumt8` field (backward compat pre-v0.3 rows) |
| `rei_checker/__init__.py` + `pyproject.toml` | version bump 0.2.0a1 → 0.3.0a1 |
| `README.md` + `CLAUDE.md` | v0.3 change log + D-FUMT₈ mapping table doc |

## D-FUMT₈ mapping table (`rei_checker/d_fumt8.py`)

| verdict / reason_code | D-FUMT₈ | 根拠 |
|---|---|---|
| VALID | TRUE (⊤) | 証明済 = 真値 |
| INVALID | FALSE (⊥) | 反証済 = 偽値 |
| UNDECIDED / TIMEOUT | NEITHER (〜) | chat-Claude 「便りが来ない」 = 判定不能 |
| UNDECIDED / PARSE_FAILURE | ZERO (〇) | まだ問われていない = 無効入力 (校正原点) |
| UNDECIDED / UNSUPPORTED_SYNTAX | NEITHER (〜) | 判定不能 = 表現不能 |
| UNDECIDED / MISSING_AXIOM | NEITHER (〜) | 判定不能 = 前提不足 |
| UNDECIDED / DEPTH_LIMIT | INFINITY (∞) | 評価不能 = 上限 hit |
| UNDECIDED / OUT_OF_SCOPE | NEITHER (〜) | 判定不能 = 対象外 |
| UNDECIDED / UNCLASSIFIED | NEITHER (〜) | 判定不能 = 未分類 (V02_PROTOCOL §6 D11) |

**Non-emitted (v0.3 spike scope)**: BOTH / FLOWING / SELF は 予約 (v0.4+ candidate、 multi-backend cross-check / streaming semantics / self-referential expressions で 実装)。

**Source marker discipline** (STEP 1349/1350 pattern 継承): 全 payload に `source: "rei-checker-d-fumt8-mapping"` field 埋め込み = downstream (rei-aios MCP / cross-project 分析) は rei-aios D-FUMT₈ producer と 区別可能。

## spec §1.3 保護 (Option X 3 条件)

1. ✅ `VerifyResult` (MCP response) には `d_fumt8` **出さない** (`to_dict()` に field なし、test `test_verify_result_dict_does_not_expose_d_fumt8` 通過)
2. ✅ `StatsResult.to_dict()` default output も 変えない (`include_d_fumt8=True` opt-in のみ で `d_fumt8_breakdown` 追加、test `test_stats_default_no_d_fumt8_breakdown` 通過)
3. ✅ `LedgerEntry.d_fumt8` optional field で backward compat (pre-v0.3 rows は `d_fumt8` 欠如で読み込み OK、test `test_ledger_entry_d_fumt8_optional_default_none` 通過)

## LeanBackend Stage 1 wire (persistent JSON REPL)

- **Binary auto-detect**: `<repo>/lean_backend/.lake/build/bin/lean_checker_repl.exe` (env `REI_CHECKER_LEAN_BINARY` override 可)
- **Persistent process**: 初回 check() で spawn、以降 reuse (warm ~1.5ms per STEP 1367)
- **Threading Queue**: stdout 読み取り background daemon thread + `Queue.get(timeout=timeout_ms)` main check() で timeout 制御
- **Timeout hard-kill**: `Queue.Empty` 検出 → subprocess terminate + wait 2s → kill + wait 1s、 次 check() で 自動 respawn = **hanging Lean process 残らない**
- **Graceful degradation**: binary 不在 → UNDECIDED/OUT_OF_SCOPE + detail path 明示
- **Protocol error handling**: unknown verdict / unknown reason_code / malformed JSON → UNDECIDED/UNCLASSIFIED or PARSE_FAILURE

## test 実測 (105/105 PASS)

- **v0.2.0a1 pre-existing**: 73 tests
- **v0.3 new**: **32 tests**
  - TestLeanBackendV03: 8 (real REPL, ~83ms total)
  - TestLeanBackendGracefulDegradation: 3
  - TestDFumt8Mapping: 13
  - TestLedgerEntryD8Field: 3
  - TestVerifyD8LedgerIntegration: 3
  - TestStatsD8Optin: 3 (default off / opt-in / pre-v0.3 skip)

Regression: 0 breaking (73/73 pre-v0.3 pass 継続、except `test_stub_always_returns_undecided_out_of_scope` → 削除 (obsolete、 stub → real wire で 期待変化))。

## E2E smoke (LeanBackend + D-FUMT₈ ledger + spec §1.3 verify)

```bash
export REI_CHECKER_BACKEND=lean
python -m rei_checker verify "1 + 1 = 2"     # {verdict: VALID, elapsed_ms: 72}
python -m rei_checker verify "<axiom-test>"  # {verdict: UNDECIDED, reason_code: MISSING_AXIOM}
```

Ledger:
```json
{"verdict": "VALID", "d_fumt8": "TRUE", ...}
{"verdict": "UNDECIDED", "reason_code": "MISSING_AXIOM", "d_fumt8": "NEITHER", ...}
```

`stats(include_d_fumt8=True)` → `d_fumt8_breakdown: {TRUE: 1, FALSE: 1, NEITHER: 2}`

## Rei stack alignment

- **D-FUMT₈ surface は rei-aios MCP 側で 既完備** (STEP 1349/1350/1371/1376/1377/1379/1397 = 6 systems 8+ tools)、rei-checker-mcp は **単方向 flow** (checker が ledger に D-FUMT₈ 記録 → 別 tool が ledger 消費) で 責務分離
- **rei-checker-mcp は Rei stack MCP 9th system 位置** (rei-aios v2.8.5 + benchtop v0.7 + mcp-lens + rei-automator-mcp + lab-notebook-mcp + rei-verify + rei-memory-mcp + rei-meta-mcp + **rei-checker-mcp**)
- **修正機 §10 甲 subset 該当** ([[project-step1394-correction-machine-naming-2026-08-23]] chat-Claude spec 継承): rei-checker-mcp は 「別系統 verifier で 一次判定」 の 甲 grade layer、Claude 系が 生成した 主張を 独立に 検証

## Honest scope 8 条

1. **Stage 1 semantics のみ** = lean_checker_repl.exe は hardcoded truth table (MockBackend mirror)、Stage 2 real `Lean.Elab.decide` dispatch は 未実装、次 v0.4 spike candidate
2. **novelty ゼロ** ([[feedback-world-uniqueness-claim-controllable]] 適用) = D-FUMT₈ 本体 STEP 406 2 年以上前既存 asset、本 STEP は ledger annotation layer 追加のみ
3. **spec §1.3 preservation** = literal preservation で 実装 (verify() response 変更なし、stats() default 変更なし、opt-in flag のみ)
4. **Timeout hard-kill は best-effort** = threading.Queue based、Windows subprocess.Popen limitation あり (parent-child signal not always guaranteed)
5. **LeanBackend cold spawn ~150ms** (STEP 1367 measurement、本 STEP CLI smoke で 72ms 実測 = subprocess spawn 込み)、warm 1.5ms は long-lived MCP server context でのみ 顕在化
6. **pre-v0.3 ledger rows は d_fumt8 欠如** = backward compat、stats include_d_fumt8=True 時 は skip (retroactive inference しない、honest scope)
7. **spec_table() 9 entries** = 現状 mapping の 完全網羅、v0.4+ で BOTH/FLOWING/SELF 3 値追加時 に spec_table + mapping table 両方 update discipline (drift 予防)
8. **SAC-4 47 教訓 Phase 3-18 継続** = pre-staged 0 件 confirm 後 明示 file add、cron sweep なし、write-time STEP number verify (STEP 1400 別タブ landed catch 済、collision なし)

## 4 pending 選択肢 status

| # | option | status |
|---|---|---|
| (a) | Andrica verify | ⏸ 別 STEP candidate (STEP 1387 予告の Andrica 22 zero-sorry 実 verify、 独立 arc) |
| **(b)** | **rei-checker-mcp v0.3 拡張** | ✅ **本 STEP で 完了** |
| (c) | ledger_query 実装 | ⏸ 別 STEP candidate (本 STEP で ledger.d_fumt8 追加済 = query layer 追加は 別 arc) |
| (d) | (b)+(c) セット | 部分完了 ((b) done、 (c) 別 STEP) |
| (e) | 別方針 | 該当なし |

## 次 candidate (別 STEP、藤本さん stance 待ち)

- **v0.4 Lean 4 Stage 2** = `Lean.Elab.decide` real dispatch + `#print axioms` verify + `Not <expr>` refutation attempt (V02_PROTOCOL.md §2 完全実装)
- **(c) ledger_query MCP tool** = spec §5 「MCP tool 2 つだけ」 tension、opt-in tool として 追加検討
- **D-FUMT₈ BOTH/FLOWING/SELF 3 値追加** = multi-backend cross-check (BOTH) + streaming semantics (FLOWING) + self-referential expr (SELF)
- **rei-checker-mcp を Rei stack MCP 9th system として rei-aios から consume** = ledger.d_fumt8 grep → rei-aios stats aggregation

## 関連

- [[pending-lean4-neither-mcp-connector-2026-08-23]] (本 STEP で pickup 完了、(b) 実装)
- [[project-step1394-correction-machine-naming-2026-08-23]] (修正機 §10 甲 subset 位置付け)
- [[project-step1349-d8-operator-connectors-2026-08-20]] (rei-aios D-FUMT₈ operator connector 起点)
- [[project-step1350-d8-verdict-mapping-phase-a-2026-08-20]] (rei-aios D-FUMT₈ 測定 domain、 本 STEP は checker domain で 兄弟)
- [[project-step1367-lean4-repl-harness-v021-stage1-spike-2026-08-22]] (Lean REPL harness 起点、 本 STEP で 実 wire)
- [[project-step1365-rei-checker-mcp-v01-spike-arc-2026-08-22]] (rei-checker-mcp v0.1 origin)
- [[project-step1366-gemini-lean-verify-archival-and-v02-protocol-2026-08-22]] (V02_PROTOCOL.md 5 protocol 準拠)
- [[feedback-all-research-site-reflection-default]] 2026-08-06 protocol 継続
- [[feedback-no-rush-publication]] 単日 close
- [[feedback-world-uniqueness-claim-controllable]] 継承
- [[feedback-projection-self-audit-pattern]] SAC-4 継承
- [[feedback-critique-response-pattern]] SAC-4 100% 認諾 discipline