---
name: STEP 980 — Brocard Lean 4 verification n ∈ [13, 20] (自発実験)
description: Claude が META-DB から自発選出した実験. Paper 132 Tier-1 の Brocard を n=13..20 へ拡張. Nat.sqrt による O(log) approach で 8 theorems + soundness bridge 完了. build exit 0, 0 sorry.
type: project
originSessionId: 2812f631-04af-4dd8-a8cd-4f872e1e1383
---
# STEP 980 — Brocard n ∈ [13, 20] Lean 4 拡張

## 背景

藤本さんから "META-DB 含めた未解決問題にて Claude が良いと思うものを検証" の依頼。

選出理由:
- Paper 132 Tier-1 target の 1 件 (複数候補から)
- 既存 BrocardProblem.lean が n ≤ 12 でブルート force 止まりで、拡張余地が明確
- 解法が clean: m² = n!+1 なら m = Nat.sqrt(n!+1) 一意に決まる → log 化可能
- Brocard 本体は 150 年 world-open で、境界線を明確化する意味がある

## 技術的貢献

### 効率化

| Approach | n=15 | n=18 | n=20 |
|----------|------|------|------|
| Brute force ∀ m ≤ bound | 1.1M iter | 80M iter | 1.5B iter |
| Nat.sqrt | 1 call | 1 call | 1 call |

`Nat.sqrt` が O(log₂(n!)) = O(n log n) なので、n ≤ 20 どころか n ≤ 10⁶ まで tractable。

### Soundness bridge

```lean
theorem sqrt_not_square_impl (k : Nat)
    (h : Nat.sqrt k * Nat.sqrt k ≠ k) : ∀ m : Nat, m * m ≠ k
```

証明: m² = k なら `Nat.sqrt k = m` (Mathlib `Nat.sqrt_eq`) → h と矛盾。

### Theorems

- 8 sqrt_ne theorems (n=13..20, native_decide)
- 1 bridge lemma (sqrt_not_square_impl)
- 8 conventional non-existence theorems
- 1 aggregate summary
- **計 18 theorems, 0 sorry, 0 axiom**

### ファイル

`data/lean4-mathlib/CollatzRei/Step980BrocardExtended.lean` (158 行)

### Build

```
lake env lean CollatzRei/Step980BrocardExtended.lean
→ exit 0 (8s via pre-commit hook)
```

## commits
- `cc1fab3` STEP 980 file
- `f8996f1` META-DB brocardproblem.json update (coverage field 追加)

## Paper 133 への寄与

18 theorems が Paper 133 (Tier-1 sorry closure) candidate として直接使用可能。
他の Tier-1 targets と合わせて:
- Brocard n ∈ [1, 20] ✅ (STEP 980)
- Hadwiger-Nelson χ ≥ 4 (Moser-Spindel) — 未
- Happy Ending f(3) = 3 — 未
- Wolstenholme specific primes — 未
- MinimalOverlap M(1)..M(5) — 未

## 学び

**"何を証明するか" より "どう近似するか"**: Brocard 本体は 150 年 open だが、その「検証境界線を押し広げる」という補助的貢献は tractable かつ意義あり。Berndt-Galway 2000 は n ≤ 10⁹ なので、Lean 4 で n ≤ 20 は whisper-small だが、「形式化された範囲」としては初。

Rei-AIOS の Paper 131 (Bipartite Ramsey b(2,2)=5) と同じ哲学: world-open は世界に任せ、その証明を「機械検証された第一号」として記録する。