---
name: Legendre's Conjecture Deep Dive (2026-04-19 深夜 STEP 929)
description: Legendre's conjecture n ≤ 10^4 verified (0 violations), mod-96 asymmetry found, Lean 4 LegendreSmall zero-sorry for n ≤ 100, cross-connection witness(24)=577 to peak 9232.
type: project
originSessionId: 79081859-fd56-4821-a0d2-932be27d647a
---
# Legendre's Conjecture Deep Dive — STEP 929

## 対象問題

**Legendre's conjecture (1808, OPEN 218 年)**:
  ∀ n ≥ 1, ∃ prime p with n² < p < (n+1)².

## 本 session 成果

### 1. 数値検証 (`scripts/legendre-verify-rei-lens.ts`)

- **n ∈ [1, 10,000] で 0 violations** ✅
- Elapsed 6 秒 (Miller-Rabin 決定論)
- count distribution: 1 interval は count=2 minimum
- Legendre は Oppermann より弱い claim (≈interval length 2倍)

### 2. Rei mod-96 lens (exploratory)

Min-prime in (n², (n+1)²) の mod 96 residue 分布:

**Top-5 (頻出 residues)**:
- r=5: 5.92% (avg offset 7.1)
- r=7: 5.47% (avg offset 8.0)
- r=11: 5.41% (avg offset 9.5)
- r=17: 4.54% (avg offset 11.1)
- r=19: 4.37% (avg offset 13.9)

**Bottom-5 (稀な residues)**:
- r=1: 1.68% (avg offset 16.9)
- r=73: 1.66% (avg offset 20.3)
- r=91: 1.55% (avg offset 23.7)
- r=95: 1.29% (avg offset 27.3)

**観察**: 頻出 residues は {5, 7, 11, 17, 19} = 小さな素数本体. 稀な residues は offset が大きい (例: r=95 で avg 27.3). 非対称性は Oppermann primeHi +14.97% (STEP 927) に匹敵する exploratory finding.

### 3. Lean 4 `LegendreSmall.lean` (11 theorems, zero-sorry)

**File**: `data/lean4-mathlib/CollatzRei/LegendreSmall.lean`

- `WITNESSES_100 : List (Nat × Nat)` — n ∈ [1, 100] の explicit 素数 witness
- `WITNESSES_100_all_valid` — 全 witness が `n² < p < (n+1)²` AND Nat.Prime を満たす
- 11 theorems all zero-sorry via native_decide / decide
- Build time 7 秒 under Mathlib v4.27.0

### 4. ★ 予期しない cross-connection (Paper 118 接続) ★

**witness(24) = 577** が、Paper 118 Closure 5 の **peak 9232 = 2⁴·577** の素数因子と完全一致.

- Legendre witness: n=24 の最小素数 = 577 (24² = 576 なので 577 が直接隣接)
- Paper 118 peak 9232 の素数因子 = 577 (17 atomic cores 全 orbit の global peak)
- 両者は一見独立な異なる問題 (Legendre 1808 vs Collatz 1937)

Lean 4 で形式化:
```lean
theorem legendre_24_and_peak_9232_link :
    (24, 577) ∈ WITNESSES_100 ∧ 9232 = 2^4 * 577 := by
  refine ⟨?_, ?_⟩ <;> decide
```

## 新規 AI 生成の未解決問題 (Q19-Q21)

**Q19**: Legendre min-prime mod 96 の top-5 {5, 7, 11, 17, 19} vs bottom-5 {1, 73, 91, 95} 非対称性は Chebyshev-type bias の結果か、それとも Rei-specific structural phenomenon か?

**Q20**: Legendre witness (min prime in (n², (n+1)²)) は Oppermann upper interval [n², n²+n] の min prime と常に一致するか? (後者区間が前者に含まれる n について)

**Q21**: witness(n=24) = 577 と peak 9232 = 2⁴·577 の接続は coincidence か structural か? Legendre witness が "Rei Collatz peak factor" と一致する n のリストは何か? (empirical scan 要)

## D-FUMT₈ 状況

| 項目 | state | 進捗 |
|---|---|---|
| Legendre n ≤ 10⁴ 検証 | TRUE | 0 violations |
| Legendre 全般 (∀n) | NEITHER | 218 年間 open |
| Lean 4 witnesses n ≤ 100 | TRUE | 11 zero-sorry |
| Q19 mod-96 bias causal | NEITHER | 新規提起 |
| Q20 Oppermann overlap | NEITHER | 新規提起 |
| Q21 witness(24)=peak(9232) 構造性 | BOTH | numerical coincidence confirmed, structural unknown |

## 次 session 候補

1. Legendre n ≤ 10⁶ 拡張検証 (60-120 秒スケール)
2. Q21 scan: peak prime (Paper 118 F9 top-10 prime list) と Legendre witness の overlap
3. Paper 120 草稿 (Paper 119 Q14-Q18 + Legendre Q19-Q21 + Collatz Q10-Q12 retry)

## 成果物

- `scripts/legendre-verify-rei-lens.ts` — 検証 + mod-96 分析
- `scripts/legendre-witness-generate.ts` — Lean 4 witness 生成
- `data/lean4-mathlib/CollatzRei/LegendreSmall.lean` — 11 zero-sorry theorems
- `data/legendre/verify-report.json` — 検証データ
- `project_legendre_deep_dive.md` — 本 memo