English
If the Lucas–Lehmer residue at p' + 2 vanishes, then there exists an integer k such that (ω : X (q (p' + 2)))^{2^{p' + 1}} = k · mersenne (p' + 2) · (ω : X (q (p' + 2)))^{2^{p'}} − 1.
Русский
Если нуль остатка Лукаса–Леммера при p' + 2, то существует целое k такое, что (ω : X (q (p' + 2)))^{2^{p' + 1}} = k · mersenne (p' + 2) · (ω : X (q (p' + 2)))^{2^{p'}} − 1.
LaTeX
$$$\operatorname{lucasLehmerResidue}(p'+2) = 0 \Rightarrow \exists k \in \mathbb{Z}, (\omega : X (q (p'+2)))^{2^{p'+1}} = k \cdot \mathrm{mersenne}(p'+2) \cdot (\omega : X (q (p'+2)))^{2^{p'}} - 1.$$$
Lean4
theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
∃ k : ℤ, (ω : X (q (p' + 2))) ^ 2 ^ (p' + 1) = k * mersenne (p' + 2) * (ω : X (q (p' + 2))) ^ 2 ^ p' - 1 :=
by
dsimp [lucasLehmerResidue] at h
rw [sZMod_eq_s p'] at h
replace h : 2 ^ (p' + 2) - 1 ∣ s p' := by simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h
obtain ⟨k, h⟩ := h
use k
replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h
dsimp at h
rw [closed_form] at h
replace h := congr_arg (fun x => ω ^ 2 ^ p' * x) h
dsimp at h
have t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1) := by ring
rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h
rw [mul_comm, coe_mul] at h
rw [mul_comm _ (k : X (q (p' + 2)))] at h
replace h := eq_sub_of_add_eq h
have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide)
exact mod_cast h
