English
Let W be a Weierstrass curve. For every integer m, the odd index of the ΨSq-polynomial is the square of a linear combination that involves preΨ, with a factor determined by the parity of m (involving Ψ₂Sq^2 or 1).
Русский
Пусть W — кривая Вейерштрасса. Для каждого целого m нечётная величина ΨSq-полином равна квадрату выражения, содержаего preΨ и зависящего от четности m (с коэффициентом Ψ₂Sq^2 или 1).
LaTeX
$$$W.\\ΨSq(2m+1) = \left( W.preΨ(m+2) \cdot W.preΨ(m)^3 \cdot (\text{if Even } m\text{ then } W.\\Ψ₂Sq^2 \text{ else } 1) \\- W.preΨ(m-1) \cdot W.preΨ(m+1)^3 \cdot (\text{if Even } m\text{ then } 1 \text{ else } W.\\Ψ₂Sq^2) \right)^2$$$
Lean4
theorem ΨSq_odd (m : ℤ) :
W.ΨSq (2 * m + 1) =
(W.preΨ (m + 2) * W.preΨ m ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^
2 :=
by rw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
