English
For natural m, the odd step relation holds: complEDS'(b,c,d,k,2(m+1)+1) equals the appropriate combination of prior terms with normEDS.
Русский
Для натурального m выполняется нечетный шаг: complEDS'(b,c,d,k,2(m+1)+1) выражается через предыдущие члены через нормы normEDS.
LaTeX
$$$\operatorname{complEDS}'(b,c,d,k,2\,(m+1) + 1) = \operatorname{complEDS}'(b,c,d,k,m+1)^2 \cdot \operatorname{normEDS}(b,c,d((m+2)\,k + 1)) \cdot \operatorname{normEDS}(b,c,d((m+2)\,k - 1)) - \operatorname{complEDS}'(b,c,d,k,(m+2))^2 \cdot \operatorname{normEDS}(b,c,d((m+1)\,k + 1)) \cdot \operatorname{normEDS}(b,c,d((m+1)\,k - 1))$$$
Lean4
theorem complEDS'_odd (m : ℕ) :
complEDS' b c d k (2 * (m + 1) + 1) =
complEDS' b c d k (m + 1) ^ 2 * normEDS b c d ((m + 2) * k + 1) * normEDS b c d ((m + 2) * k - 1) -
complEDS' b c d k (m + 2) ^ 2 * normEDS b c d ((m + 1) * k + 1) * normEDS b c d ((m + 1) * k - 1) :=
by
rw [show 2 * (m + 1) + 1 = 2 * m + 3 by rfl, complEDS', dif_neg m.not_even_two_mul_add_one]
simpa only [Nat.mul_add_div two_pos] using by rfl
