English
An alternate proof of the even-step recurrence for complEDS: using negation symmetry and previous lemmas, the relation complEDS(b,c,d,k,2m) = ... holds for all m.
Русский
Альтернативное доказательство чётного шага для complEDS: используя симметрию относительно отрицания и предыдущие леммы, выполняется тождество complEDS(b,c,d,k,2m) = ... для всех m.
LaTeX
$$$\operatorname{complEDS}(b,c,d,k,2m) = \operatorname{complEDS}(b,c,d,k,m) \cdot \operatorname{complEDS}_2(b,c,d)(m k)$$$
Lean4
theorem complEDS_even (m : ℤ) : complEDS b c d k (2 * m) = complEDS b c d k m * complEDS₂ b c d (m * k) := by
induction m using Int.negInduction with
| nat m =>
rcases m with _ | _
· simp
norm_cast
simpa only [complEDS_ofNat] using complEDS'_even ..
| neg ih => simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]
