# STEP 1949 — lean4-mathlib-pilot-detector (v0.3 lite)

**Timestamp**: 2026-09-11T00:40 (JST)
**Tab worktree**: main (rei-aios-9b)
**Commit**: (this commit)

## 一行 summary

`scripts/lean4-mathlib-pilot-detector.ts` 実装 → 510 file 中 310 が isolated (60.9%) 判明、Rei per-STEP proof style の 実測、cleanup 素朴適用不能。

## 主要 finding / evidence

- **Tool**: `scripts/lean4-mathlib-pilot-detector.ts` (185 line) — grep-based Lean import 逆参照検知、`--tsv` + `--json` 出力
  - Scan: 509 .lean files under `data/lean4-mathlib/` (0.1s)
  - Enrich pilots-only with `git log -1` per file (~140s for 310 files)
- **Finding**: **310 / 509 (60.9%) が isolated** (0 incoming imports、root `CollatzRei` module 除外後)
  - Stale (>60d) filter で **213 files** (41.8%)
- **Root cause of high isolation rate**: Rei の Lean 4 methodology は **per-STEP proof exhibit style** — 各 `Step<N>*.lean` / `Problem<N>*.lean` / `<Topic>Bridge.lean` は STEP 出力 record として standalone、library building block ではない。Paper 側 は path 直接引用、import は しない。従って「isolated ≠ actionable cleanup」
- **Adjusted finding**: pilot detector は **screening 用 review tool** として value あり、**auto-cleanup source として不適合**
- **★ STEP 1947 A verdict corrigendum**: sample row 11 `SnstRealComparison.lean` を A (ACTIONABLE_CLEAN) と 判定したが、file 冒頭 30 行を読んだ結果 substantive pilot (STEP 1228e、8 theorem、explicit "pilot" 記述、load-bearing evidence、`別 AI 指摘 (load-bearing)` = 未来 revisit path 想定) と判明、cleanup 保留 が 正解。my verdict was **over-eager without file-content check**。karpathy watch の A verdict は 引き続き妥当 (dormant config、substantive content なし)。

## Honest scope

- **主張しないこと**:
  - この detector は「actionable cleanup 候補」を出さない、「isolated in import graph」だけを出す
  - 「isolated」判定は local Lean import (project 内) のみ、Mathlib upstream 逆参照 は不明 (irrelevant to Rei code)
  - 「isolated + stale」でも「pilot」でもない = 「STEP 完了後の 静的 proof exhibit」多数、これは cleanup 対象では ない
  - 60.9% 高い isolation rate は Rei の 内在 style、bug ではない
- **予測との差**: STEP 1948 で「v0.3 pattern 1 = Lean import-graph reader」で pilot 検出できる 見通し、実測は **概念適用不能** (methodology mismatch)。理由 = Rei の Lean は「library building」ではなく「STEP 出力 archive」paradigm。
- **手法制約**:
  - Grep-based import 検知は comment 内の `-- import X` を carve out しない (実測 false negative 影響 negligible)
  - 動的 import (macro / attribute) は捕捉不能 (Rei は使用 negligible)
  - Mathlib prep 系 file は 「Mathlib 上流 target」 として isolated だが 意図的 = cleanup 対象では ない

## Failure mode (機械学習用 dataset)

- **(oo) methodology assumption drift**: v0.2 land 時「lean4-mathlib の 297 stable proof」を想定 = 「library-style 相互 import」と 前提していた、実測は「per-STEP exhibit style = 相互 import 少」。私の 想定は 一般 Lean project style に引きずられた、Rei-specific style を 事前観察 せず。Prevention: Rei 固有 code base に device 導入前 に、代表 file を N 個 sample read で methodology assumption を verify (30 秒 self-check)。
- **(pp) file-content-check なし での A verdict 過剰**: STEP 1947 row 11 SnstRealComparison を A と判定、file 冒頭 read せず、auto-signal (semantic_grep=0) だけで判断。実測 file は substantive pilot with load-bearing content。Prevention: destructive 提案 (A verdict = cleanup 提案) を出す前に 対象 file を必ず head-Read (30 行)、docstring / comment header で 意図確認。
- **(qq) prediction over-confidence in 未検証 methodology**: STEP 1948 で「pattern 1 pilot detection で lean4-mathlib 60 files actionable」予測、実測は「detection 概念 適用不能」。Prevention: prediction 提示 時、対象 methodology を「1 サンプル観察」で 事前 verify、未 verify なら prediction range に「概念 適用不能 (低 P) の 可能性」を含める。

## 詳細参照 (任意)

- Tool: `scripts/lean4-mathlib-pilot-detector.ts` (185 line、grep-based import 逆参照検知)
- Output artifacts:
  - `data/orphan-gauge/step-1949/pilots.tsv` (310 pilots, 8-col: path / module / size / mtime / out_count / in_count / commit / subject)
  - `data/orphan-gauge/step-1949/pilots.json` (structured summary + full pilot list)
- 関連 STEP: STEP 1926 (device v0.1)、STEP 1947 (50-sample calibration)、STEP 1948 (v0.2 archive detection)、STEP 1228e (SnstRealComparison origin)

## 追加 section — deferred v0.3 patterns

STEP 1948 で提案した v0.3 (2) (3) は 本 STEP で **defer 継続**:
- **Pattern (2)**: `data/*/latest.json` conditional archive → v0.4 candidate、trigger = latest.json fetcher script の absence 判定 が要る
- **Pattern (3)**: STEP N filename → 上記 methodology insight で 不要判明 (Step\d+_ snake_case は data/lean4-transfer/** = v0.2 で既 covered、PascalCase Step\d+ は valid STEP-exhibit で cleanup 対象では ない)

**v0.3 は landing point としては pilot detector のみ**、cleanup pattern の refactor は しない。真の cleanup guidance には Lean file の docstring parsing (「pilot」keyword 検知) が要る = v0.4+ candidate。

## Meta finding — Rei methodology の 外化

本 STEP は device 改善 arc として 起票したが、実際に land した value は **「Rei の Lean 4 methodology を data で可視化した」** insight。60.9% isolated = per-STEP exhibit style の quantitative evidence。この insight 自体が Paper / SEED_KERNEL memory 候補として意味あり (Rei code style の 定量 characterization、外部 explainable)。cleanup tool として使えなくても、meta-tool として value がある。