feat(NumberTheory/EllipticDivisibilitySequence): show elliptic relations follow from even-odd recursion

[alreadydone]

This PR is centered around the (generalized) elliptic relations (rel₄)
$E(a,b,c,d): W_{a+b}W_{a-b}W_{c+d}W_{c-d}=W_{a+c}W_{a-c}W_{b+d}W_{b-d}-W_{a+d}W_{a-d}W_{b+c}W_{b-c}$.
For an integer-indexed sequence W valued in a commutative ring, the relation makes sense only when a,b,c,d are all integers or all half integers. For convenience of formalization, we instead consider integers a,b,c,d of the same parity and divide all subscripts by 2. We extract the subexpression $W_{(a+b)/2}W_{(a-b)/2}$ (which appear six times) as addMulSub W a b.

The collection of all $E(a,b,c,d)$ is equivalent to Stange's axiom for elliptic nets (net), and the literature (e.g. Silverman) commonly consider only the three-index special case $E(m,n,r,0)$ (Rel₃). Important special cases of these relations are
(i) $E(m+1,m,1,0): W_{2m+1}W_1^3=W_{m+2}W_m^3-W_{m+1}^3 W_{m-1}$ (oddRec) and
(ii) $E(m+1,m-1,1,0): W_{2m}W_2 W_1^2=W_m(W_{m+2}W_{m-1}^2-W_{m-2}W_{m+1}^2)$ (evenRec),
which suffice to uniquely specify $W$ on all positive integers recursively from four initial values $W_1, W_2, W_3, W_4$ (IsEllSequence.ext, if $W_1 W_2$ is not a zero divisor). In the usual setting where $W_1=1$ and $W_2\mid W_4$, there does exist a sequence (normEDS) satisfying (i) and (ii) given initial values $W_2, W_3$ and $W_4/W_2$. It turns out the same non-zerodivisor condition also guarantees that W is an odd function with $W_0=0$, which naturally extends W to all integers.

The main result of this PR (rel₄_of_oddRec_evenRec, IsEllSequence.of_oddRec_evenRec) is a purely algebraic proof that the sequence W defined by the single-parameter elliptic relations (i) and (ii) implies all $E(a,b,c,d)$, based on my original argument first published on Math.SE. It's based on the observation that a nonzerodivisor-multiple of $E(a,b,c,d)$ can be expressed as a linear combination of various $E(a,b,c_\min,d_\min)$ with the two smallest indices fixed at their minimal possible values, which can be transformed (transf) to an elliptic relation with smaller a (which can be assumed to hold by induction), unless they are of the form (i) or (ii) which hold by assumption. For this argument it's necessary to assume a > b > c > d ≥ 0 (see StrictAnti₄ and Rel₄OfValid), but it's easy to extend to arbitrary a,b,c,d by symmetry properties of rel₄ under negation and permutations of indices.

In the subsequent PR #13057, we show all normalized EDSs (normEDS), defined using the even-odd recursion (i)-(ii), are elliptic (i.e. satisfy the elliptic relations) divisibility sequences. This PR doesn't directly apply because a normEDS doesn't always satisfy the nonzerodivisor condition, but they are specializations of the universal normEDS, which does satisfy the condition. The technique of reducing to the universal case will be applied many times, and relies on the naturality (map) lemmas.

We also change the ℕ in the definition IsDivSequence to ℤ which is more natural given that W is a ℤ-indexed sequence.

---

• depends on: [Merged by Bors] - feat(Algebra): auxiliary results for proofs about elliptic divisibility sequences #13153

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Algebra): auxiliary results for proofs about elliptic divisibility sequences #13153
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

Requesting a review from @Multramate since you're probably the only one who've read my proof on StackExchange :)

[alreadydone]

Hi @Multramate do you have plans to review this in the near future? If there's any difficulty please let me know.

[Multramate]

I'll give a brief review today. I won't have much time this week and next week, but I'll do the full review after that.

[Multramate]

Here are some very preliminary comments on the naming mostly on the first half of the PR, without looking at the code or referring to your notes. I still think that this is a massive PR, especially since your argument is new. There isn't an obvious structure to the lemmas even if I understood the entire argument, and many definitions seem to just be auxiliary to prove some small part of the argument. I reckon will take very a long time to review, so I still suggest that you find a way to split this further.

[Multramate]

I feel that the stuff on elliptic nets may deserve its own file, maybe EllipticNet.lean, or we can make EllipticDivisibilitySequence a folder and split this file into two subfiles. In any case, I think you should elaborate this in detail in the module docstrings, and do add a reference to Stange's paper or otherwise.

[alreadydone]

I think splitting this to another file would break the coherence and the flow of this file, since net is closely connected (equivalent) to rel₄. I would only consider splitting if we want to define net more generally on arbitrary abelian groups instead of ℤ.

I agree I should mention it in module docstring and add the reference.

[Multramate]

We should still have a reference on your entire MSE argument somewhere. I would personally just write it all out in the module docstrings, but you can also just add a link to the MSE answer. Once you've incorporated it to the notes (or write a paper containing the argument), you should link that instead.

On the stuff on elliptic nets: it seems that you don't actually use nets in the proof of _root_.IsEllSequence.of_oddRec_evenRec, which was supposed to be the main theorem in this PR? I suggest omitting these entirely in this PR.

If you were to define net, you should split it eventually into its own file, partly to set up a precedent to develop the general theory over abelian groups, and partly because it's going to be very long once we add the code from the other PRs.

[Multramate]

I'm not a huge fan of the subscript naming, unless it's something like $\psi_2$ where we're defining a sequence. This could instead be some mixture of the keywords addMulSub, mul, add, sub, cyclic, partition, etc.

[alreadydone]

The subscript means the number of arguments, and I'm using this convention consistently in this file. It's not uncommon to use subscripts to indicate the number of arguments involved, see e.g. congr_fun₃ and norm_add₃_le.

This is a term (unlike Rel₃, which is a Prop), but I use the same name (just different capitalization) because its close connection to Rel₃.

Again note that this is defined in terms of addMulSub and both are auxiliary to the proof so we shouldn't care much about the name. It's equivalent to net but net is easier to use. (We could consider making both private, but then you won't see them in the online docs. Maybe it doesn't matter because if anyone wants to understand the proof they would need to look at the source code anyway.)

[Multramate]

This name doesn't reflect the div 2, but I can't think of a better name.

[alreadydone]

I can add a subscript 2 but this def is auxiliary to the proof and not expected to be used outside of this file, so I don't care much about its name ... It's also an implementation detail, it's inconvenient to make a type for $\frac12\mathbb{Z}$ in Lean so we use $\mathbb{Z}$ instead, and that's why we need to divide by 2.

[Multramate]

Ditto, and note that this is a relation (so Rel still makes sense), but rel₄ is an element of R so it should be called something else.

[alreadydone]

See above; I want to keep the name of rel₄ to stress close connection with Rel₃ (see rel₃_iff₄), but I should probably make rel₄ private.

[Multramate]

Here is my suggestion: make this into an term rel₃ of R rather than a Prop, and replace instances of Rel₃ elsewhere with rel₃ .. = 0. I prefer keeping this analogous to rel₄ (especially if you decide to expose it, but also for people who might read the source code), and lemmas like rel₃_iff_rel₄_eq_zero suggest that rel₃ and rel₄ are terms of the same type. In any case, 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 = 0 might be more suggestive of its cyclic nature.

I still don't quite like rel because that suggests a Prop, but I guess it's a "relator" rather than a "relation".

[Multramate]

Spell out average?

[alreadydone]

I don't want to make it longer because it appears a lot of times. I can make it private though.

[alreadydone]

Thanks, pushed some initial fixes.

[alreadydone]

I can add a subscript 2 but this def is auxiliary to the proof and not expected to be used outside of this file, so I don't care much about its name ... It's also an implementation detail, it's inconvenient to make a type for $\frac12\mathbb{Z}$ in Lean so we use $\mathbb{Z}$ instead, and that's why we need to divide by 2.

[alreadydone]

The subscript means the number of arguments, and I'm using this convention consistently in this file. It's not uncommon to use subscripts to indicate the number of arguments involved, see e.g. congr_fun₃ and norm_add₃_le.

This is a term (unlike Rel₃, which is a Prop), but I use the same name (just different capitalization) because its close connection to Rel₃.

Again note that this is defined in terms of addMulSub and both are auxiliary to the proof so we shouldn't care much about the name. It's equivalent to net but net is easier to use. (We could consider making both private, but then you won't see them in the online docs. Maybe it doesn't matter because if anyone wants to understand the proof they would need to look at the source code anyway.)

[alreadydone]

I think splitting this to another file would break the coherence and the flow of this file, since net is closely connected (equivalent) to rel₄. I would only consider splitting if we want to define net more generally on arbitrary abelian groups instead of ℤ.

I agree I should mention it in module docstring and add the reference.

[alreadydone]

See above; I want to keep the name of rel₄ to stress close connection with Rel₃ (see rel₃_iff₄), but I should probably make rel₄ private.

[alreadydone]

I don't want to make it longer because it appears a lot of times. I can make it private though.

[Multramate]

Here are some further preliminary comments. Now that I've some time to try to understand the code organisation, I feel that we should extract out all the stuff not directly necessary in the proof of the main result (i.e. the stuff on net and invarNum/Denom).

[Multramate]

I think these will end up in the same line, so maybe you want to do:

Suggested change

	M. Ward, *Memoir on Elliptic Divisibility Sequences*
	[K Stange, *Elliptic nets and elliptic curves*][Stange2011]
	* M. Ward, *Memoir on Elliptic Divisibility Sequences*
	* [K Stange, *Elliptic nets and elliptic curves*][Stange2011]

I was told to indent them by one space to make formatting work properly.

While you're at this, can you add the proper reference to Ward's article in the mathlib bibliography (and remove the . in M. to make it consistent)?

[Multramate]

We should still have a reference on your entire MSE argument somewhere. I would personally just write it all out in the module docstrings, but you can also just add a link to the MSE answer. Once you've incorporated it to the notes (or write a paper containing the argument), you should link that instead.

On the stuff on elliptic nets: it seems that you don't actually use nets in the proof of _root_.IsEllSequence.of_oddRec_evenRec, which was supposed to be the main theorem in this PR? I suggest omitting these entirely in this PR.

If you were to define net, you should split it eventually into its own file, partly to set up a precedent to develop the general theory over abelian groups, and partly because it's going to be very long once we add the code from the other PRs.

[Multramate]

I guess if we were to make this private, we won't need the docstring, so maybe make these /- -/ instead?

Do you think it's better if we make literally everything except _root_.IsEllSequence.of_oddRec_evenRec (including cMin and dMin) private? If everything were to be private, I guess I don't care about the code...

I don't actually know how I feel about making this (and rel₄, etc) private. On one hand it's an implementation detail, but on the other hand the facts about rel₄ are fine results on their own that are highly symmetric.

[Multramate]

If we hide rel₄, then we can't talk about it here.

[Multramate]

I haven't read through your notes, but from the MSE answer and the main comment in this PR, these are unrelated to _root_.IsEllSequence.of_oddRec_evenRec, which was supposed to be the main theorem in this PR?

[Multramate]

What is the recommended symbol to use here? I always used => but you always use ↦.

[Multramate]

Seems like these and everything below are unrelated to _root_.IsEllSequence.of_oddRec_evenRec, but instead a consequence of rel₄_of_oddRec_evenRec and the lemmas for invarNum/Denom, and only added here because it's part of a downstream PR. I hope this is not too much work, but given the size of the PR (and the novelty of the argument), I suggest that you split off everything that's not directly related to the main argument.

[Multramate]

You should certainly add your name here.

[Multramate]

Here is my suggestion: make this into an term rel₃ of R rather than a Prop, and replace instances of Rel₃ elsewhere with rel₃ .. = 0. I prefer keeping this analogous to rel₄ (especially if you decide to expose it, but also for people who might read the source code), and lemmas like rel₃_iff_rel₄_eq_zero suggest that rel₃ and rel₄ are terms of the same type. In any case, 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 = 0 might be more suggestive of its cyclic nature.

I still don't quite like rel because that suggests a Prop, but I guess it's a "relator" rather than a "relation".

[Multramate]

My opinion on ring_nf is that it should never be used in the final code. Instead it's just a way to understand the expressions on both sides while proving a result, to be replaced with ring at the end (I prefer ring1 because it would fail if both sides are not identical). It might be only my side but I also feel that ring_nf is significantly slower than ring1 when compiling. Its behaviour should (heuristically) be identical to ring1, otherwise it's a bug...

[grunweg]

@alreadydone Coming here for PR triage, it seems this PR is waiting for you to respond to the review comments. (You also have a merge conflict.) I have thus labelled it awaiting-author. Please remove this label when this is ready for review again. Thanks!