search_verified — Rei stack 統合 index 検索

MCP tool v0.1 段 2 完成 (2026-08-20) · SEED_KERNEL 1,677 理論 + Rei Lean 4 axiom-free 資産 = 7,466 items

役割: Rei stack の「既に verify されているもの」を一箇所から検索する tool。 SEED_KERNEL 理論と Rei が Lean 4 で書いた axiom-free 資産 (data/lean4-mathlib/CollatzRei/) を同じ index に載せ、 substring + filter で探せる。「これ既に verify したっけ?」に数百ミリ秒で答える手が速くなる道具。補完的な tool: find_gaps (curated Mathlib gap 検索) + audit_gaps (Mathlib mirror cross-check)。

使い方

CLI

# 一度だけ (index build、 ~700ms、 data/exploration/verified-index.db を書き出す)
npm run search:build

# 検索 (数百ミリ秒)
npm run search:verified -- "brownawell"
npm run search:verified -- "trailing" --proved-only --limit 5
npm run search:verified -- "" --unverified                 # sorry を含む全 Lean decl
npm run search:verified -- "" --namespace BrownawellMasser # namespace browse
npm run search:verified -- "collatz" --status proved --json

MCP (Claude Desktop / Claude Code から呼ぶ)

rei-aios MCP server の tool として呼び出せる (rei-mcp-server v2.7.0 の 36 tool の 1 つ)。 index が未生成なら {indexMissing: true} を返して fake 検索結果を永久生成しない (finding #30/#31 discipline 継承)。

返却 payload の field (drift audit 済)

field	意味
`hits[]`	ヒット配列
`hits[].id`	安定 unique id (`seed:...` or `lean4:...`)
`hits[].source`	`seed-kernel` or `lean4-collatz-rei`
`hits[].title`	SEED axiom 文 or Lean theorem 名
`hits[].statement`	full statement (最大 400 文字 truncate)
`hits[].proofStatus`	`proved` \| `hypothesis` \| `speculative`
`hits[].lean4Verified`	true = sorry なし / false = sorry あり / null = 非 Lean 4
`hits[].filePath`, `lineNumber`	Lean 4 decl の source location
`hits[].categoryA`, `dfumt8Value`, `namespace`	metadata
`hits[].score`, `matchedIn`	ranking score + 一致箇所
`totalReturned`	hits.length
`indexBuiltAt`, `indexItemCount`, `indexPath`	index メタデータ
`honestScope`	制約明示 (regex parser + syntactic proxy + substring only)

Filter option

proofStatus — csv (proved,hypothesis,speculative の subset)
source — csv (seed-kernel,lean4-collatz-rei の subset)
lean4Only — true = Lean 4 decl に限定
provedOnly — proofStatus=['proved'] の shorthand
unverifiedOnly — Lean 4 で sorry を含むもののみ
namespace — namespace substring (case-insensitive)
excludeRefuted — extra.refuted=true の SEED を除外

Honest scope (譲れない線、 v0.1)

Lean 4 parser は regex-based で elaborator ではない。 lean4Verified=true は「コメント除去後の本体に sorry が無い」の syntactic proxy、 lake build / #print axioms guarantee ではない。
Axiom decl は hypothesis 分類 — Rei style の axiom goldbach_conjecture : ... は「statement を記録して証明を defer」の意味、その予想が他所で証明されているかどうかとは無関係。
SEED_KERNEL default は speculative。 STEP 1276 の judgmentStatus field が明示 set されていない限り、 SEED が Rei stack の load-bearing でも Lean 4 proof とは同一視しない。
Substring ranking のみ — trigram / semantic embedding は v0.2+ scope。 7,466 items で LIKE 検索は < 20 ms。

Rei stack 位置付け

2026-08-19 合意 Order 原則: ローカル CLI が「手が速くなる」 verify → MCP → find_gaps → dep-graph 解析。本 tool は段 1 + 段 2。

段 1 CLI: 2026-08-19 実装 (49/49 test PASS)
段 2 MCP wrap: 2026-08-20 (3484e266b)
段 3 find_gaps: 同 commit
段 4 audit_gaps: 0022af11e

詳細は 2026-08-20 三段 arc research-log 参照。