English
For any W and any natural m, the odd-index recurrence holds: preΨ'(2(m+2)+1) = preΨ'(m+4) · preΨ'(m+2)^3 · (if m even then Ψ₂Sq^2 else 1) − preΨ'(m+1) · preΨ'(m+3)^3 · (if m even then 1 else Ψ₂Sq^2).
Русский
Для любой W и любого натурального m выполняется рекуррентное соотношение для нечётных индексов: preΨ'(2(m+2)+1) = preΨ'(m+4) · preΨ'(m+2)^3 · (если m чётное тогда Ψ₂Sq^2, иначе 1) − preΨ'(m+1) · preΨ'(m+3)^3 · (если m чётное тогда 1, иначе Ψ₂Sq^2).
LaTeX
$$$W.pre\\Psi'(2(m+2)+1) = W.pre\\Psi'(m+4) \cdot W.pre\\Psi'(m+2)^3 \cdot \begin{cases} W.\\Ψ_2S_q^2 & \text{if } \text{Even}(m) \\ 1 & \text{otherwise} \end{cases} - W.pre\\Psi'(m+1) \cdot W.pre\\Psi'(m+3)^3 \cdot \begin{cases} 1 & \text{if } \text{Even}(m) \\ W.\\Ψ_2S_q^2 & \text{otherwise} \end{cases}$$$
Lean4
theorem preΨ'_odd (m : ℕ) :
W.preΨ' (2 * (m + 2) + 1) =
W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
preNormEDS'_odd ..
