rei-repair-mcp v0.2 P0 audit

rei-repair-mcp は checker が 出す reject を 「座標付き の 構造化 reject」 に 正規化し、 修正 の 試行履歴 を 計測可能 な 形 で 記録 する MCP server の 仕様 で あり、 実装 は go 後。

中心仮説 (未検証):

修正ループ の 効率 を 決める の は 修正器 (AI) の 賢さ で は なく、 1 回 の reject が 返す 情報量 で ある。

したがって v0 で 3 stream (ctx = 装置C / lean = Lean4 build / lrat = cake_lpr) を 順次 wire。 修正 そのもの は AI 側 が 書き、 装置 は 拒否 の 情報量 と 試行回数 の 測定装置 に 徹する。

装置C (ctx_ledger.py v0.3.1) は subprocess で 叩く binary で は なく Python module。 adapter は import ctx_ledger して 例外 を 捕捉 する 形。 §4.2 の raw_output: str は 「例外 の str(exc) のみ」 で は なく、 {traceback, parsed: {exc_type, message, raise_site, caller_site}} の JSON envelope が 必要 (v0.2 §4.2.1 で 確定)。

Well-known 却下 の 特殊扱い: 例外 で は なく state (si.well_known_pass=False + si.reclassify_reason)。 §6.1 は 「refusal-until-declared 機構 が 出す reject」 に scope 限定 の ため、 v0.1 adapter は 座標化 せず raw_text 経由 で AI に 可視化。 wellknown_reclassify axis は v0.2 adapter candidate (別 STEP)。

Multi-item message の 2 展開ルート: (a) "missing/invalid fields: ['X', 'Y']" (declare 系) / (b) "pending:\n - X\n - Y" (IncompleteLedgerError)。 各 item を regex で 分解 して item 数 = 座標数 として 展開。

装置C は checker binary で は なく core dependency の ため、 v0.1_1 §12 の 「digest 不一致 は warning」 を v0.2 §12.1 で abort に 格上げ。 さらに 「pin が 正しく 取られた か」 と 「upstream の drift」 は 別 concern なので 3 層 に 分ける:

Runtime で sidecar に 触れない: 実行された コード の 同定 に は 12.1 で 足りる (vendored が 実行されている ので vendored の digest が single source of truth)。 sidecar digest が 必要 な の は 「pin が 古びていない か」 と いう 外的妥当性 の 話 で、 これ は ctx_ledger_source_commit + last_drift_check の bookkeeping で 足る。 tab isolation protocol を 壊さない。

価値仮説 「座標付き reject は 修正試行回数 を 減らす」 は、 以下 の いずれか で 反証:

• (a) 同一課題群 で coordinate mode の attempts_to_fix median が naive mode の 0.8 倍以上 (= 20% 未満 の 改善)
• (b) coordinate mode の FIXED_BY_REPAIR 到達率 が naive mode を 下回る
• (c-1) unlocalizable_count > 0 の reject が coordinate mode intake の 50% 超 (multi-stream 汎用閾値)
• (c-2) observed または required の 少なくとも 一方 が null / placeholder の 座標 が 全 coordinate の 50% 超 (partial-coordinatization 検定、 装置C では decoder_exception が captured)
• (d) 同一 candidate に 対する verdict が 非決定的 な 試行 が 10% 超 (測定自体 が 無効)

同時凍結 4 種 (W-R3 別 STEP で 決定、 初回 run 後 改訂禁止):

1. 閾値 (a) / (b) / (c-1) / (c-2) / (d)
2. 課題群 item mix (選定規則・件数・seed)
3. escape_rate = count(FIXED_BY_DECLARED_ESCAPE) / count(all terminal outcomes) の 予測上限 と 読み方 (診断: なぜ 痩せた か)
4. mode 別 n_min(FIXED_BY_REPAIR) — これ を 下回る run は underpowered で 主要指標 を 読まない (判定: 痩せた か どうか)

escape_rate と n_min の 役割分離 が 重要: escape_rate は TIMEOUT / ABANDONED が 嵩んで 主要標本 が 薄くなった とき 何 も 警告しない (分母 が all terminal outcomes)。 n_min が 「痩せた か どうか」 の 判定、 escape_rate は 「なぜ 痩せた か」 の 説明。