STEP 1655 — rei-checker-mcp ledger ingest

Date: 2026-09-01  ·  Repo: fc0web/rei-aios  ·  Consumes: fc0web/rei-checker-mcp v0.4.0a1

起点

藤本さん directive: 「verify を SEED_KERNEL と Andrica に繋いでください」。 順序判定 (前 turn) = 作らずに繋ぐ。既存の rei-checker-mcp verify/stats/ledger 三点は 2026-08-26 に 藤本さん自ら §7 by_decision timing まで landed 済 (v0.4.0a1)。 足りないのは投入量 (13 rows) だった。

Path 選択

3 択のうち Path C (既存 axiom-scan の retrofit ingest) を採用。verify() 経路を通さず、 STEP 1368 で既に lake env lean により計算済みの 333 theorem × axiom profile を ledger schema に mapping して append する bridge。

Mapping table

Axiom profileVerdictReasonD-FUMT₈
zero-axiomVALID—TRUE
Mathlib-base only (propext / Classical.choice / Quot.sound)VALID—TRUE
hasSorryAxUNDECIDEDMISSING_AXIOMNEITHER
hasUserAxiomUNDECIDEDMISSING_AXIOMNEITHER
hasNativeDecide (only)UNDECIDEDOUT_OF_SCOPENEITHER

実測 (post-apply)

ledger: 13 → 429 rows

stats() output:
  total:              429
  valid:              331
  invalid:            0
  undecided:          98
  decision_rate:      0.7716    (was ~0.15 with 13 rows)
  reason_breakdown:   {"OUT_OF_SCOPE": 89, "MISSING_AXIOM": 3, "TIMEOUT": 6}
  d_fumt8_breakdown:  {"TRUE": 327, "NEITHER": 95}
  by_decision:
    VALID:     p50=0ms  p90=0ms  p99=0ms
    UNDECIDED: p50=0ms  p90=0ms  p99=0ms

由来別内訳 (checker_version マーカー)

checker_versionRows由来
axiom-scan-ingest/2026-08-22+lean-4.33.1333STEP 1368 axiom-scan pipeline (SEED_KERNEL formalized subset)
andrica-source-scan/2026-09-01+no-axiom-check-sidecar83AndricaConjecture.lean (63) + AndricaGoldenConstantPolynomial.lean (20) の theorem/lemma 名 regex 抽出 (AxiomCheck sidecar 未整備)
rei-checker-mcp/0.3.0a1+lean-repl-d8-2026-08-2413既存 STEP 1401/1402 smoke
Honest scope:
  1. elapsed_ms=0 は仕様。 これらの row は verify() を経由していない。 by_decision timing 診断 (藤本さん 2026-08-26 §7 論点) の p50/p90/p99 は現状すべて 0ms で、 「時間分布はまだ空」の状態を honest に示している。Stage 2 LeanBackend の real dispatch が landed した後、verify() 経由の row が入り始めて初めて timing 分布が意味を持つ。
  2. Andrica 83 rows は全 UNDECIDED / OUT_OF_SCOPE。 AndricaConjecture.lean + AndricaGoldenConstantPolynomial.lean には 対応する *AxiomCheck.lean sidecar が存在しないため、 theorem 名は抽出できたが axiom profile は不明。 sidecar を追加して axiom-scan を再実行すれば retroactively promote 可能 (ledger は append-only、古い UNDECIDED は上書きしない — 差分自体が evidence)。
  3. Andrica の 「22 zero-sorry」 は本 ingest では検証していない。 memory 記録上の 22 zero-sorry は STEP 1387 由来の主張で、本 STEP はその 22 の内訳を 独立に再検証してはいない。sidecar 追加が正しい経路。
  4. 由来分離は checker_version prefix のみ。 verify() row と ingest row の 混同予防は将来の stats() side に filter_by_source option 追加で 構造化可能 (現状 v0.5 candidate、未 spec)。

Files

次段 candidate

STEP 1554 atomic-commit protocol dogfood 33 例目。3 tab 併走中の独立 arc。