English
For integer m, the odd step relation holds: complEDS'(b,c,d,k,2m+3) equals a specific expression built from prior terms and normEDS with k.
Русский
Для целого m выполняется нечетный шаг в целочисленной индексации: complEDS'(b,c,d,k,2m+3) выражается через предыдущие члены и normEDS.
LaTeX
$$$\operatorname{complEDS}'(b,c,d,k,2m+3) = \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
/-- The complement sequence `Wᶜ : ℤ × ℤ → R` for a normalised EDS `W : ℤ → R` that witnesses
`W(k) ∣ W(n * k)`. In other words, `W(k) * Wᶜ(k, n) = W(n * k)` for any `k, n ∈ ℤ`.
This extends `complEDS'` by defining its values at negative integers. -/
def complEDS (n : ℤ) : R :=
n.sign * complEDS' b c d k n.natAbs
