English
If p ≥ 3 and the Mersenne number mersenne(p) is prime, then the Lucas–Lehmer test holds for p.
Русский
Если p ≥ 3 и число Мерсенна mersenne(p) простое, то тест Лукас–Леммера выполняется для p.
LaTeX
$$$p \ge 3 \ \&\& \ \text{mersenne}(p) \text{ prime} \Rightarrow \text{LucasLehmerTest}(p)$$$
Lean4
/-- If `2^p-1` is prime then the Lucas-Lehmer test holds, `s(p-2) % (2^p-1) = 0. -/
theorem lucas_lehmer_necessity (p : ℕ) (w : 3 ≤ p) (hp : (mersenne p).Prime) : LucasLehmerTest p :=
by
have : Fact (mersenne p).Prime := ⟨‹_›⟩
set p' := p - 2 with hp'
clear_value p'
obtain rfl : p = p' + 2 := by cutsat
dsimp [LucasLehmerTest, lucasLehmerResidue]
rw [sZMod_eq_s p', ← X.fst_intCast, X.closed_form, add_tsub_cancel_right]
have :=
X.ω_pow_trace (q := mersenne (p' + 2)) (by simp)
(legendreSym_mersenne_three w <| hp.of_mersenne.odd_of_ne_two (by cutsat)) (legendreSym_mersenne_two w)
(by simp [pow_add])
rw [succ_mersenne, pow_add, show 2 ^ 2 = 4 by norm_num, mul_div_cancel_right₀ _ (by norm_num)] at this
simp [this]
