feat(NumberTheory/EllipticDivisibilitySequence): prove that a normalised elliptic divisibility sequence is an elliptic sequence

[Multramate]

This is the updated version of #13155 and contains the proof that a sequence satisfying the even and odd elliptic relations (with mild additional conditions) is an elliptic net and hence an elliptic sequence. This is the main argument in Section 2 of Junyan's paper. Previously it was broken down into hundreds of lines of multiple lemmas but I was able to condense it into a single lemma with multiple wlogs that are hopefully self-explanatory.

Co-authored-by: Junyan Xu junyanxu.math@gmail.com

---

• depends on: feat(NumberTheory/EllipticDivisibilitySequence): add some lemmas and grind some proofs #42477

[github-actions]

PR summary e602d4575c

Import changes exceeding 2%

%	File
+45.50%	Mathlib.NumberTheory.EllipticDivisibilitySequence

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.EllipticDivisibilitySequence	745	1084	+339 (+45.50%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree	1
Mathlib.NumberTheory.EllipticDivisibilitySequence	339

---

Declarations diff (regex)

+ X_mem_nonZeroDivisors
+ atomRel_abs
+ atomRel_even
+ atomRel_neg
+ atomRel_odd
+ atomRel_of_even_odd
+ atomRel_perm
+ atom_mul_atomRel
+ atom_mul_atomRel_fst
+ atom_mul_atomRel_snd
+ isEllipticSequence_normEDS
+ neg_atomRel₁₂
+ neg_atomRel₂₃
+ neg_atomRel₃₄
+ normEDS_atomRel_even
+ normEDS_atomRel_odd
+ normEDS_rel_even
+ normEDS_rel_odd
++ of_even_odd
++++ comp

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e602d45).

• +24 new declarations
• −0 removed declarations

+IsDvdSequence.comp
+IsEllipticDvdSequence.comp
+IsEllipticNet.atomRel_abs
+IsEllipticNet.atomRel_even
+IsEllipticNet.atomRel_neg
+IsEllipticNet.atomRel_odd
+IsEllipticNet.atomRel_of_even_odd
+IsEllipticNet.atomRel_perm
+IsEllipticNet.atom_mul_atomRel
+IsEllipticNet.atom_mul_atomRel_fst
+IsEllipticNet.atom_mul_atomRel_snd
+IsEllipticNet.comp
+IsEllipticNet.neg_atomRel₁₂
+IsEllipticNet.neg_atomRel₂₃
+IsEllipticNet.neg_atomRel₃₄
+IsEllipticNet.of_even_odd
+IsEllipticSequence.comp
+IsEllipticSequence.of_even_odd
+Polynomial.X_mem_nonZeroDivisors
+isEllipticSequence_normEDS
+normEDS_atomRel_even
+normEDS_atomRel_odd
+normEDS_rel_even
+normEDS_rel_odd

---

Increase in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
499	1	erw

No changes to weak technical debt.

Current commit e602d4575c
Reference commit d0060d7bbb

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[tb65536]

Can you add a PR description?

[Copilot]

🟡 Not ready to approve

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean removes tactic imports but still uses linarith/ring1, which leaves them out of scope and will break compilation.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

This review doesn't count toward merge requirements. Sign up for the private preview to control whether Copilot approvals count.

Pull request overview

This PR extends the elliptic divisibility sequence development by adding infrastructure to transport “elliptic(-net/sequence/EDS)” predicates across scalar multiplication and ring homomorphisms, and then uses these tools to show the canonical normalised EDS normEDS satisfies IsEllipticSequence.

Changes:

• Adds permutation/parity/normalisation lemmas for atomRel/rel, plus “even/odd relations ⇒ elliptic net/sequence” constructors.
• Proves the main new result isEllipticSequence_normEDS : IsEllipticSequence (normEDS b c d).
• Adds a general IsDvdSequence.map lemma to compose divisibility sequences.

File summaries

File	Description
Mathlib/NumberTheory/EllipticDivisibilitySequence.lean	Adds new lemmas and the main theorem isEllipticSequence_normEDS, plus mapping/smul infrastructure.
Mathlib/Data/Nat/DvdSequence.lean	Adds IsDvdSequence.map to compose two divisibility sequences.

Review details

• Files reviewed: 2/2 changed files
• Comments generated: 1
• Review effort level: Lite

We're testing this review assessment. Please use 👍 or 👎 to tell us if it's correct.

[tb65536]

Not the biggest fan of convert since it can hide defeq problems.

Suggested change

	convert IsEllipticSequence.of_even_odd (normEDS_neg X (C c) (C d)) (by simp)
	(by simpa using isRegular_X.mem_nonZeroDivisors) (normEDS_rel_even _ _ _)
	(normEDS_rel_odd _ _ _) |>.comp <| evalRingHom b
	ext; simp_rw [Function.comp_apply, map_normEDS, coe_evalRingHom, eval_X, eval_C]
	have key : normEDS b c d = evalRingHom b ∘ normEDS X (C c) (C d) := by
	ext; simp_rw [Function.comp_apply, map_normEDS, coe_evalRingHom, eval_X, eval_C]
	rw [key]
	exact IsEllipticSequence.of_even_odd (normEDS_neg X (C c) (C d)) (by simp)
	(by simpa using isRegular_X.mem_nonZeroDivisors) (normEDS_rel_even _ _ _)
	(normEDS_rel_odd _ _ _) |>.comp <| evalRingHom b

[Multramate]

I'm not convinced of this: you're just changing the convert to an exact, which also potentially hides defeq problems, and now it's longer with a have that I do not like :)

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(NumberTheory/EllipticDivisibilitySequence): add some lemmas and grind some proofs #42477
  By Dependent Issues (🤖). Happy coding!