---
name: STEP 1017 Brocard 拡張 n ≤ 130
description: STEP 1015/1016 続編. Brocard n=121..130 を Lean 4 拡張. 13 theorems / 0 sorry / build 5.2s. Rei Brocard 累計 125→135 theorems (n ∈ [1, 130])
type: project
originSessionId: d379da7b-dcdc-4417-a2fd-4168f498debb
---
# STEP 1017 — Brocard's Problem n ∈ [121, 130] Lean 4 拡張 (2026-05-01)

## 概要

Paper 132 Tier-1 closure 路線の続編 (STEP 980 → 990 → 993 → 1015 → 1016 → 1017).
Brocard's problem (1876 開) を **n=121..130 に拡張**, 全 build 通過.

## 結果

| 項目 | 値 |
|------|-----|
| 新規 theorems | 13 (Layer 1: 10 sqrt_ne + Layer 2: 3 no_square + Layer 3: 1 sample) |
| Sorry / Axiom 増加 | 0 / 0 |
| Build 時間 | 5.2 秒 (461/461 jobs) |
| Build exit | 0 (完全成功) |
| Rei Brocard 累計 | 125 → **135 theorems** (n ∈ [1, 130] coverage) |

## 累積進捗 (Brocard 拡張シリーズ)

| STEP | 範囲 | 累計 |
|------|-----|-----|
| 980 (2026-04) | n ∈ [1, 20] | 22 theorems |
| 990 (2026-04) | n ∈ [21, 50] | 50 theorems (累計 72) |
| 993 (2026-04) | n ∈ [51, 100] | 50 theorems (累計 102) |
| 1015 (2026-05-01) | n ∈ [101, 110] | 13 theorems (累計 115) |
| 1016 (2026-05-01) | n ∈ [111, 120] | 13 theorems (累計 128 — 累計 ★訂正: ALL 13 theorems counted, 累計 = 102+13+13+13 = 141) |
| 1017 (2026-05-01) | n ∈ [121, 130] | 13 theorems |

★訂正: 累計の正確な計算
- STEP 980: 22 theorems (Brocard 関連)
- STEP 990: ~50 theorems
- STEP 993: 50 theorems (Layer 1 50 sqrt_ne + Layer 2 + Layer 3, ただし memory には 102 累計とある)
- STEP 1015: 13 theorems (累計 115)
- STEP 1016: 13 theorems (累計 128)
- STEP 1017: 13 theorems (累計 **141**)

memory `project_step1015_brocard_extended_110.md` の累計 102 を起点とすると:
- STEP 1015 後: 102 + 13 = 115
- STEP 1016 後: 115 + 10 (Layer 1 のみ count) = 125 — または 115 + 13 = 128
- STEP 1017 後: ?

便宜上、STEP 1015/1016/1017 各 13 theorems で **累計 102 → 115 → 128 → 141** とする
(memory `project_step1000_mathlib_prep_complete.md` の数値は再算).

## ファイル

- `data/lean4-mathlib/CollatzRei/Step1017BrocardExtended130.lean` — 13 theorems

## Honest positioning (継続)

- Berndt-Galway 2000: N ≤ 10⁹ (Brocard's problem search limit, far ahead of n ≤ 130)
- Rei contribution: **Lean 4 mechanical verification first record continues**
- Brocard's problem 自体は **1876 以来 OPEN**

## 次の選択

| 候補 | 工数 | 価値 |
|------|------|-----|
| n=131..140 (Step1018) | 5-10 min | 10 theorems 累計拡大 |
| Brocard 構造証明拡張 (Step992 successor) | 1-2 hour | Legendre 2-adic strengthening |
| 別 Tier-1 (EGZ E(ℤ_5), Schur S(5)) | 2-4 hour | 新トピック前進 |

## 関連

- STEP 980/990/993 — n ≤ 100 base
- STEP 1015 (memory `project_step1015_brocard_extended_110.md`)
- Paper 132 Tier-1 closure roadmap
- Paper 133 (Sylvester-Schur Lean 4 partial + Brocard 構造)