Elliptic divisibility sequences

This file defines the predicates for a sequence to be an elliptic net or an elliptic divisibility sequence, as well as the canonical example of a normalised elliptic divisibility sequence.

Mathematical background

Let R be a commutative ring, and let W be a sequence of elements in R indexed by ℤ. The elliptic relator ER(p, q, r, s) ∈ R associated to W is given for all p, q, r, s ∈ ℤ by ER(p, q, r, s) := W(p+q+s)W(p-q)W(r+s)W(r) - W(p+r+s)W(p-r)W(q+s)W(q) + W(q+r+s)W(q-r)W(p+s)W(p). Call W an elliptic net if it satisfies the elliptic relation ER(p, q, r, s) = 0 for all p, q, r, s ∈ ℤ. By a change of variables, ER is related to the symmetric relation ERₐ (see IsEllipticNet.rel_eq and IsEllipticNet.atomRel_eq), where ERₐ(a, b, c, d) ∈ R is given for all a, b, c, d ∈ ℤ by ERₐ(a, b, c, d) := Wₐ(a, b)Wₐ(c, d) - Wₐ(a, c)Wₐ(b, d) + Wₐ(a, d)Wₐ(b, c) defined in terms of elliptic atoms Wₐ(a, b) := W((a + b) / 2)W((a - b) / 2).

As a special case, W is an elliptic sequence if it satisfies ER(p, q, r, 0) = 0 for all p, q, r ∈ ℤ. It is a divisibility sequence if it satisfies W(k) ∣ W(n * k) for all k, n ∈ ℤ, and an elliptic divisibility sequence (EDS) if it is a divisibility sequence that is elliptic. If W is an EDS, then x • W is also an EDS for any x ∈ R. It turns out that any EDS W can be normalised such that W(1) = 1, in which case it can be characterised completely by

• the even relations ER(m + 1, m - 1, 1, 0) = 0 for all m ∈ ℤ, or in other words that W(2m)W(2) = W(m - 1)²W(m)W(m + 2) - W(m - 2)W(m)W(m + 1)² for all m ∈ ℤ, and
• the odd relations ER(m + 1, m, 1, 0) = 0 for all m ∈ ℤ, or in other words that W(2m + 1) = W(m + 2)W(m)³ - W(m - 1)W(m + 1)³ for all m ∈ ℤ,

with initial values W(0) = 0, W(1) = 1, W(2) = b, W(3) = c, and W(4) = d * b for some b, c, d ∈ R. This will be called the canonical example of a normalised EDS in this file.

Some examples of EDSs include

• the identity sequence,
• certain terms of Lucas sequences, and
• division polynomials of elliptic curves.

Main definitions

• IsEllipticNet.atom: the elliptic atom Wₐ(a, b) indexed by ℤ.
• IsEllipticNet.atomRel: the elliptic relator ERₐ(a, b, c, d) indexed by ℤ.
• IsEllipticNet.rel: the elliptic relator ER(p, q, r, s) indexed by ℤ.
• IsEllipticNet: a sequence indexed by ℤ is an elliptic net.
• IsEllipticSequence: a sequence indexed by ℤ is an elliptic sequence.
• IsEllipticDvdSequence: a sequence indexed by ℤ is an EDS.
• preNormEDS': the auxiliary sequence for a normalised EDS indexed by ℕ.
• preNormEDS: the auxiliary sequence for a normalised EDS indexed by ℤ.
• complEDS₂: the 2-complement sequence for a normalised EDS indexed by ℕ.
• normEDS: the canonical example of a normalised EDS indexed by ℤ.
• complEDS': the complement sequence for a normalised EDS indexed by ℕ.
• complEDS: the complement sequence for a normalised EDS indexed by ℤ.

Main statements

• TODO: prove that normEDS satisfies IsEllipticDvdSequence.
• TODO: prove that a sequence satisfying IsEllipticDvdSequence can be normalised to a normEDS.

Implementation notes

The elliptic relator is identical to the elliptic net recurrence defined by Stange, except that the final term in the latter is negated. This unifies the definitions of Stange's elliptic nets and Ward's elliptic sequences without requiring the sequence to be an odd function.

The normalised EDS normEDS b c d n is defined in terms of the auxiliary sequence preNormEDS (b ^ 4) c d n, which are equal when n is odd, and which differ by a factor of b when n is even. This coincides with the definition in the references since both agree for normEDS b c d 2 and for normEDS b c d 4, and the correct factors of b are removed in normEDS b c d (2 * (m + 2) + 1) and in normEDS b c d (2 * (m + 3)).

One reason is to avoid the necessity for ring division by b in the inductive definition of normEDS b c d (2 * (m + 3)). The idea is that it can be shown that normEDS b c d (2 * (m + 3)) always contains a factor of b, so it is possible to remove a factor of b a posteriori, but stating this lemma requires first defining normEDS b c d (2 * (m + 3)), which requires having this factor of b a priori. Another reason is to allow the definition of univariate n-division polynomials of elliptic curves, omitting a factor of the bivariate 2-division polynomial.

References

• K Stange, Elliptic Nets and Elliptic Curves
• M Ward, Memoir on Elliptic Divisibility Sequences

Tags

elliptic net, elliptic divisibility sequence

def IsEllipticNet.atom {R : Type u_1} [CommRing R] (W : ℤ → R) (a b : ℤ) : R

The elliptic atom Wₐ(a, b) that defines an elliptic net. Note that this is defined in terms of truncated integer division, and hence should only be used when a and b have the same parity.

Equations

• IsEllipticNet.atom W a b = W ((a + b).tdiv 2) * W ((a - b).tdiv 2)

@[simp]

theorem IsEllipticNet.atom_same {R : Type u_1} [CommRing R] (W : ℤ → R) (a : ℤ) : atom W a a = W a * W 0

@[simp]

theorem IsEllipticNet.neg_atom {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b : ℤ) : -atom W a b = atom W b a

theorem IsEllipticNet.atom_mul_atom {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atom W a b * atom W c d = atom W b a * atom W d c

@[simp]

theorem IsEllipticNet.atom_neg_left {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b : ℤ) : atom W (-a) b = atom W a b

@[simp]

theorem IsEllipticNet.atom_neg_right {R : Type u_1} [CommRing R] (W : ℤ → R) (a b : ℤ) : atom W a (-b) = atom W a b

@[simp]

theorem IsEllipticNet.atom_abs_left {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b : ℤ) : atom W |a| b = atom W a b

@[simp]

theorem IsEllipticNet.atom_abs_right {R : Type u_1} [CommRing R] (W : ℤ → R) (a b : ℤ) : atom W a |b| = atom W a b

theorem IsEllipticNet.atom_even {R : Type u_1} [CommRing R] (W : ℤ → R) (a b : ℤ) : atom W (2 * a) (2 * b) = W (a + b) * W (a - b)

theorem IsEllipticNet.atom_odd {R : Type u_1} [CommRing R] (W : ℤ → R) (a b : ℤ) : atom W (2 * a + 1) (2 * b + 1) = W (a + b + 1) * W (a - b)

theorem IsEllipticNet.map_atom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : ℤ → R) {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (a b : ℤ) : f (atom W a b) = atom (⇑f ∘ W) a b

def IsEllipticNet.atomRel {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : R

The elliptic relator ERₐ(a, b, c, d) obtained by a change of variables in ER(p, q, r, s) (see IsEllipticNet.rel_eq and IsEllipticNet.atomRel_eq). Note that this is defined in terms of elliptic atoms, and hence should only be used when a, b, c, and d have the same parity.

Equations

• IsEllipticNet.atomRel W a b c d = IsEllipticNet.atom W a b * IsEllipticNet.atom W c d - IsEllipticNet.atom W a c * IsEllipticNet.atom W b d + IsEllipticNet.atom W a d * IsEllipticNet.atom W b c

@[simp]

theorem IsEllipticNet.atomRel_same₁₂ {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c : ℤ) : atomRel W a a b c = W a * W 0 * atom W b c

@[simp]

theorem IsEllipticNet.atomRel_same₁₃ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c : ℤ) : atomRel W a b a c = W a * W 0 * atom W c b

@[simp]

theorem IsEllipticNet.atomRel_same₁₄ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c : ℤ) : atomRel W a b c a = W a * W 0 * atom W b c

@[simp]

theorem IsEllipticNet.atomRel_same₂₃ {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c : ℤ) : atomRel W a b b c = W b * W 0 * atom W a c

@[simp]

theorem IsEllipticNet.atomRel_same₂₄ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c : ℤ) : atomRel W a b c b = W b * W 0 * atom W c a

@[simp]

theorem IsEllipticNet.atomRel_same₃₄ {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c : ℤ) : atomRel W a b c c = W c * W 0 * atom W a b

@[simp]

theorem IsEllipticNet.atomRel_neg₁ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atomRel W (-a) b c d = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_neg₂ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atomRel W a (-b) c d = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_neg₃ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atomRel W a b (-c) d = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_neg₄ {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : atomRel W a b c (-d) = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_abs₁ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atomRel W |a| b c d = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_abs₂ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atomRel W a |b| c d = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_abs₃ {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (a b c d : ℤ) : atomRel W a b |c| d = atomRel W a b c d

@[simp]

theorem IsEllipticNet.atomRel_abs₄ {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : atomRel W a b c |d| = atomRel W a b c d

theorem IsEllipticNet.atomRel_avg_sub {R : Type u_1} [CommRing R] (W : ℤ → R) {a b c d : ℤ} (parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2) : atomRel W ((a + b + c + d) / 2 - d) ((a + b + c + d) / 2 - c) ((a + b + c + d) / 2 - b) ((a + b + c + d) / 2 - a) = atomRel W a b c d

theorem IsEllipticNet.map_atomRel {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : ℤ → R) {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (a b c d : ℤ) : f (atomRel W a b c d) = atomRel (⇑f ∘ W) a b c d

def IsEllipticNet.rel {R : Type u_1} [CommRing R] (W : ℤ → R) (p q r s : ℤ) : R

The elliptic relator ER(p, q, r, s) that defines an elliptic net.

Equations

• IsEllipticNet.rel W p q r s = W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q + W (q + r + s) * W (q - r) * W (p + s) * W p

theorem IsEllipticNet.rel_eq {R : Type u_1} [CommRing R] (W : ℤ → R) (p q r s : ℤ) : rel W p q r s = atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s

theorem IsEllipticNet.atomRel_two_mul {R : Type u_1} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : atomRel W (2 * a) (2 * b) (2 * c) (2 * d) = rel W (a - d) (b - d) (c - d) (2 * d)

theorem IsEllipticNet.atomRel_eq {R : Type u_1} [CommRing R] (W : ℤ → R) {a b c d : ℤ} (parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2) : atomRel W a b c d = rel W ((a - d) / 2) ((b - d) / 2) ((c - d) / 2) d

@[simp]

theorem IsEllipticNet.rel_neg {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (p q r s : ℤ) : rel W (-p) (-q) (-r) (-s) = rel W p q r s

theorem IsEllipticNet.rel_even {R : Type u_1} [CommRing R] (W : ℤ → R) (m : ℤ) : rel W (m + 1) (m - 1) 1 0 = W (2 * m) * W 2 * W 1 ^ 2 - W (m - 1) ^ 2 * W m * W (m + 2) + W (m - 2) * W m * W (m + 1) ^ 2

The even elliptic relator ER(m + 1, m - 1, 1, 0) for m ∈ ℤ.

theorem IsEllipticNet.rel_odd {R : Type u_1} [CommRing R] (W : ℤ → R) (m : ℤ) : rel W (m + 1) m 1 0 = W (2 * m + 1) * W 1 ^ 3 - W (m + 2) * W m ^ 3 + W (m - 1) * W (m + 1) ^ 3

The odd elliptic relator ER(m + 1, m, 1, 0) for m ∈ ℤ.

theorem IsEllipticNet.map_rel {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : ℤ → R) {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (p q r s : ℤ) : f (rel W p q r s) = rel (⇑f ∘ W) p q r s

def IsEllipticNet {R : Type u_1} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by ℤ is an elliptic net.

Equations

• IsEllipticNet W = ∀ (p q r s : ℤ), IsEllipticNet.rel W p q r s = 0

def IsEllipticSequence {R : Type u_1} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by ℤ is an elliptic sequence.

Equations

• IsEllipticSequence W = ∀ (p q r : ℤ), IsEllipticNet.rel W p q r 0 = 0

@[deprecated IsEllipticSequence (since := "2026-07-01")]

def IsEllSequence {R : Type u_1} [CommRing R] (W : ℤ → R) : Prop

Alias of IsEllipticSequence.

---

The proposition that a sequence indexed by ℤ is an elliptic sequence.

Equations

• @IsEllSequence = @IsEllipticSequence

def IsEllipticDvdSequence {R : Type u_1} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by ℤ is an EDS.

Equations

• IsEllipticDvdSequence W = (IsEllipticSequence W ∧ IsDvdSequence W)

@[deprecated IsEllipticDvdSequence (since := "2026-06-30")]

def IsEllDivSequence {R : Type u_1} [CommRing R] (W : ℤ → R) : Prop

Alias of IsEllipticDvdSequence.

---

The proposition that a sequence indexed by ℤ is an EDS.

Equations

• @IsEllDivSequence = @IsEllipticDvdSequence

theorem IsEllipticNet.isEllipticSequence {R : Type u_1} [CommRing R] {W : ℤ → R} (h : IsEllipticNet W) : IsEllipticSequence W

theorem IsEllipticNet.id : IsEllipticNet id

theorem IsEllipticNet.smul {R : Type u_1} [CommRing R] {W : ℤ → R} (h : IsEllipticNet W) (x : R) : IsEllipticNet (x • W)

theorem IsEllipticSequence.id : IsEllipticSequence id

theorem IsEllipticSequence.smul {R : Type u_1} [CommRing R] {W : ℤ → R} (h : IsEllipticSequence W) (x : R) : IsEllipticSequence (x • W)

@[deprecated IsEllipticSequence.id (since := "2026-07-01")]

theorem isEllSequence_id : IsEllipticSequence id

Alias of IsEllipticSequence.id.

@[deprecated IsEllipticSequence.smul (since := "2026-07-01")]

theorem IsEllSequence.smul {R : Type u_1} [CommRing R] {W : ℤ → R} (h : IsEllipticSequence W) (x : R) : IsEllipticSequence (x • W)

Alias of IsEllipticSequence.smul.

theorem IsEllipticDvdSequence.id : IsEllipticDvdSequence id

The identity sequence is an EDS.

theorem IsEllipticDvdSequence.smul {R : Type u_1} [CommRing R] {W : ℤ → R} (h : IsEllipticDvdSequence W) (x : R) : IsEllipticDvdSequence (x • W)

@[deprecated IsEllipticDvdSequence.id (since := "2026-06-30")]

theorem isEllDivSequence_id : IsEllipticDvdSequence id

Alias of IsEllipticDvdSequence.id.

---

The identity sequence is an EDS.

@[deprecated IsEllipticDvdSequence.smul (since := "2026-06-30")]

theorem IsEllDivSequence.smul {R : Type u_1} [CommRing R] {W : ℤ → R} (h : IsEllipticDvdSequence W) (x : R) : IsEllipticDvdSequence (x • W)

Alias of IsEllipticDvdSequence.smul.

@[irreducible]

def preNormEDS' {R : Type u_1} [CommRing R] (b c d : R) : ℕ → R

The auxiliary sequence for a normalised EDS W : ℕ → R, with initial values W(0) = 0, W(1) = 1, W(2) = 1, W(3) = c, and W(4) = d and extra parameter b.

Equations

• One or more equations did not get rendered due to their size.
• preNormEDS' b c d 0 = 0
• preNormEDS' b c d 1 = 1
• preNormEDS' b c d 2 = 1
• preNormEDS' b c d 3 = c
• preNormEDS' b c d 4 = d

@[simp]

theorem preNormEDS'_zero {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS' b c d 0 = 0

@[simp]

theorem preNormEDS'_one {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS' b c d 1 = 1

@[simp]

theorem preNormEDS'_two {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS' b c d 2 = 1

@[simp]

theorem preNormEDS'_three {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS' b c d 3 = c

@[simp]

theorem preNormEDS'_four {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS' b c d 4 = d

theorem preNormEDS'_even {R : Type u_1} [CommRing R] (b c d : R) (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

theorem preNormEDS'_odd {R : Type u_1} [CommRing R] (b c d : R) (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

def preNormEDS {R : Type u_1} [CommRing R] (b c d : R) (n : ℤ) : R

The auxiliary sequence for a normalised EDS W : ℤ → R, with initial values W(0) = 0, W(1) = 1, W(2) = 1, W(3) = c, and W(4) = d and extra parameter b.

This extends preNormEDS' by defining its values at negative integers.

Equations

• preNormEDS b c d n = ↑n.sign * preNormEDS' b c d n.natAbs

@[simp]

theorem preNormEDS_ofNat {R : Type u_1} [CommRing R] (b c d : R) (n : ℕ) : preNormEDS b c d ↑n = preNormEDS' b c d n

@[simp]

theorem preNormEDS_zero {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS b c d 0 = 0

@[simp]

theorem preNormEDS_one {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS b c d 1 = 1

@[simp]

theorem preNormEDS_two {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS b c d 2 = 1

@[simp]

theorem preNormEDS_three {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS b c d 3 = c

@[simp]

theorem preNormEDS_four {R : Type u_1} [CommRing R] (b c d : R) : preNormEDS b c d 4 = d

@[simp]

theorem preNormEDS_neg {R : Type u_1} [CommRing R] (b c d : R) (n : ℤ) : preNormEDS b c d (-n) = -preNormEDS b c d n

theorem preNormEDS_even {R : Type u_1} [CommRing R] (b c d : R) (m : ℤ) : preNormEDS b c d (2 * m) = preNormEDS b c d (m - 1) ^ 2 * preNormEDS b c d m * preNormEDS b c d (m + 2) - preNormEDS b c d (m - 2) * preNormEDS b c d m * preNormEDS b c d (m + 1) ^ 2

theorem preNormEDS_odd {R : Type u_1} [CommRing R] (b c d : R) (m : ℤ) : preNormEDS b c d (2 * m + 1) = (preNormEDS b c d (m + 2) * preNormEDS b c d m ^ 3 * if Even m then b else 1) - preNormEDS b c d (m - 1) * preNormEDS b c d (m + 1) ^ 3 * if Even m then 1 else b

def complEDS₂ {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : R

The 2-complement sequence Wᶜ₂ : ℤ → R for a normalised EDS W : ℤ → R that witnesses W(k) ∣ W(2 * k). In other words, W(k) * Wᶜ₂(k) = W(2 * k) for all k ∈ ℤ.

This is defined in terms of preNormEDS.

Equations

• complEDS₂ b c d k = (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) - preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) * if Even k then 1 else b

@[simp]

theorem complEDS₂_zero {R : Type u_1} [CommRing R] (b c d : R) : complEDS₂ b c d 0 = 2

@[simp]

theorem complEDS₂_one {R : Type u_1} [CommRing R] (b c d : R) : complEDS₂ b c d 1 = b

@[simp]

theorem complEDS₂_two {R : Type u_1} [CommRing R] (b c d : R) : complEDS₂ b c d 2 = d

@[simp]

theorem complEDS₂_three {R : Type u_1} [CommRing R] (b c d : R) : complEDS₂ b c d 3 = preNormEDS (b ^ 4) c d 5 * b - d ^ 2 * b

@[simp]

theorem complEDS₂_four {R : Type u_1} [CommRing R] (b c d : R) : complEDS₂ b c d 4 = c ^ 2 * preNormEDS (b ^ 4) c d 6 - preNormEDS (b ^ 4) c d 5 ^ 2

@[simp]

theorem complEDS₂_neg {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : complEDS₂ b c d (-k) = complEDS₂ b c d k

theorem preNormEDS_mul_complEDS₂ {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : preNormEDS (b ^ 4) c d k * complEDS₂ b c d k = preNormEDS (b ^ 4) c d (2 * k) * if Even k then 1 else b

def normEDS {R : Type u_1} [CommRing R] (b c d : R) (n : ℤ) : R

The canonical example of a normalised EDS W : ℤ → R, with initial values W(0) = 0, W(1) = 1, W(2) = b, W(3) = c, and W(4) = d * b.

This is defined in terms of preNormEDS whose even terms differ by a factor of b.

Equations

• normEDS b c d n = preNormEDS (b ^ 4) c d n * if Even n then b else 1

@[simp]

theorem normEDS_ofNat {R : Type u_1} [CommRing R] (b c d : R) (n : ℕ) : normEDS b c d ↑n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1

@[simp]

theorem normEDS_zero {R : Type u_1} [CommRing R] (b c d : R) : normEDS b c d 0 = 0

@[simp]

theorem normEDS_one {R : Type u_1} [CommRing R] (b c d : R) : normEDS b c d 1 = 1

@[simp]

theorem normEDS_two {R : Type u_1} [CommRing R] (b c d : R) : normEDS b c d 2 = b

@[simp]

theorem normEDS_three {R : Type u_1} [CommRing R] (b c d : R) : normEDS b c d 3 = c

@[simp]

theorem normEDS_four {R : Type u_1} [CommRing R] (b c d : R) : normEDS b c d 4 = d * b

@[simp]

theorem normEDS_neg {R : Type u_1} [CommRing R] (b c d : R) (n : ℤ) : normEDS b c d (-n) = -normEDS b c d n

theorem normEDS_mul_complEDS₂ {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)

theorem normEDS_dvd_normEDS_two_mul {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : normEDS b c d k ∣ normEDS b c d (2 * k)

theorem complEDS₂_mul_b {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : complEDS₂ b c d k * b = normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) - normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2

theorem normEDS_even {R : Type u_1} [CommRing R] (b c d : R) (m : ℤ) : normEDS b c d (2 * m) * b = normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) - normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2

theorem normEDS_odd {R : Type u_1} [CommRing R] (b c d : R) (m : ℤ) : normEDS b c d (2 * m + 1) = normEDS b c d (m + 2) * normEDS b c d m ^ 3 - normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3

noncomputable def normEDSRec' {P : ℕ → Sort u_4} (zero : P 0) (one : P 1) (two : P 2) (three : P 3) (four : P 4) (even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))) (odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)) (n : ℕ) : P n

Strong recursion principle for a normalised EDS: if we have

• P 0, P 1, P 2, P 3, and P 4,
• for all m : ℕ we can prove P (2 * (m + 3)) from P k for all k < 2 * (m + 3), and
• for all m : ℕ we can prove P (2 * (m + 2) + 1) from P k for all k < 2 * (m + 2) + 1,

then we have P n for all n : ℕ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def normEDSRec {P : ℕ → Sort u_4} (zero : P 0) (one : P 1) (two : P 2) (three : P 3) (four : P 4) (even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))) (odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)) (n : ℕ) : P n

Recursion principle for a normalised EDS: if we have

• P 0, P 1, P 2, P 3, and P 4,
• for all m : ℕ we can prove P (2 * (m + 3)) from P (m + 1), P (m + 2), P (m + 3), P (m + 4), and P (m + 5), and
• for all m : ℕ we can prove P (2 * (m + 2) + 1) from P (m + 1), P (m + 2), P (m + 3), and P (m + 4),

then we have P n for all n : ℕ.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def complEDS' {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : ℕ → R

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 all k, n ∈ ℤ.

This is defined in terms of normEDS and agrees with complEDS₂ when n = 2.

Equations

• One or more equations did not get rendered due to their size.
• complEDS' b c d k 0 = 0
• complEDS' b c d k 1 = 1

@[simp]

theorem complEDS'_zero {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : complEDS' b c d k 0 = 0

@[simp]

theorem complEDS'_one {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : complEDS' b c d k 1 = 1

theorem complEDS'_even {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) (m : ℕ) : complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑m + 1) * k)

theorem complEDS'_odd {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) (m : ℕ) : complEDS' b c d k (2 * (m + 1) + 1) = complEDS' b c d k (m + 1) ^ 2 * normEDS b c d ((↑m + 2) * k + 1) * normEDS b c d ((↑m + 2) * k - 1) - complEDS' b c d k (m + 2) ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1)

def complEDS {R : Type u_1} [CommRing R] (b c d : R) (k n : ℤ) : R

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 all k, n ∈ ℤ.

This extends complEDS' by defining its values at negative integers.

Equations

• complEDS b c d k n = ↑n.sign * complEDS' b c d k n.natAbs

@[simp]

theorem complEDS_ofNat {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) (n : ℕ) : complEDS b c d k ↑n = complEDS' b c d k n

@[simp]

theorem complEDS_zero {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : complEDS b c d k 0 = 0

@[simp]

theorem complEDS_one {R : Type u_1} [CommRing R] (b c d : R) (k : ℤ) : complEDS b c d k 1 = 1

@[simp]

theorem complEDS_neg {R : Type u_1} [CommRing R] (b c d : R) (k n : ℤ) : complEDS b c d k (-n) = -complEDS b c d k n

theorem complEDS_even {R : Type u_1} [CommRing R] (b c d : R) (k m : ℤ) : complEDS b c d k (2 * m) = complEDS b c d k m * complEDS₂ b c d (m * k)

theorem complEDS_odd {R : Type u_1} [CommRing R] (b c d : R) (k 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)

noncomputable def complEDSRec' {P : ℕ → Sort u_4} (zero : P 0) (one : P 1) (even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))) (odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)) (n : ℕ) : P n

Strong recursion principle for the complement sequence for a normalised EDS: if we have

• P 0, P 1,
• for all m : ℕ we can prove P (2 * (m + 3)) from P k for all k < 2 * (m + 3), and
• for all m : ℕ we can prove P (2 * (m + 2) + 1) from P k for all k < 2 * (m + 2) + 1,

then we have P n for all n : ℕ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def complEDSRec {P : ℕ → Sort u_4} (zero : P 0) (one : P 1) (even : (m : ℕ) → P (m + 1) → P (2 * (m + 1))) (odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)) (n : ℕ) : P n

Recursion principle for the complement sequence for a normalised EDS: if we have

• P 0, P 1,
• for all m : ℕ we can prove P (2 * (m + 3)) from P (m + 1), P (m + 2), P (m + 3), P (m + 4), and P (m + 5), and
• for all m : ℕ we can prove P (2 * (m + 2) + 1) from P (m + 1), P (m + 2), P (m + 3), and P (m + 4),

then we have P n for all n : ℕ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem map_preNormEDS' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (n : ℕ) : f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n

@[simp]

theorem map_preNormEDS {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (n : ℤ) : f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n

@[simp]

theorem map_complEDS₂ {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (n : ℤ) : f (complEDS₂ b c d n) = complEDS₂ (f b) (f c) (f d) n

@[simp]

theorem map_normEDS {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (n : ℤ) : f (normEDS b c d n) = normEDS (f b) (f c) (f d) n

@[simp]

theorem map_complEDS' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (k : ℤ) (n : ℕ) : f (complEDS' b c d k n) = complEDS' (f b) (f c) (f d) k n

@[simp]

theorem map_complEDS {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (k n : ℤ) : f (complEDS b c d k n) = complEDS (f b) (f c) (f d) k n