English
Let b, c, d be elements of a commutative ring R. For every natural m, the even-indexed value of the auxiliary sequence satisfies a specialized product–sum identity: the term at index 2(m+3) equals a combination of earlier terms, specifically (preNormEDS′(b,c,d,m+2))^2 · preNormEDS′(b,c,d,m+3) · preNormEDS′(b,c,d,m+5) minus preNormEDS′(b,c,d,m+1) · preNormEDS′(b,c,d,m+3) · (preNormEDS′(b,c,d,m+4))^2.
Русский
Пусть b, c, d принадлежат коммутативному кольцу R. Для каждого натурального m неравенства чётной степени выполнения последовательности существует тождество, связывающее элементы с чётными индексами: член с индексом 2(m+3) равен разности произведения и суммы, выраженной через ранее заданные значения preNormEDS′(b,c,d,·).
LaTeX
$$$$\text{preNormEDS}'(b,c,d,2(m+3)) = \text{preNormEDS}'(b,c,d,m+2)^2 \cdot \text{preNormEDS}'(b,c,d,m+3) \cdot \text{preNormEDS}'(b,c,d,m+5) \\ - \text{preNormEDS}'(b,c,d,m+1) \cdot \text{preNormEDS}'(b,c,d,m+3) \cdot \text{preNormEDS}'(b,c,d,m+4)^2.$$$$
Lean4
theorem preNormEDS'_even (m : ℕ) :
preNormEDS' b c d (2 * (m + 3)) =
preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2 :=
by
rw [show 2 * (m + 3) = 2 * m + 1 + 5 by rfl, preNormEDS', dif_neg m.not_even_two_mul_add_one]
simpa only [Nat.mul_add_div two_pos] using by rfl
