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 : \mathbb{Z} \to R$ satisfying $$ W(m + n)W(m - n)W(r)^2 = W(m + r)W(m - r)W(n)^2 - W(n + r)W(n - r)W(m)^2, $$ for any $m, n, r \in \mathbb{Z}$. A divisibility sequence is a sequence $W : \mathbb{Z} \to R$ satisfying $W(m) \mid W(n)$ for any $m, n \in \mathbb{Z}$ such that $m \mid n$.

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 ℤ.
• normEDS: the canonical example of 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.

Equations

• IsEllSequence W = ∀ (m n r : ℤ), W (m + n) * W (m - n) * W r ^ 2 = W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2

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

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

Equations

• IsDivSequence W = ∀ (m n : ℕ), m ∣ n → W ↑m ∣ W ↑n

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

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

Equations

• IsEllDivSequence W = (IsEllSequence W ∧ IsDivSequence W)

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.

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} [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'_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

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

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.

Equations

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

@[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

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

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

@[simp]

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

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.

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} [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

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

theorem normEDS_even {R : Type u} [CommRing R] (b c d : R) (m : ℕ) : normEDS b c d (2 * (↑m + 3)) * b = normEDS b c d (↑m + 2) ^ 2 * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 5) - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 4) ^ 2

@[simp]

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

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 : ℕ.

Equations

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

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 : ℕ.

Equations

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

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

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

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