English
Let b, c, d be elements of a commutative ring R. For every natural m, the odd-indexed value of the auxiliary sequence satisfies a parity-sensitive recurrence: preNormEDS′(b,c,d,2(m+2)+1) equals preNormEDS′(b,c,d,m+4) · preNormEDS′(b,c,d,m+2)^3 · (if Even m then b else 1) minus preNormEDS′(b,c,d,m+1) · preNormEDS′(b,c,d,m+3)^3 · (if Even m then 1 else b).
Русский
Пусть b, c, d лежат в коммутативном кольце R. Для каждого натурального m нечетное значение дополняющей последовательности удовлетворяет зависимости по парности: preNormEDS′(b,c,d,2(m+2)+1) равно произведению соответствующих степеней и модификаторов в зависимости от чётности m.
LaTeX
$$$$\text{preNormEDS}'(b,c,d,2(m+2)+1) = \text{preNormEDS}'(b,c,d,m+4) \cdot \text{preNormEDS}'(b,c,d,m+2)^3 \cdot (\text{If Even } m \text{ then } b \text{ else } 1) \\ - \text{preNormEDS}'(b,c,d,m+1) \cdot \text{preNormEDS}'(b,c,d,m+3)^3 \cdot (\text{If Even } m \text{ then } 1 \text{ else } b). $$$$
Lean4
theorem preNormEDS'_odd (m : ℕ) :
preNormEDS' b c d (2 * (m + 2) + 1) =
preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * (if Even m then b else 1) -
preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * (if Even m then 1 else b) :=
by rw [show 2 * (m + 2) + 1 = 2 * m + 5 by rfl, preNormEDS', dif_pos <| even_two_mul m, m.mul_div_cancel_left two_pos]
