Papers With

← All papers
First page of On Elliptic Sequences over Commutative Rings

On Elliptic Sequences over Commutative Rings

Junyan Xu

math.NT Apr 7, 2026 · v1 math.AC
formalization mathlib number-theory algebra
Read PDF arXiv abstract
TL;DR
Most results are formalized in Lean's Mathlib in EllipticDivisibilitySequence.lean via a Mathlib pull request, using normEDS and preNormEDS definitions.
Abstract
We define elliptic sequences over a commutative ring as sequences indexed by the (positive) integers satisfying a 4-parameter, highly symmetric family of homogeneous quartic relations among terms which we call elliptic relations. We classify elliptic sequences over a field into three types, and show that most of them are dilated multiples of standard elliptic divisibility sequences (EDSs) which form countably many 4-dimensional families. In particular, we show standard EDSs are elliptic in a purely algebraic way using intricate implications among elliptic relations, without relying on complex analytic theory of Weierstrass functions. We shall use results presented here to give a purely algebraic treatment of division polynomials in a follow-up paper.
Problem

Elliptic sequences and elliptic divisibility sequences are usually studied over the integers, often using complex-analytic tools such as Weierstrass functions. A purely algebraic theory over arbitrary commutative rings was sought, motivated by formalizing division polynomials in Lean.

Approach

Elliptic sequences are defined by a symmetric 4-parameter family of quartic elliptic relations, and implication rules among these relations are developed. Identity principles show when sequences are determined by their initial terms. Standard EDSs are built from an auxiliary sequence via the even-odd recurrence, and a translation invariant is derived. Most results are formalized in Mathlib (normEDS, preNormEDS) through a pull request.

Results

Standard EDSs are proven elliptic by purely algebraic means. Elliptic sequences over a field are classified into three types, most being dilated multiples of standard EDSs forming countably many 4-dimensional families. The results support an algebraic treatment of division polynomials in a follow-up paper.