---
name: STEP 979 — Wikipedia shim sweep (Paper 132 Part F.4 実行)
description: META-DB ingestion artifact の広域 sweep 完了。5 新規汚染修正 + 再発防止 tool `scripts/sweep-wikipedia-shims.ts` 構築。全 9 shim が正しく corrected tag 付きへ。
type: project
originSessionId: 2812f631-04af-4dd8-a8cd-4f872e1e1383
---
# STEP 979 — Wikipedia shim sweep

## 動機
Paper 132 Part F.4 の "structural lesson":
> Ingest scripts should never record sorryCount from a file whose non-import body is zero-length without flagging it.
> A follow-up STEP should audit the META-DB for other Wikipedia-shim artifacts.

## 実行結果

### 検出された shim (9 件 / 116 Wikipedia/*.lean 中)

**既 corrected (Paper 132 時点で修正済)**: 4
- ErdosRadoSunflowerConjecture → ErdosProblems/20.lean (sorry 2)
- HadwigerNelson → ErdosProblems/508.lean (sorry 5)
- HappyEndingProblem → ErdosProblems/107.lean (sorry 7)
- HerzogSchonheimConjecture → ErdosProblems/274.lean (sorry 4)

**新規発見・修正 (STEP 979)**: 5
| JSON | Import target | sorry 0→ | p 0.95+→ |
|------|---------------|---------:|---------:|
| brocardproblem.json | ErdosProblems/398.lean | **2** | 0.45 |
| hilbertfifthproblem.json | HilbertProblems/5.lean | **5** | 0.40 |
| minimaloverlapproblem.json | ErdosProblems/36.lean | **21** | 0.55 |
| nothreeinlineproblem.json | GreensOpenProblems/72.lean | **7** | 0.50 |
| sparseruler.json | ErdosProblems/170.lean | **2** | 0.50 |

**合計新規 37 attack targets** を META-DB に正しく計上。

## 恒久ツール

`scripts/sweep-wikipedia-shims.ts`:
- 全 Wikipedia/*.lean を走査
- 正規表現 `^(theorem|lemma|def |noncomputable def|structure) ` で declaration 有無判定
- `import FormalConjectures.X.«N»` から実 target path 解決
- 対応 META-DB JSON の sorryCount vs 実体比較
- `corrected:` tag 付きは skip (rerun-safe)
- **contaminated があれば exit 1** (CI 組込可)

`npm run sweep:wikipedia-shims` で実行可能。

## 追加 known_progress (5 件に加筆)

- Brocard: Berndt-Galway 2000 (N ≤ 10⁹), Ramanujan 1913
- Hilbert-Smith: Gleason-Montgomery-Zippin 1952 (Hilbert 5 本体), Pardon 2013 (3-manifold), Myers-Steenrod (Riemannian case)
- MinimalOverlap: Erdős 1955 / Scherk 1955 / Świerczkowski 1958 / Motzkin-Ralston-Selfridge 1956 / Haugland 1996, 2022 / White 2022 (範囲 [0.379005, 0.3809268534330870])
- NoThreeInLine: Dudeney 1917 / Erdős 1951 / N ≤ 60 pre-2000 / **Grebennikov-Kwan 2025 arXiv:2510.17743 (k > 10³⁷)**
- SparseRuler: Erdős-Gál 1948 / Leech 1956 / Wichmann 1963

## Paper 133 新 Tier-1 候補

本 sweep で明確化した追加 attack surface:
- **M(1)=1..M(5)=3** (MinimalOverlap): 5 件 native_decide Finset 全列挙
- **allowedSetSize_le** (NoThreeInLine): pigeonhole 初等的証明
- **Brocard n ≤ 100 numerical**: Nat.factorial + Nat.sqrt decidable
- **trivial_ruler_is_perfect** (既 proved, SparseRuler): 参考パターン

## commit
- `d0d17ea` STEP 979: 5 JSON fix + sweep tool + package.json script
- rerun check: "All 9 shims corrected, Contaminated=0" ✓

## 学び

Paper 132 Part K (computational poetics) が述べた "counted-zero vs defaulted-zero" の区別を、本 STEP 979 で tool 化。META-DB schema 本体には未だ `sorryCount: { value, source }` の分離は入れていないが、**runtime detector** でカバー。

将来の ingest script 変更時は `sweep-wikipedia-shims.ts` を pre-commit / CI gate として活用すれば再発防止。