English
Let W be a Weierstrass curve. The int-version of the odd recurrence holds: preΨ(2m+1) = preΨ(m+2) · preΨ(m)^3 · (if Even m then Ψ₂Sq^2 else 1) − preΨ(m−1) · preΨ(m+1)^3 · (if Even m then 1 else Ψ₂Sq^2).
Русский
Пусть W — кривая Вейерштрасса. Целочисленная версия нечетной рекуррентности: preΨ(2m+1) = preΨ(m+2) · preΨ(m)^3 · (если m четное, то Ψ₂Sq^2, иначе 1) − preΨ(m−1) · preΨ(m+1)^3 · (если m четное, то 1, иначе Ψ₂Sq^2).
LaTeX
$$$W.pre\\Psi(2m+1) = W.pre\\Psi(m+2) \cdot W.pre\\Psi(m)^3 \cdot \begin{cases} W.\\Ψ_2S_q^2 & m \text{ even} \\ 1 & \text{otherwise} \end{cases} - W.pre\\Psi(m-1) \cdot W.pre\\Psi(m+1)^3 \cdot \begin{cases} 1 & m \text{ even} \\ W.\\Ψ_2S_q^2 & \text{otherwise} \end{cases}$$$
Lean4
@[simp]
theorem ΨSq_ofNat (n : ℕ) : W.ΨSq n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1 := by simp [ΨSq]
