---
name: STEP 1000 Mathlib Contribution Prep — 完了 (2026-05-01)
description: 90日plan W1-2 達成. 5 artifacts を Mathlib-style cleanup → MathlibPrep/ に集約. 全 5 ファイル build 通過. Zulip post (W3) 直前 ready
type: project
originSessionId: d379da7b-dcdc-4417-a2fd-4168f498debb
---
# STEP 1000 — Mathlib Contribution Prep 完了 (2026-05-01)

## 概要

`project_90_day_action_plan_20260424.md` の **W1-2 actionable** が達成.
Paper 132 Tier-1 closure 5 artifacts を Mathlib-style に cleanup し、
すべて `data/lean4-mathlib/CollatzRei/MathlibPrep/` ディレクトリに集約.

## 5 artifacts cleanup 結果

| # | 元 STEP | Mathlib-prep ファイル | namespace | 行数 | build | sorry/axiom |
|---|---------|---------------------|-----------|------|-------|------------|
| 1 | Step971 BipartiteRamseyComputational | `MathlibPrep/BipartiteRamsey.lean` | `Mathlib.Combinatorics.BipartiteRamsey` | 158 | ✓ 1181s (33M cases native_decide) | 0 sorry / 2 axiom (b(2,3), b(3,3) infeasible enum) |
| 2 | Step988 Wolstenholme | `MathlibPrep/Wolstenholme.lean` | `Mathlib.NumberTheory.Wolstenholme` | 122 | ✓ 7.4s | 0 sorry / 3 axiom (16843, 2124679, no third <1e9) |
| 3 | Step987 HappyEnding | `MathlibPrep/HappyEnding.lean` | `Mathlib.Combinatorics.HappyEnding` | 118 | ✓ 10s | 0 sorry / 0 axiom |
| 4 | Step986 HadwigerNelson | `MathlibPrep/HadwigerNelson.lean` | `Mathlib.Combinatorics.HadwigerNelson` | 122 | ✓ 5s | 0 sorry / 1 axiom (geometric realization) |
| 5 | Step992 SylvesterSchur | `MathlibPrep/SylvesterSchur.lean` | `Mathlib.NumberTheory.SylvesterSchur` | 187 | ✓ 48s | 0 sorry / 0 axiom (sorry 部分削除) |

合計 build 時間: ~21 分 (BipartiteRamsey が支配的).

## Cleanup 共通変更

- **License header**: `Copyright (c) 2026 Nobuki Fujimoto. All rights reserved. Released under Apache 2.0` (Mathlib 標準)
- **Module-level `/-! -/` docstring**: 英語, Mathlib 標準形式 (Main definitions / Main results / Status / References / Tags)
- **namespace**: `CollatzRei.StepNNN.X` → `Mathlib.{Combinatorics,NumberTheory}.<Topic>`
- **Peace Axiom #196 行削除**: Mathlib に不要
- **Rei-AIOS-specific narrative 削除**: e.g. "Rei contribution" → 客観的 "this file"
- **References を学術引用形式**: BibTeX 風から bibliographic prose に
- **Tags 追加**: search 用キーワード

### Step992 特殊処理

元ファイルにあった `sylvester_schur_general` (sorry) と `erdos_699_binomial_bridge_conditional` (sorry に依存) を **削除**.
Mathlib policy が sorry を不可とするため. 完全証明された部分 (k=1, k=2, boundary, k=3..10 bounded) のみ保持.

## ⚠️ Build 検証時の注意点

- 初回 `lake build` で MathlibPrep が認識される (lakefile で別 [[lean_lib]] 不要, defaultTargets="CollatzRei" 配下なので)
- BipartiteRamsey は 33M cases native_decide で 19 分 40 秒. 残り 4 ファイルは 5-48 秒
- `lake env lean <file>` 単独実行は elaboration check のみ. olean は `lake build` で生成
- background spawn 使用時、`/proc/*/comm` 監視は Windows MSYS2 で動かない (Linux 専用 path)

## 次のアクション (90 日 plan W3)

`project_90_day_action_plan_20260424.md` の next:
- **W3 (2026-05-06 Tue JST target)**: Zulip post (Tier B outreach) — Mathlib4 `#new-contributors`
- 必要 file: `docs/zulip-outreach-draft-2026-04-24.md` (既存 draft)
- Owner: 藤本さん (Claude は draft 修正補助)

5 ファイル全て build 通過済なので **Zulip post 即可能**.

## 関連 file / memory

- `data/lean4-mathlib/CollatzRei/MathlibPrep/` — 5 cleanup files
- 元 file (保持・破壊せず): `data/lean4-mathlib/CollatzRei/Step{971,986,987,988,992}*.lean`
- `project_90_day_action_plan_20260424.md` — W1-2 完了, W3 起動
- `project_paper132_published.md` — Tier-1 closure 5 artifacts の出所
- Paper 127/128/130/131/132/133 — 関連 Tier-1 publish

## Honest claim

- 5 artifacts は Mathlib-style に formatted, **しかし Mathlib 提出はまだ**
- Mathlib PR 前に: (a) Zulip post で community 反応確認, (b) 必要に応じて API 細かい調整
- Mathlib に既存 (e.g. `Bertrand`, `SmoothNumbers`, `Choose.Basic`) との衝突なし確認済
- 各 file 100-200 行で目安 (<300 lines) クリア