An elliptic net from its two doubling recurrences

IsEllipticNet W is a condition on every quadruple of integers, IsEllipticSequence W on every triple. This file proves both equivalent to two families of equations indexed by a single integer — the odd doubling recurrence from m = 2 on and the even one from m = 3 on — for a sequence that is odd, vanishes at 0, and has W 1 and W 2 nonzerodivisors.

The forward direction is Recurrence.lean. The reverse is the descent proved here, by induction on the largest index a:

• below 6 there is no valid quadruple at all, four nonnegative same-parity indices in strict decrease forcing 6 ≤ a (Transfer.lean);
• above it, a relator on four unconstrained indices is rewritten into relators carrying a fixed pair of small indices, by the three-term and ten-term expansions below;
• that reduces to the minimal same-parity pair (a % 2 + 2, a % 2), where either b + 2 < a admits the transfer down to a smaller first index, or b + 2 = a lands on one of the two recurrences, chosen by the parity of a.

Arbitrary indices are then reduced to a valid quadruple: absolute values make them nonnegative, coincidences collapse through Mathlib's atomRel_same family, and the rest are sorted.

The expansions are polynomial identities in the atoms — atomRel is a fixed quadratic expression in atom, so both sides expand to combinations of products of two atoms and ring closes them. No index arithmetic is involved, which is why they need none of the parity hypotheses that atom_even, atom_odd and atomRel_eq carry.

Main results

• isEllipticNet_iff: the equivalence at four indices, and the headline result of the file.
• isEllipticSequence_iff: the classical three-index equivalence, its s = 0 case.
• IsEllipticNet.of_rel: the hard direction of the first, with the recurrences in relator form.
• IsEllipticNet.atom_mul_atomRel_eq_of_last_eq_fst, …_of_last_eq_snd, IsEllipticNet.atom_mul_atomRel_eq: the three-term and ten-term expansions that drive it.

Implementation notes

The descent itself is private. AtomRelVanishes and the three lemmas lowering it are shaped by this proof rather than by any consumer, and the interface a caller wants is the equivalence and its hard direction.

Both levels are stated. isEllipticNet_iff is the stronger statement and everything is proved through it, but IsEllipticSequence is the predicate Mathlib defines and that IsEllipticDvdSequence is built from, so the three-index equivalence is kept named rather than left as (isEllipticNet_iff …).mpr … |>.isEllipticSequence at each use. The relator-form isEllipticSequence_of_rel is not kept: it restated IsEllipticNet.of_rel in the spelling this file uses internally, and had no consumer.

That predicate carries the parity and ordering conditions inside it. The induction applies its hypothesis at quadruples whose validity is not known in advance, so the recursive call has to be a statement about indices alone.

The antisymmetry of atomRel under transpositions is not proved here: SignEquivariance.lean already exports atomRel_swap₁₂, atomRel_swap₂₃ and atomRel_swap₃₄, together with the general atomRelFin4_perm. It is that general form the sorting uses. The net has no distinguished index — rel_eq produces the quadruple (2p + s, 2q + s, 2r + s, s), in which s is free — so all four are sorted, by Tuple.sort composed with the reversal, rather than three against a fixed 0.

Two parts of the source's apparatus are not needed here, each because Mathlib has absorbed the layer that made them necessary. Its rel₄_transf is atomRel_avg_sub; and its minimal-index definition if Even a then 0 else 1, with five Int.negOnePow lemmas about it, is a % 2, about which everything needed is omega. Its Tuple.sort argument over four indices is needed, and is used.

Provenance

Adapted from D. K. Angdinata's LutzNagell/EllipticDivisibilitySequence.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, main at 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), declarations rel₆_eq₃, rel₆_eq₃', rel₆_eq₁₀, rel₄_iff_evenRec, dMin, cMin, Rel₄OfValid, rel₄_fix₁_of_fix₂, rel₄_of_fix₂, rel₄_of_min₂, rel₄_of_anti_oddRec_evenRec, rel₄_of_oddRec_evenRec and IsEllSequence.of_oddRec_evenRec. 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 declarations above.

The four-index sorting and the net entry point adapt two further declarations of that same file, IsEllSequence.rel₄ and IsEllSequence.net.

The source states its expansions against its own addMulSub and rel₄, which Mathlib now supplies as atom and atomRel with the same definitions, so those statements transfer by renaming. Three of its declarations are deliberately not ported. Its rel₆ abbreviation for addMulSub W k l * rel₄ W a b c d, with the @[simp] lemma unfolding it, names a product rather than a concept and exists only to shorten four statements, so it would stand a second public spelling of atom _ _ * atomRel _ _ _ _; the statements below write the product out. Its addMulSub_sq_mul_rel₄_eq₉, the nine-term expansion, is unused in the source itself — it occurs there only at its own declaration — and this descent does not need it. Its swap family rel₄_swap₀₁, rel₄_swap₁₂, rel₄_swap₂₃ and the relFin4_perm built on them are already in this repository as SignEquivariance.lean, and are used from there.

rel₄_iff_evenRec is the one source declaration carrying set_option allowUnsafeReducibility true together with attribute [local reducible] Nat.rawCast, which #2860 declined to bring into this repository. Stating the base cases with indices in 2 * _ and 2 * _ + 1 form lets atomRel_two_mul and atom_odd apply directly, so neither the option nor the attribute appears here.

theorem IsEllipticNet.atom_mul_atomRel_eq_of_last_eq_fst {R : Type u_1} [CommRing R] (W : ℤ → R) (c d m n r : ℤ) : atom W c d * atomRel W m n r c = atom W m c * atomRel W n r c d - atom W n c * atomRel W m r c d + atom W r c * atomRel W m n c d

Expanding over a fixed pair, when the relator already ends at the atom's first index. Each relator on the right carries both c and d, so this trades one occurrence of c for the pair c, d.

theorem IsEllipticNet.atom_mul_atomRel_eq_of_last_eq_snd {R : Type u_1} [CommRing R] (W : ℤ → R) (c d m n r : ℤ) : atom W c d * atomRel W m n r d = atom W m d * atomRel W n r c d - atom W n d * atomRel W m r c d + atom W r d * atomRel W m n c d

Expanding over a fixed pair, when the relator already ends at the atom's second index. The companion of atom_mul_atomRel_eq_of_last_eq_fst with the roles of c and d exchanged in the atoms, the relators on the right being the same three.

theorem IsEllipticNet.atom_mul_atomRel_eq {R : Type u_1} [CommRing R] (W : ℤ → R) (c d m n r s : ℤ) : atom W c d * atomRel W m n r s = atom W n d * atomRel W m r s c - atom W r d * atomRel W m n s c + atom W s d * atomRel W m n r c + atom W n c * atomRel W m r s d - atom W r c * atomRel W m n s d + atom W s c * atomRel W m n r d + atom W n r * atomRel W m s c d - atom W n s * atomRel W m r c d + atom W r s * atomRel W m n c d - 2 * (atom W m d * atomRel W n r s c)

Expanding over a fixed pair, for four unconstrained relator indices. Every relator on the right has at least one index drawn from the fixed pair c, d, which is what lets the descent lower the indices it is working on.

theorem IsEllipticNet.of_rel {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (zero : W 0 = 0) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (oddRec : ∀ (m : ℤ), 2 ≤ m → rel W (m + 1) m 1 0 = 0) (evenRec : ∀ (m : ℤ), 3 ≤ m → rel W (m + 1) (m - 1) 1 0 = 0) : IsEllipticNet W

An elliptic net from the two doubling recurrences. A sequence that is odd, vanishes at 0, has W 1 and W 2 nonzerodivisors, and satisfies the odd recurrence from m = 2 and the even one from m = 3, satisfies the full four-index relation at every quadruple.

theorem isEllipticNet_iff {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (zero : W 0 = 0) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) : IsEllipticNet W ↔ (∀ (m : ℤ), 2 ≤ m → W (2 * m + 1) * W 1 ^ 3 = W (m + 2) * W m ^ 3 - W (m - 1) * W (m + 1) ^ 3) ∧ ∀ (m : ℤ), 3 ≤ m → W (2 * m) * W 2 * W 1 ^ 2 = W m * (W (m - 1) ^ 2 * W (m + 2) - W (m - 2) * W (m + 1) ^ 2)

Being an elliptic net is exactly satisfying the two doubling recurrences. For a sequence that is odd, vanishes at 0 and has W 1, W 2 nonzerodivisors, the four-index relation at every quadruple is equivalent to the odd recurrence from m = 2 and the even one from m = 3 — finitely many equations per index rather than a condition on quadruples.

Under these hypotheses, therefore, being an elliptic net and being an elliptic sequence are the same condition. They are not the same condition in general: normEDS b c d at arbitrary parameters need not have W 2 = b a nonzerodivisor, and NormEDS.lean obtains the net there without this equivalence.

theorem isEllipticSequence_iff {R : Type u_1} [CommRing R] {W : ℤ → R} (odd : Function.Odd W) (zero : W 0 = 0) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) : IsEllipticSequence W ↔ (∀ (m : ℤ), 2 ≤ m → W (2 * m + 1) * W 1 ^ 3 = W (m + 2) * W m ^ 3 - W (m - 1) * W (m + 1) ^ 3) ∧ ∀ (m : ℤ), 3 ≤ m → W (2 * m) * W 2 * W 1 ^ 2 = W m * (W (m - 1) ^ 2 * W (m + 2) - W (m - 2) * W (m + 1) ^ 2)

Being an elliptic sequence is exactly satisfying the two doubling recurrences. For a sequence that is odd, vanishes at 0 and has W 1, W 2 nonzerodivisors, the whole three-index relation is equivalent to the odd recurrence from m = 2 and the even one from m = 3 — finitely many equations per index rather than a condition on triples.

This is the classical statement, about the predicate IsEllipticSequence; isEllipticNet_iff is its four-index strengthening.