Elliptic divisibility sequences

This file defines the type of an elliptic divisibility sequence (EDS) and a few examples.

Mathematical background

Let R be a commutative ring. An elliptic sequence is a sequence W : ℤ → R satisfying W(m + n)W(m - n)W(r)² = W(m + r)W(m - r)W(n)² - W(n + r)W(n - r)W(m)² for any m, n, r ∈ ℤ. A divisibility sequence is a sequence W : ℤ → R satisfying W(m) ∣ W(n) for any m, n ∈ ℤ such that m ∣ n. An elliptic divisibility sequence is simply a divisibility sequence that is elliptic.

Some examples of EDSs include

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

Main definitions

• IsEllSequence: a sequence indexed by integers is an elliptic sequence.
• IsDivSequence: a sequence indexed by integers is a divisibility sequence.
• IsEllDivSequence: a sequence indexed by integers 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 IsEllDivSequence.
• TODO: prove that a normalised sequence satisfying IsEllDivSequence can be given by normEDS.

Implementation notes

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

M Ward, Memoir on Elliptic Divisibility Sequences

Tags

elliptic, divisibility, sequence

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

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

def IsDivSequence {R : Type u} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by integers is a divisibility sequence.

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

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

theorem isEllSequence_id : IsEllSequence id

theorem isDivSequence_id : IsDivSequence id

theorem isEllDivSequence_id : IsEllDivSequence id

The identity sequence is an EDS.

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

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

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

@[irreducible]

def preNormEDS' {R : Type u} [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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem preNormEDS'_even {R : Type u} [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} [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} [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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem preNormEDS_even {R : Type u} [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

@[deprecated preNormEDS_even (since := "2025-05-15")]

theorem preNormEDS_even_ofNat {R : Type u} [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

Alias of preNormEDS_even.

theorem preNormEDS_odd {R : Type u} [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

@[deprecated preNormEDS_odd (since := "2025-05-15")]

theorem preNormEDS_odd_ofNat {R : Type u} [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

Alias of preNormEDS_odd.

def complEDS₂ {R : Type u} [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 any k ∈ ℤ.

This is defined in terms of preNormEDS.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem complEDS₂_three {R : Type u} [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} [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} [CommRing R] (b c d : R) (k : ℤ) : complEDS₂ b c d (-k) = complEDS₂ b c d k

theorem preNormEDS_mul_complEDS₂ {R : Type u} [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} [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.

@[simp]

theorem normEDS_ofNat {R : Type u} [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} [CommRing R] (b c d : R) : normEDS b c d 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem normEDS_mul_complEDS₂ {R : Type u} [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} [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} [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} [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

@[deprecated normEDS_even (since := "2025-05-15")]

theorem normEDS_even_ofNat {R : Type u} [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

Alias of normEDS_even.

theorem normEDS_odd {R : Type u} [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

@[deprecated normEDS_odd (since := "2025-05-15")]

theorem normEDS_odd_ofNat {R : Type u} [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

Alias of normEDS_odd.

noncomputable def normEDSRec' {P : ℕ → Sort u} (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 : ℕ.

noncomputable def normEDSRec {P : ℕ → Sort u} (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 : ℕ.

@[irreducible]

def complEDS' {R : Type u} [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 any k, n ∈ ℤ.

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

@[simp]

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

@[simp]

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

theorem complEDS'_even {R : Type u} [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} [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} [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 any k, n ∈ ℤ.

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

@[simp]

theorem complEDS_ofNat {R : Type u} [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} [CommRing R] (b c d : R) (k : ℤ) : complEDS b c d k 0 = 0

@[simp]

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

@[simp]

theorem complEDS_neg {R : Type u} [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} [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} [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} (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 : ℕ.

noncomputable def complEDSRec {P : ℕ → Sort u} (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 : ℕ.

@[simp]

theorem map_preNormEDS' {R : Type u} [CommRing R] (b c d : R) {S : Type v} [CommRing S] (f : R →+* S) (n : ℕ) : f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n

@[simp]

theorem map_preNormEDS {R : Type u} [CommRing R] (b c d : R) {S : Type v} [CommRing S] (f : R →+* S) (n : ℤ) : f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n

@[simp]

theorem map_complEDS₂ {R : Type u} [CommRing R] (b c d : R) {S : Type v} [CommRing S] (f : R →+* S) (n : ℤ) : f (complEDS₂ b c d n) = complEDS₂ (f b) (f c) (f d) n

@[simp]

theorem map_normEDS {R : Type u} [CommRing R] (b c d : R) {S : Type v} [CommRing S] (f : R →+* S) (n : ℤ) : f (normEDS b c d n) = normEDS (f b) (f c) (f d) n

@[simp]

theorem map_complEDS' {R : Type u} [CommRing R] (b c d : R) {S : Type v} [CommRing S] (f : R →+* S) (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} [CommRing R] (b c d : R) {S : Type v} [CommRing S] (f : R →+* S) (k n : ℤ) : f (complEDS b c d k n) = complEDS (f b) (f c) (f d) k n