English
The recurrence s(i) has the closed form s(i) = ω^{2^i} + ω_b^{2^i} in X_q.
Русский
Рекуррентность s(i) имеет замкнутую форму s(i) = ω^{2^i} + ω_b^{2^i} в X_q.
LaTeX
$$$ (s(i) : X q) = (\omega : X q)^{2^i} + (\omega_b : X q)^{2^i} $$$
Lean4
/-- If 3 is not a square and 2 is square then $\omega^{(q+1)/2}=-1$. -/
theorem pow_ω [Fact q.Prime] (odd : Odd q) (leg3 : legendreSym q 3 = -1) (leg2 : legendreSym q 2 = 1) :
(ω : X q) ^ ((q + 1) / 2) = -1 :=
by
have pow2 : (2 : ZMod q) ^ ((q + 1) / 2) = 2 := by
obtain ⟨_, _⟩ := odd
rw [(by cutsat : (q + 1) / 2 = q / 2 + 1), pow_succ]
have leg := legendreSym.eq_pow q 2
have : (2 : ZMod q) = ((2 : ℤ) : ZMod q) := by norm_cast
rw [this, ← leg, leg2]
ring
have := two_mul_ω_pow odd leg3
rw [mul_pow] at this
have coe : (2 : X q) = (2 : ZMod q) := by rw [map_ofNat]
rw [coe, ← RingHom.map_pow, pow2, ← coe, (by ring : (-2 : X q) = 2 * -1)] at this
refine (isUnit_of_mul_eq_one (2 : X q) ((q + 1) / 2 : ℕ) ?_).mul_left_cancel this
norm_cast
simp [Nat.mul_div_cancel' odd.add_one.two_dvd]
