English
For integer m, the odd-step relation is given by a formula involving squared prior complEDS' and normEDS terms.
Русский
Для целого m существует формула для нечетного шага, выражающаяся через квадраты предыдущих complEDS' и элементы normEDS.
LaTeX
$$$\operatorname{complEDS}(b,c,d,k,2m+1) = \operatorname{complEDS}(b,c,d,k,m)^2 \cdot \operatorname{normEDS}(b,c,d((m+1)k+1)) \cdot \operatorname{normEDS}(b,c,d((m+1)k-1) ) - \operatorname{complEDS}(b,c,d,k,m+1)^2 \cdot \operatorname{normEDS}(b,c,d(mk+1)) \cdot \operatorname{normEDS}(b,c,d(mk-1))$$
Lean4
theorem complEDS_odd (m : ℤ) :
complEDS b c d k (2 * m + 1) =
complEDS b c d k m ^ 2 * normEDS b c d ((m + 1) * k + 1) * normEDS b c d ((m + 1) * k - 1) -
complEDS b c d k (m + 1) ^ 2 * normEDS b c d (m * k + 1) * normEDS b c d (m * k - 1) :=
by
induction m using Int.negInduction with
| nat m =>
rcases m with _ | _
· simp
norm_cast
simpa only [complEDS_ofNat] using complEDS'_odd ..
| neg ih m =>
rcases m with _ | m
· simp
simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl, show (-(m + 1 : ℤ) + 1) = -m by ring1,
neg_mul, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', complEDS_neg, normEDS_neg, ih]
ring1
