---
name: STEP 1015 Brocard 拡張 n ≤ 110
description: Paper 132 Tier-1 closure 続編. Brocard's problem を n=101..110 に Lean 4 拡張. 13 theorems / 0 sorry / build 5.4s 成功. Rei Brocard 累計 102→115 theorems
type: project
originSessionId: d379da7b-dcdc-4417-a2fd-4168f498debb
---
# STEP 1015 — Brocard's Problem n ∈ [101, 110] Lean 4 拡張 (2026-05-01)

## 概要

Paper 132 Tier-1 closure 路線の続編 (前回 STEP 993 で n ≤ 100 完了).
Brocard's problem (1876 開) を **n=101..110 に拡張**, 全 build 通過.

## 結果

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

## 構造

### Layer 1: Sqrt-based non-square (10 theorems)

```lean
theorem brocard_n101_sqrt_ne :
    Nat.sqrt (brocardValue 101) * Nat.sqrt (brocardValue 101) ≠ brocardValue 101
  := by native_decide
-- ... n102 through n110
```

### Layer 2: Bridge to ∀-form (3 theorems)

`sqrt_not_square_impl` (Step980 定義) は signature `∀ m : Nat, m * m ≠ k`:

```lean
theorem brocard_n101_no_square : ∀ m : Nat, m * m ≠ brocardValue 101 :=
  sqrt_not_square_impl _ brocard_n101_sqrt_ne
-- ... n105, n110
```

### Layer 3: Spot-check summary (1 theorem)

n=101/105/110 の AND 結合 (確認用).

## 重要技法

- **Nat.sqrt-based O(log) approach** (Step980 で確立) を継続使用
- native_decide が n=110 (n! ≈ 1.59 × 10^178) でも 5.4s で通る
- **import 削減**: `Step993BrocardExtended100` は不要 (brocardValue/sqrt_not_square_impl は Step980 にあり), 削除で olean 依存リスク回避

## ⚠️ Build 検証時の罠

最初 `lake env lean` 実行で「Step993...olean does not exist」エラー. 原因:
- Step1015 の `import CollatzRei.Step993BrocardExtended100` が冗長 (Step980 で十分)
- Step993 の olean が cache 未生成だった

**教訓**: 新規 Lean ファイルの import は **最小依存** に絞る. 既存 Step ファイルからの「念のため import」が build cache 不在を露呈する.

## Honest positioning

- **Berndt-Galway 2000**: N ≤ 10⁹ (Brocard's problem search limit) — Rei n=110 は遥か手前
- **Rei contribution**: Lean 4 mechanical verification first record continues
- **Brocard's problem 自体は 1876 以来 OPEN**, 本拡張は **計算的検証範囲のみ拡大**

## ファイル

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

## 関連 STEP / Paper

- STEP 980 Brocard n ∈ [1, 20] — sqrt-based 起点
- STEP 990 Brocard n ∈ [21, 50]
- STEP 993 Brocard n ∈ [51, 100]
- STEP 992 Brocard 構造分析 (Legendre 2-adic + Overholt 1993 ABC)
- Paper 132 (DOI 10.5281/zenodo.19704359) Tier-1 closure roadmap
- Paper 133 (Sylvester-Schur Lean 4 partial + 699↔961 bridge)

## Next step candidates

1. n=111..120 (Step1016) — 同パターンで継続容易
2. n=200 までの一気拡張 (50 theorems) — native_decide 時間 risk
3. Brocard 構造証明 (Step992 拡張) — Legendre 2-adic 強化
4. 別 Tier-1 (EGZ E(ℤ_5), Schur S(5)) — 新規前進