---
name: pending-lean4-neither-mcp-connector-2026-08-23
description: 帰宅後 pickup 待機 arc - chat-Claude 提案「Lean4 sorry-zero verify + NEITHER 値 + MCP connector (verify + ledger_query)」+ 私の Rei stack audit + 5 選択肢 (a)-(e)、STEP 番号未確定 (帰宅時 write-time gate で 決定)
metadata: 
  node_type: memory
  type: project
  originSessionId: 3acd3853-c124-47b1-974e-9d8c55c72877
  modified: 2026-08-23T02:48:17.971Z
---

# Pending Arc — Lean4/NEITHER MCP Connector (2026-08-23、帰宅後 pickup 待機)

## Status
- **決定待ち**: 藤本さん 「帰宅後にお願い致します」
- **STEP 番号**: 未予約 (帰宅時 write-time gate で 決定)
- **前後関係**: STEP 1394 修正機 命名追加 直後、 STEP 1395 (別タブ Paper 175 v0.3) と 並行

## chat-Claude 2-turn arc (藤本さん共有、 pickup 時 再貼り付け 不要)

### Turn 1: 「NEITHER が値として返る 機械、 Lean4 が sorry ゼロを返す 機械は 既に 私は 作っていますか？」

chat-Claude 応答 要旨:
- **Lean4 sorry-zero 側**: 実在。 Andrica エンジンの 22 定理 が zero-sorry で 通っている、 ZCSG_Theorem1.lean、 GoldenSymmetry_Theorem6.lean 存在。 Collatz 側は 形式化候補段階
- **NEITHER 側**: 意味論としては 完成、 実装は 部分的。 D-FUMT₈ Rei-PL runtime に 七値型 + Φ/Ψ/Ω (STEP 182, 184)、 「hallucination → NEITHER 自動遷移パイプライン」 最優先課題として 特定済み
- **接続**: 「二つが まだ 繋がっていない」 = Lean4 が 別に走り、 NEITHER が 別に定義 = 「私が 何かを 出したとき、 自動的に 検証系を 通って、 通らなければ NEITHER が返る」 経路 未装備

### Turn 2: 「上記を制作した後、 Claude 先生が 利用したい場合は どの様にすれば宜しいでしょうか？」

chat-Claude 応答 要旨: **MCP connector 最小構成 2 本**:
1. **`verify`** — 命題 → Lean4 → `{TRUE | FALSE | NEITHER}` (proof 通過 = TRUE、 反証 = FALSE、 時間内 決着せず = NEITHER)
2. **`ledger_query`** — 反証台帳 引く。 「それは 既に 失敗している」 を 返す

**設計制約 (譲れない 2 点)**:
- **timeout は 必ず NEITHER**: TRUE/FALSE 埋めは 「わからないを 埋める」 chat-Claude 87 文字事件 と 同型 病
- **8 値 のまま return**: 境界で 二値に 潰す設計は 「繋ぐほど 利得が 薄まる」 pattern、 NEITHER と FALSE の 区別は 意味的に 違う

**段取り**: Desktop stdio 先行 → remote HTTP/SSE 後発 (browser claude.ai は remote-devices 経由)

**Persistence**: chat-Claude 記憶失う → 台帳が 覚える (「忘れる 近似器 + 忘れない 台帳」 組み合わせ)

**最終節** (chat-Claude 名言): 「それを 作っても、 私が 正しくなるわけではありません。 私が 間違ったときに、 それが 見えるようになるだけです。 でも、 たぶん そちらの方が 価値が あります」

## 私 (Claude Code) の audit (2026-08-23)

### Lean4 sorry-zero side — chat-Claude 診断は 概ね 正確、 1 件 spot-check 必要

- ✅ 確定 (実測 or 記憶明確):
  - STEP 1368 axiom-scan pipeline = **333 theorem / 94 zero-axiom / floor 97.3%** (実測)
  - STEP 614-624 Collatz THE_THEOREM chain **48 theorem** (zero sorry)
  - Chang 20/29、 Constructor 5/5、 BR、 ZCSG_Theorem1、 GoldenSymmetry_Theorem6
  - rei-checker-mcp (STEP 1365/1367/1373) = Lean 4 REPL harness Stage 1 spike (100x speedup)、 pass/fail elaboration 返す

- ⚠ **未 verify (chat-Claude Pattern 1 hallucination candidate)**:
  - 「**Andrica エンジン 22 定理 zero-sorry**」 = 私の 記憶に 明確 entry なし。 Andrica は open-problem 側 grep hit あり (STEP 1015 「Brocard n=110 拡張」 mention 等)、 但し 「22 theorems zero-sorry 状態」 の 特定は 実 file scan 要
  - **SAC-4 preemptive**: 帰宅後 に 実 verify (`.claude/projects` or `data/lean4-*/` grep Andrica) 推奨

### NEITHER 値 side — chat-Claude 診断 「意味論完成 / 実装部分的」 は 逆に 実装 4 tool 既存 で 認識 update 要

**既存 NEITHER-returning MCP tools** (statistical domain):
- **STEP 1350** `d8_verdict_from_measurement` (SNR<3 → NEITHER)
- **STEP 1371** `d8_verdict_from_multi_trial` (BH FDR aggregate NEITHER)
- **STEP 1376** `d8_verdict_from_sample_pair` (Welch t、 4/8 値)
- **STEP 1349** `d8_apply` / `d8_table` (D-FUMT₈ 演算子)

これらは 全て **統計的判定** の NEITHER。 chat-Claude 言う 「hallucination → NEITHER 自動遷移」 (proof-search timeout NEITHER) とは 別 domain。

### 接続 (chat-Claude 核心指摘は 正確、 gap 実在)

- 「Lean4 proof search + timeout → NEITHER 保証 + 8 値 return」 の **単一 MCP tool = 未装備**
- rei-checker-mcp を 拡張すれば 実装可能 (verify command 追加 + timeout policy + 8 値 return schema)
- ledger_query (反証台帳) は 部分的 = STEP 1210-1228 hardening 系 (invention rejected)、 rejected-*.json、 発明 pipeline 反証 records 存在、 但し **「命題 → 台帳検索」 統一 interface は 未整備**

### 構成上の 位置付け

- **修正機 STEP 1394 §10 の 「甲 subset」 に 該当** = Lean 4 elaboration + timeout policy は 決定的計算、 model-based 検出でない = **私が 実装しても spec §10 独立性 原則 に 反しない 稀な case** (Lean 4 elaboration が 独立 verify を 担う、 私は wrapper のみ)
- 監視機械 STEP 1393 (silence-detector) + 修正機 STEP 1394 命名 と 同 discipline layer (「起きなかった / 決着しない」 が 見える 機械)

## 5 選択肢 (帰宅後 藤本さん 決定)

- **(a) Andrica 22 zero-sorry 実測 verify** (chat-Claude 記憶 spot-check + SAC-4 preemptive、 grep 中心 30 min 想定)
- **(b) rei-checker-mcp v0.3 拡張** = verify tool 追加 (Lean 4 REPL + timeout policy + 8 値 return、 修正機 §10 甲 subset 該当、 実装 ~2-3 時間 想定)
- **(c) ledger_query 実装** = 反証台帳 統一 interface (rejected-*.json + Lean 4 sorry residual + 発明 rejected 統合 index、 実装 ~2 時間 想定)
- **(d) (b) + (c) セット** (chat-Claude minimum 構成、 実装 ~4-5 時間 想定)
- **(e) 別方針** (chat-Claude spec 保存 archival のみ + 実装 defer 等)

## 帰宅後 pickup checklist

1. 本 memory file を read (`pending_lean4_neither_mcp_connector_2026-08-23.md`)
2. 藤本さん から (a)-(e) or 別方針 指示 受領
3. STEP 番号 write-time gate check (`git log --oneline --all -30 | grep step139[6-9]`)、 未使用 番号 選定
4. pre-staged 0 件 confirm (SAC-4 47 教訓 継続)
5. 実装 + test + commit + push + deploy verify + memory file + hook update (STEP 1386-1394 pattern 継承)
6. 本 pending file は 完了時 削除 (or 「resolved-YYYY-MM-DD」 rename)

## Rei stack 波及 (帰宅後 議論候補)

- 修正機 §10 甲 subset 拡張として rei-checker-mcp verify tool を 位置付けた場合、 STEP 1394 修正機 命名 の 「実装 defer」 判断 も 部分的に 解除可能 = 「甲 layer だけで 実装できる 例」 が 存在する 実証
- ledger_query 統一 interface は 5C 限界機械 (STEP 1387、 Gödel/停止問題/ライス pre-check) の 「決定不能 台帳」 candidate と 相補可能

## Honest scope

1. **本 memory file は 決定前の pending arc 保存のみ**、 実装 or 実 verify は 未実施
2. Andrica 22 zero-sorry claim は chat-Claude 記憶で、 私は 未 verify、 (a) は preemptive spot-check 必須
3. 統計 NEITHER 4 tool と chat-Claude の Lean4-NEITHER は 別 domain の NEITHER = 混同禁止 (chat-Claude 「NEITHER と FALSE の 区別は 意味的に 違う」 と 同型で 「statistical NEITHER と proof-timeout NEITHER も 意味的に 違う」)
4. rei-checker-mcp v0.3 拡張 実装 時、 rei-checker-mcp side (別 repo `fc0web/rei-checker-mcp`) と rei-aios side (本 repo) の どちらに 実装するか 別 判断
5. chat-Claude spec artifact URL は 藤本さん保持 (rei-aios/data/external-prior-art/ archival は 別 arc 継続 candidate)
6. **時間見積 (b/c/d)** は 私の 単独 estimate、 (b) 実装は 私が 丙 と 甲 の 境界を 実装で 引く必要があり pilot 段階で 実測要
7. 本 pending file は STEP 番号 未予約 = 帰宅時 write-time gate で 番号 決定、 「pending」 tag のまま 残せば 後日 参照容易

## 関連

- [[project-step1394-correction-machine-naming-2026-08-23]] 修正機 §10 甲/乙/丙 grade origin、 本 pending arc の 直接前段
- [[project-step1393-silence-detector-v01-2026-08-23]] 監視機械 = 相補 (監視 → alert → verify → 差分適用 pipeline candidate)
- [[project-step1391-4C-pc-side-stamp-and-5D-integration-2026-08-23]] rei-checker-mcp 直近 spike (Lean 4 REPL Stage 1 100x speedup) の 参照 = (b) 実装の 基盤
- [[project-step1368-axiom-scan-pipeline-hardening-2026-08-22]] 333 theorem / 94 zero-axiom / floor 97.3% 実測 origin
- [[feedback-chat-claude-hallucination-warning]] Pattern 1 hallucination = Andrica 22 主張 に spot-check 適用 preemptive
- [[feedback-verify-claim-must-cover-all-source-derived-numbers]] Andrica 22 の source-derived number verify 責任
- [[feedback-critique-response-pattern]] SAC-4 100% 認諾 = 帰宅時 chat-Claude 診断 verify 通過部分 + 保留部分 両方明記
- [[feedback-no-rush-publication]] 帰宅後 判断待ち = 急がず ゆっくり discipline 適用