An elliptic sequence is determined by its first four terms

Two elliptic sequences that agree at 1, 2, 3, 4 are equal, provided the first two terms are nonzerodivisors. The two doubling recurrences determine every later term from a bounded window of earlier ones — five for the even step, four for the odd — Elementary.lean supplies the value at 0 and the behaviour at negative indices, and normEDSRec is the induction that puts those together.

Main results

• IsEllipticSequence.ext: W = U from agreement at 1, 2, 3, 4.

Implementation notes

The recurrences give the doubled-index term only up to a nonzerodivisor factor — W 2 * W 1 ^ 2 at even indices and W 1 ^ 3 at odd ones, which is exactly the shape Recurrence.lean's docstring flags as needing "a hypothesis this file does not carry". Each inductive step therefore cancels that factor before comparing, which is where one and two are used.

normEDSRec is indexed by ℕ while the recurrences are stated over ℤ, so each step pushes the cast through before rewriting; Int.negInduction then reduces negative indices to nonnegative ones through oddness.

The index arithmetic then needs ring_nf. rel_even at m + 3 writes its indices as m + 3 - 1 and so on, while the induction hypotheses are stated at m + 2; W is opaque, so nothing equates those two terms until both are in normal form. Once they are, rewriting the hypotheses through the W side of the recurrence leaves it with the same right-hand side as the U side, and the two subtract.

Provenance

Adapted from D. K. Angdinata's LutzNagell/EllipticDivisibilitySequence.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, main at 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), declaration IsEllSequence.ext. That file's header reads Authors: David Kurniadi Angdinata; following this repository's convention for adapted material the upstream authorship is credited here rather than in the copyright header. J. Xu is acknowledged for the surrounding LutzNagell development — he authors Universal.lean and co-authors DivisionPolynomialOmega.lean at the same revision — as context for this port, not as an author of the declaration above.

The source derives the value at 0 and the oddness inline from its own zero and neg; here those are Elementary.lean's IsEllipticSequence.zero and IsEllipticSequence.neg, so this file is the induction alone.

theorem IsEllipticSequence.ext {R : Type u_1} [CommRing R] {W U : ℤ → R} (hW : IsEllipticSequence W) (hU : IsEllipticSequence U) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (h1 : W 1 = U 1) (h2 : W 2 = U 2) (h3 : W 3 = U 3) (h4 : W 4 = U 4) : W = U

An elliptic sequence is determined by its first four terms. Two elliptic sequences agreeing at 1, 2, 3, 4 are equal, given that W 1 and W 2 are nonzerodivisors.