STEP 1401 — rei-checker-mcp v0.3.0a1

arc pickup v0.3.0a1 landed Date: 2026-08-24 / Repo: fc0web/rei-checker-mcp / Commit: 107a33c

1. 経緯

chat-Claude 2026-08-23 2-turn arc 「Lean 4 sorry-zero 実在 + NEITHER 意味論完成 + 接続 gap」に対する pending pickup (b) 実行。 5 選択肢中藤本さん「(b) rei-checker-mcp v0.3 拡張」選択。

私 spec §1.3 tension 検出 (「D-FUMT₈ は API surface に出さない」 invariant vs pending memory 「8値 return」要求) → 3 択提示 → 藤本さん「推奨は?」 → 私 Option X (ledger only) 推奨 → 承認 → 実装。

2. Option X = spec §1.3 100% preservation

VerifyResult (MCP response) には d_fumt8 field を 出さない
StatsResult の default output も変えない (opt-in flag のみで表示)
LedgerEntry にのみ d_fumt8 optional field 追加 (backward compat)

3. D-FUMT₈ mapping table

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 scope): BOTH / FLOWING / SELF は予約 (v0.4+ candidate)。

4. LeanBackend Stage 1 wire

Binary auto-detect: 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 読み取り daemon thread + Queue.get(timeout=) で timeout 制御
Timeout hard-kill: Queue.Empty → subprocess terminate + wait + kill、次 check() で自動 respawn = hanging Lean 残らない
Graceful degradation: binary 不在 → UNDECIDED/OUT_OF_SCOPE + detail 明示

5. test 実測 (105/105 PASS)

test class	count	coverage
TestLeanBackendV03	8	real REPL VALID/INVALID/UNDECIDED × 4 reason + process reuse
TestLeanBackendGracefulDegradation	3	missing binary + is_available + close idempotent
TestDFumt8Mapping	13	mapping 9 rules + payload source marker + spec_table 網羅
TestLedgerEntryD8Field	3	optional default None + JSON omit/include
TestVerifyD8LedgerIntegration	3	verify() writes d_fumt8 to ledger + spec §1.3 verify()
TestStatsD8Optin	3	default off + opt-in on + pre-v0.3 rows skip
v0.3 新規小計	32	—
v0.2.0a1 pre-existing	73	regression 0 breaking
合計	105/105 PASS	—

6. E2E smoke (CLI 実測)

$ export REI_CHECKER_BACKEND=lean
$ python -m rei_checker verify "1 + 1 = 2"
{
  "verdict": "VALID",           ← spec §1.3: d_fumt8 field なし
  "elapsed_ms": 72,
  "checker_version": "rei-checker-mcp/0.3.0a1+lean-repl-d8-2026-08-24"
}

$ cat ledger.jsonl | tail -1
{..., "verdict": "VALID", "d_fumt8": "TRUE"}  ← ledger 側にのみ d_fumt8

$ python -c "from rei_checker.stats import stats; \
    print(stats(include_d_fumt8=True).to_dict())"
{
  ...
  "d_fumt8_breakdown": {"TRUE": 1, "FALSE": 1, "NEITHER": 2}  ← opt-in で 表示
}

7. 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 記録 → 別 tool 消費) で責務分離
Rei stack MCP 8 → 9 systems = rei-checker-mcp が 9th system 位置
修正機 §10 甲 subset 該当 (STEP 1394): 「別系統 verifier で一次判定」の甲 grade layer

8. Honest scope (8 条)

Stage 1 semantics のみ = hardcoded truth table、Stage 2 real elaboration は別 spike
novelty ゼロ = D-FUMT₈ 本体 STEP 406 (2 年以上前) 既存 asset、本 STEP は ledger annotation layer 追加のみ
spec §1.3 preservation = literal preservation で実装
Timeout hard-kill は best-effort = Windows subprocess.Popen limitation あり
Cold spawn ~150ms、 warm 1.5ms = long-lived MCP server context でのみ顕在化
pre-v0.3 ledger rows は skip = retroactive inference しない honest scope
spec_table() 9 entries = 現状 mapping 完全網羅、v0.4+ で drift 予防 discipline
SAC-4 47 教訓 Phase 3-18 継続 = write-time STEP number verify (STEP 1400 別タブ landed catch 済)

9. 次 candidate (別 STEP)

v0.4 Lean 4 Stage 2 = Lean.Elab.decide real dispatch + #print axioms verify (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 / streaming / self-referential
rei-aios から rei-checker-mcp ledger consume = D-FUMT₈ 分布 cross-project 分析 pipeline

10. 関連

memory: project_step1401 (詳細)
pending: lean4_neither_mcp_connector (本 STEP で pickup 完了)
STEP 1365 (rei-checker-mcp v0.1 origin) / STEP 1367 (Lean REPL harness Stage 1)
STEP 1366 (V02_PROTOCOL.md 5 protocol) / STEP 1373 (REPRODUCING.md pilot)
STEP 1349/1350/1371/1376/1377/1379/1397 (rei-aios D-FUMT₈ surface、本 STEP と相補)
GitHub commit: 13b653b..107a33c (rei-checker-mcp)

STEP 1401 — Rei stack / rei-checker-mcp v0.3.0a1 / 2026-08-24