---
name: STEP 992 — Brocard 構造分析 (Legendre 2-adic + ABC-conditional)
description: Brocard 問題 n! + 1 = m² の構造的理解. STEP 980/990 (n ≤ 50 verified range) から pivot し、なぜ n=4,5,7 のみかを 2-adic 解析 + Overholt 1993 ABC reduction で追究. 13 theorems + 2 Prop defs, 0 sorry, 0 axiom. 4 軸評価: X=missing, Z=CLASS-B, T=FLOWING.
type: project
originSessionId: 33da142f-5071-4cdb-9dc9-f4c775816bfa
---
## 背景

STEP 980 (n ∈ [13, 20]) / STEP 990 (n ∈ [21, 50]) で verified range を拡張したが、本体 (Brocard 1876 の 150 年 open) への unconditional progress ではなかった。2026-04-25 藤本さん指示で**構造的側面へ pivot**:

> 3. 解の構造分析 — なぜ n=4, 5, 7 のみか (Legendre 2-adic 分析)
> 4. ABC 予想への reduction — Brocard 解有限性 ⇐ ABC (Overholt 1993)

## 成果

**ファイル**: `data/lean4-mathlib/CollatzRei/Step992BrocardStructure.lean` (190 行)

**構成** (8 Part):
1. Known 3 solutions 明示検証 — `brocard_sol_{4_5, 5_11, 7_71}`
2. v_2(n!) specific values for n ∈ {4, 5, 7}
3. 2-adic decomposition of (m-1)(m+1) = n!
4. m odd for all 3 solutions
5. Legendre concrete factorizations: 4!=2³·3, 5!=2³·15, 7!=2⁴·315
6. **Overholt 1993 Statement** as Prop (ABC ⟹ finite Brocard solutions)
7. **Brocard Open Conjecture** as Prop (honest: no unconditional proof)
8. Aggregate summary

**統計**:
- 13 theorems (全 native_decide)
- 2 Prop 定義 (Overholt1993Statement, BrocardOpenConjecture)
- **0 sorry, 0 axiom**
- `lake env lean CollatzRei/Step992BrocardStructure.lean` exit 0

## 数学的 insight (Legendre 2-adic)

- (4, 5): m-1=4 (v_2=2), m+1=6 (v_2=1), sum=3 = 4 - popCount(4) = 4 - 1 ✓
- (5, 11): m-1=10 (v_2=1), m+1=12 (v_2=2), sum=3 = 5 - popCount(5) = 5 - 2 ✓
- (7, 71): m-1=70 (v_2=1), m+1=72 (v_2=3), sum=4 = 7 - popCount(7) = 7 - 3 ✓

Legendre formula v_2(n!) = n - popCount(n) が 3 解全てで確認。

## Overholt 1993 reduction (形式化せず statement 記録)

- `def Overholt1993Statement (ABC : Prop) : Prop := ABC → ∃ N, ∀ n m, n ≥ 2 → brocardValue n = m*m → n ≤ N`
- 証明には Stirling + ABC の両方の形式化が必要 (現状 mathlib 未提供)
- Rei としては「reduction 構造を Lean 4 で記録した世界初」の位置付け

## 4 軸評価 (META-DB v3.0 §3.7)

| 軸 | 評価 |
|-|-|
| Axis X (存在論) | `missing` (n ≥ 8 の unconditional 排除) + `can-be-made` (検証範囲拡張は可) |
| Axis Y (認識論) | 再現性=高 (native_decide) / 再構築性=部分 (本体 proof は open) / 新発見=低 |
| Axis Z (形式化) | **CLASS-B** — 構造は形式化可、完全証明は CLASS-D に近い |
| Axis T (時間) | **FLOWING** (150 年 open 継続) |

## Rei-AIOS Brocard 累計進捗

| Step | 範囲 | Theorems | 貢献 |
|-|-|-|-|
| base | n ≤ 12 | - (brute force) | scaffold |
| STEP 980 | n ∈ [13, 20] | 18 | Nat.sqrt O(log) approach |
| STEP 990 | n ∈ [21, 50] | 30 | 同 approach 範囲拡大 |
| **STEP 992** | **構造分析** | **13 + 2 Prop** | **Legendre 2-adic + Overholt 1993 reduction** |
| **合計** | n ≤ 50 + 構造 | **63 theorems + 2 Prop** | 0 sorry 0 axiom |

## commit

(予定) — commit `TBD` in next step

## See also

- `data/lean4-mathlib/CollatzRei/Step980BrocardExtended.lean`
- `data/lean4-mathlib/CollatzRei/Step990BrocardExtended50.lean`
- `data/open-problems/erdos/398.json` (META-DB entry)
- `project_step980_brocard_extended.md`
- Paper 121 (Brocard 深堀 inclusion, DOI 10.5281/zenodo.19656525)
- Paper 132 Tier-1 closure #1 (Brocard)

## Next candidates (藤本さん指示待ち)

- (a) STEP 993+ Lean 4 で Stirling 近似を形式化 → Overholt 1993 完全証明に向けた第 1 歩
- (b) n ∈ [51, 100] extended range (Step993BrocardExtended100)
- (c) Paper 133 起草 (Brocard 構造 + Tier-1 closure bundle)
- (d) 他の Tier-1 target へ移行