English
For any Weierstrass curve W and integer m, the odd-index relation 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 и целого m выполняется нечетная рекуррентная формула: 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
theorem preΨ_odd (m : ℤ) :
W.preΨ (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) :=
preNormEDS_odd ..
