feat(EllipticCurve): zsmul formula in terms of division polynomials (WIP, bump of #13782) - #41197
feat(EllipticCurve): zsmul formula in terms of division polynomials (WIP, bump of #13782)#41197kbuzzard wants to merge 94 commits into
Conversation
…acobian.Representative
…ve.Jacobian.Point
…acobian.Representative
…acobian.Representative
…ve.Jacobian.Point
…er-community/mathlib4 into DivisionPolynomial_smul
…l_smul # Conflicts: # Mathlib.lean # Mathlib/Algebra/Polynomial/Bivariate.lean # Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean # Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean # Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean # Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean # Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
Bump the original PR (leanprover-community#13782) to current mathlib (Lean v4.32.0-rc1), porting the content onto the refactored EllipticCurve directory and the new module system. The mathematical content is lifted from Junyan Xu's near-current port in CBirkbeck/AINTLIB (same toolchain, ~80 commits behind master), which had already adapted these proofs to the current API: * extend `EllipticDivisibilitySequence.lean` with `net`/`invar`/`addMulSub`, even-odd recursion (`IsEllSequence.of_oddRec_evenRec`), and the `complEDS`/`redInvar` machinery; * add `EllipticCurve/Universal.lean` (universal Weierstrass curve, coordinate ring, specialization homomorphisms, cusp curve); * add `DivisionPolynomial/Omega.lean` (the `ω` family, `ψc`, `invar`); * add `DivisionPolynomial/ZSMul.lean` with the main result `WeierstrassCurve.zsmul_eq_smulEval`: `n • P = (φₙ(x,y) : ωₙ(x,y) : ψₙ(x,y))` in Jacobian coordinates. `DivisionPolynomial/Basic.lean` needs two small adjustments: eta-reduce `ψ` (required by the downstream `rw [ψ]`/`rw [← ψ]` proofs) and pass the `map_preNormEDS`/`map_normEDS` lemmas explicitly (they are no longer `@[simp]`). Everything compiles; `zsmul_eq_smulEval` uses only the standard axioms. WIP. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk> Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
github-actions
Bot
added
the
large-import
PR summary f46c499f84Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.NumberTheory.EllipticDivisibilitySequence | 633 | 1389 | +756 (+119.43%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree |
2 |
Mathlib.NumberTheory.EllipticDivisibilitySequence |
756 |
Mathlib.AlgebraicGeometry.EllipticCurve.Universal (new file) |
1792 |
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Omega (new file) |
1798 |
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.ZSMul (new file) |
1799 |
Declarations diff (regex)
+ Affine.point
+ C_Ψ₃_eq
+ Coeff
+ EllSequence.map_compl
+ EllSequence.map_compl'
+ EvenRec
+ Field
+ Field.two_ne_zero
+ HaveSameParity₄
+ IsDivSequence.map
+ IsDivSequence.normEDS
+ IsEllDivSequence.eq_normEDS
+ IsEllDivSequence.map
+ IsEllDivSequence.normEDS
+ IsEllSequence.eq_normEDS_of_dvd
+ IsEllSequence.ext
+ IsEllSequence.isDivSequence_of_dvd
+ IsEllSequence.isEllDivSequence_of_dvd
+ IsEllSequence.map
+ IsEllSequence.mul_compl_eq_apply_mul_of_mem_nonZeroDivisors
+ IsEllSequence.normEDS
+ IsEllSequence.normEDS_of_mem_nonZeroDivisors
+ Jacobian.point
+ OddRec
+ Param
+ Poly
+ Poly.two_ne_zero
+ Rel₃
+ Rel₄OfValid
+ Ring
+ StrictAnti₄
+ _root_.IsEllSequence
+ _root_.IsEllSequence.of_oddRec_evenRec
+ abs
+ addMulSub
+ addMulSub_abs₀
+ addMulSub_abs₁
+ addMulSub_even
+ addMulSub_mem_nonZeroDivisors
+ addMulSub_neg₀
+ addMulSub_neg₁
+ addMulSub_odd
+ addMulSub_same
+ addMulSub_sq_mul_rel₄_eq₉
+ addMulSub_swap
+ addMulSub_three_one
+ addMulSub_transf
+ addMulSub_two_zero
+ addMulSub₄
+ addMulSub₄_mul_addMulSub₄
+ addXYZ_smulEval
+ addXYZ_smulEval₁
+ addXYZ_smulField
+ addXYZ_smulField₁
+ addXYZ_smulRing
+ addXYZ_smulRing₁
+ addX_smul_one_smul_one
+ addX_smul_one_smul_one_aux
+ addX_smul_ring_identity
+ addY_smul_one_smul_one
+ addY_smul_one_smul_one_aux
+ addZ_smulPoly
+ add_point_of_ne_eq_addXYZ
+ algebraMap_comp_smulRing
+ algebraMap_field_eq_comp
+ algebraMap_field_injective
+ algebraMap_injective'
+ algebraMap_poly_injective
+ algebraMap_ring_eq_comp
+ avg₄
+ avg₄_add_avg₄
+ cMin
+ compl
+ compl'
+ complEDS
+ complEDS_eq_aeval
+ compl_neg
+ compl_ofNat
+ compl₂EDS
+ compl₂EDSAux
+ compl₂EDSAux_mul_b
+ compl₂EDSAux_neg
+ compl₂EDSAux_neg_one
+ compl₂EDSAux_neg_two
+ compl₂EDSAux_one
+ compl₂EDSAux_two
+ compl₂EDSAux_zero
+ compl₂EDS_eq_aeval
+ compl₂EDS_eq_redInvarNum_sub
+ compl₂EDS_mul_b
+ compl₂EDS_neg
+ compl₂EDS_one
+ compl₂EDS_two
+ compl₂EDS_two_three_two
+ compl₂EDS_zero
+ curve
+ curveField
+ curveField_eq
+ curvePoly
+ curveRing
+ curveRing_map_ringEval
+ cusp
+ cusp_equation_one_one
+ cusp_preΨ₄
+ cusp_Ψ₃
+ cusp_ψ₂
+ dMin
+ dMin_le
+ dMin_lt_cMin
+ dMin_nonneg
+ dblXYZ_smulEval
+ dblXYZ_smulField
+ dblXYZ_smulRing
+ dblZ_smulPoly
+ equation_point
+ evalEval_preΨ₄
+ evalEval_Ψ₃
+ evalEval_φ
+ evalEval_ψ
+ evalEval_ψ₂
+ evalEval_ω
+ evenRec
+ even_sum
+ instance : AddGroup ((curve.baseChange Universal.Field).toAffine.Point) := inferInstance
+ instance : CommRing Poly := Polynomial.commRing /- why is this not automatic ... -/
+ instance : pointedCurve.IsElliptic
+ invarDenom
+ invarDenom_eq_redInvarDenom_mul
+ invarDenom_normEDS_two
+ invarNum
+ invarNum_eq_redInvarNum_mul
+ invarNum_normEDS
+ invarNum_normEDS_two
+ invar_normEDS
+ invar_of_net
+ invar₂_normEDS
+ invar₂_normEDS_of_mem_nonZeroDivisors
+ isEllSequence_ψ
+ isEllSequence_ψᵤ
+ map_addMulSub
+ map_complEDS_root
+ map_compl₂EDS
+ map_compl₂EDSAux
+ map_invarDenom
+ map_invarNum
+ map_net
+ map_redInvarDenom
+ map_redInvarNum
+ map_rel₄
+ map_specialize
+ map_ω
+ neg
+ negOnePow_cMin
+ negOnePow_cMin_eq_dMin
+ negOnePow_dMin
+ net_add_sub_iff
+ net_eq_rel₄
+ net_normEDS
+ net_ψᵤ
+ nonsingular_smulField
+ nonsingular_smulX_smulY
+ normEDS_def
+ normEDS_dvd_two_mul
+ normEDS_eq_aeval
+ normEDS_mul_complEDS
+ normEDS_mul_complEDS_div
+ normEDS_mul_complEDS_of_mem
+ normEDS_mul_compl₂EDS
+ normEDS_six_eq_mul
+ normEDS_two_three_two
+ oddRec
+ perm
+ point_point
+ pointedCurve
+ pointedCurve_a₁
+ pointedCurve_a₂
+ pointedCurve_a₃
+ pointedCurve_a₄
+ pointedCurve_a₆
+ polyEval
+ polyEval_apply
+ polyEval_comp_eq_specialize
+ polyEval_cusp_φ
+ polyEval_cusp_ψ
+ polyEval_cusp_ψc
+ polyEval_cusp_ω
+ polyToField
+ polyToField_apply
+ polyToField_polynomial
+ polyToField_φ_ne_zero
+ polyToField_ψ₂Sq
+ preΨ₄_add_Ψ₂Sq_sq
+ preΨ₄_add_ψ₂_pow_four
+ redInvarDenom
+ redInvarDenom_one
+ redInvarDenom_two
+ redInvarDenom_zero
+ redInvarNum
+ redInvar_normEDS
+ redInvar_normEDS_of_mem_nonZeroDivisors
+ relFin4
+ relFin4_perm
+ relFin4_perm'
+ rel₃_iff_evenRec
+ rel₃_iff_oddRec
+ rel₃_iff₄
+ rel₄_abs
+ rel₄_eq_net
+ rel₄_fix₁_of_fix₂
+ rel₄_iff_evenRec
+ rel₄_normEDS
+ rel₄_of_anti_oddRec_evenRec
+ rel₄_of_fix₂
+ rel₄_of_min₂
+ rel₄_of_oddRec_evenRec
+ rel₄_same₀₁
+ rel₄_same₁₂
+ rel₄_same₂₃
+ rel₄_swap₀₁
+ rel₄_swap₁₂
+ rel₄_swap₂₃
+ rel₄_transf
+ rel₆
+ rel₆_eq
+ rel₆_eq₁₀
+ rel₆_eq₃
+ rel₆_eq₃'
+ ringEval
+ ringEval_comp_eq_specialize
+ ringEval_comp_mk
+ ringEval_comp_smulRing
+ ringEval_mk
+ ringEval_ψ
+ same₀₃
+ six_le_of_strictAnti₄
+ slopeOne
+ slopeOne_eq_neg_div
+ smulEval
+ smulField
+ smulField_neg
+ smulField_zero
+ smulPoly
+ smulPoly_neg
+ smulPoly_zero
+ smulRing
+ smulRing_neg
+ smulX
+ smulX_add
+ smulX_add_aux
+ smulX_eq
+ smulX_eq_smulX_iff
+ smulX_ne_smulX
+ smulX_ne_zero
+ smulX_neg
+ smulX_one
+ smulX_sub_smulX
+ smulX_sub_sub_smulX_add
+ smulX_two
+ smulX_zero
+ smulY
+ smulY_add_sub_negY
+ smulY_add_sub_negY_aux
+ smulY_neg
+ smulY_neg_aux
+ smulY_one
+ smulY_one_ne_negY
+ smulY_one_sub_negY
+ smulY_sub_negY
+ smulY_sub_negY_aux
+ smulY_zero
+ some_eq_some_iff
+ specialize
+ strictAnti₄_transf
+ sub_add_neg_sub_mul_eq_zero
+ transf
+ two_mul_ω
+ two_zsmul_point_eq_dblXYZ
+ universalNormEDS
+ universalNormEDS_mem_nonZeroDivisors
+ universalNormEDS_ne_zero
+ universal_ω_neg
+ zero
+ zero'
+ zsmul_eq_smulEval
+ zsmul_point_eq_smulField
+ zsmul_point_eq_smulX_smulY
+ zsmul_point_ne
+ Δ_curve_ne_zero
+ φ_mul_ψ
+ ψc
+ ψc_neg
+ ψc_spec
+ ψᵤ
+ ψᵤ_eq_normEDS
+ ψᵤ_ne_zero
+ ω
+ ω_neg
+ ω_neg_eq_neg_negY
+ ω_one
+ ω_spec
+ ω_zero
++ invar
++ net
++ rel₄
++ zsmul_point_ne_zero
- IsEllSequence
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
f46c499).
- +338 new declarations
- −17 removed declarations
(showing first 200 of 355 lines)
+EllSequence.EvenRec
+EllSequence.HaveSameParity₄
+EllSequence.HaveSameParity₄.abs
+EllSequence.HaveSameParity₄.addMulSub_transf
+EllSequence.HaveSameParity₄.addMulSub₄
+EllSequence.HaveSameParity₄.addMulSub₄_mul_addMulSub₄
+EllSequence.HaveSameParity₄.avg₄_add_avg₄
+EllSequence.HaveSameParity₄.even_sum
+EllSequence.HaveSameParity₄.perm
+EllSequence.HaveSameParity₄.rel₄_eq_net
+EllSequence.HaveSameParity₄.rel₄_transf
+EllSequence.HaveSameParity₄.same₀₃
+EllSequence.HaveSameParity₄.six_le_of_strictAnti₄
+EllSequence.HaveSameParity₄.strictAnti₄_transf
+EllSequence.HaveSameParity₄.transf
+EllSequence.OddRec
+EllSequence.Rel₃
+EllSequence.Rel₄OfValid
+EllSequence.StrictAnti₄
+EllSequence.addMulSub
+EllSequence.addMulSub_abs₀
+EllSequence.addMulSub_abs₁
+EllSequence.addMulSub_even
+EllSequence.addMulSub_mem_nonZeroDivisors
+EllSequence.addMulSub_neg₀
+EllSequence.addMulSub_neg₁
+EllSequence.addMulSub_odd
+EllSequence.addMulSub_same
+EllSequence.addMulSub_sq_mul_rel₄_eq₉
+EllSequence.addMulSub_swap
+EllSequence.addMulSub_three_one
+EllSequence.addMulSub_two_zero
+EllSequence.avg₄
+EllSequence.cMin
+EllSequence.compl
+EllSequence.compl'
+EllSequence.compl'.eq_def
+EllSequence.complEDS
+EllSequence.compl_neg
+EllSequence.compl_ofNat
+EllSequence.compl₂EDS_eq_redInvarNum_sub
+EllSequence.dMin
+EllSequence.dMin_le
+EllSequence.dMin_lt_cMin
+EllSequence.dMin_nonneg
+EllSequence.invarDenom
+EllSequence.invarDenom_eq_redInvarDenom_mul
+EllSequence.invarNum
+EllSequence.invarNum_eq_redInvarNum_mul
+EllSequence.invar_of_net
+EllSequence.map_compl
+EllSequence.map_compl'
+EllSequence.map_compl₂EDSAux
+EllSequence.map_redInvarDenom
+EllSequence.map_redInvarNum
+EllSequence.negOnePow_cMin
+EllSequence.negOnePow_cMin_eq_dMin
+EllSequence.negOnePow_dMin
+EllSequence.net
+EllSequence.net_add_sub_iff
+EllSequence.net_eq_rel₄
+EllSequence.redInvarDenom
+EllSequence.redInvarDenom_one
+EllSequence.redInvarDenom_two
+EllSequence.redInvarDenom_zero
+EllSequence.redInvarNum
+EllSequence.relFin4
+EllSequence.relFin4_perm
+EllSequence.relFin4_perm'
+EllSequence.rel₃_iff_evenRec
+EllSequence.rel₃_iff_oddRec
+EllSequence.rel₃_iff₄
+EllSequence.rel₄
+EllSequence.rel₄_abs
+EllSequence.rel₄_fix₁_of_fix₂
+EllSequence.rel₄_iff_evenRec
+EllSequence.rel₄_of_anti_oddRec_evenRec
+EllSequence.rel₄_of_fix₂
+EllSequence.rel₄_of_min₂
+EllSequence.rel₄_of_oddRec_evenRec
+EllSequence.rel₄_same₀₁
+EllSequence.rel₄_same₁₂
+EllSequence.rel₄_same₂₃
+EllSequence.rel₄_swap₀₁
+EllSequence.rel₄_swap₁₂
+EllSequence.rel₄_swap₂₃
+EllSequence.rel₆
+EllSequence.rel₆_eq
+EllSequence.rel₆_eq₁₀
+EllSequence.rel₆_eq₃
+EllSequence.rel₆_eq₃'
+IsDivSequence.map
+IsDivSequence.normEDS
+IsEllDivSequence.eq_normEDS
+IsEllDivSequence.map
+IsEllDivSequence.normEDS
+IsEllSequence.eq_normEDS_of_dvd
+IsEllSequence.evenRec
+IsEllSequence.ext
+IsEllSequence.invar
+IsEllSequence.isDivSequence_of_dvd
+IsEllSequence.isEllDivSequence_of_dvd
+IsEllSequence.map
+IsEllSequence.mul_compl_eq_apply_mul_of_mem_nonZeroDivisors
+IsEllSequence.neg
+IsEllSequence.net
+IsEllSequence.normEDS
+IsEllSequence.oddRec
+IsEllSequence.of_oddRec_evenRec
+IsEllSequence.rel₄
+IsEllSequence.sub_add_neg_sub_mul_eq_zero
+IsEllSequence.zero
+IsEllSequence.zero'
+Param
+Param.B
+Param.B.elim
+Param.B.sizeOf_spec
+Param.C
+Param.C.elim
+Param.C.sizeOf_spec
+Param.D
+Param.D.elim
+Param.D.sizeOf_spec
+Param.casesOn
+Param.ctorElim
+Param.ctorElimType
+Param.ctorIdx
+Param.noConfusion
+Param.noConfusionType
+Param.rec
+Param.recOn
+Param.toCtorIdx
+WeierstrassCurve.Affine.CoordinateRing.algebraMap_injective'
+WeierstrassCurve.Affine.CoordinateRing.algebraMap_poly_injective
+WeierstrassCurve.Affine.Point.some_eq_some_iff
+WeierstrassCurve.C_Ψ₃_eq
+WeierstrassCurve.Coeff
+WeierstrassCurve.Coeff.A₁
+WeierstrassCurve.Coeff.A₁.elim
+WeierstrassCurve.Coeff.A₁.sizeOf_spec
+WeierstrassCurve.Coeff.A₂
+WeierstrassCurve.Coeff.A₂.elim
+WeierstrassCurve.Coeff.A₂.sizeOf_spec
+WeierstrassCurve.Coeff.A₃
+WeierstrassCurve.Coeff.A₃.elim
+WeierstrassCurve.Coeff.A₃.sizeOf_spec
+WeierstrassCurve.Coeff.A₄
+WeierstrassCurve.Coeff.A₄.elim
+WeierstrassCurve.Coeff.A₄.sizeOf_spec
+WeierstrassCurve.Coeff.A₆
+WeierstrassCurve.Coeff.A₆.elim
+WeierstrassCurve.Coeff.A₆.sizeOf_spec
+WeierstrassCurve.Coeff.casesOn
+WeierstrassCurve.Coeff.ctorElim
+WeierstrassCurve.Coeff.ctorElimType
+WeierstrassCurve.Coeff.ctorIdx
+WeierstrassCurve.Coeff.noConfusion
+WeierstrassCurve.Coeff.noConfusionType
+WeierstrassCurve.Coeff.rec
+WeierstrassCurve.Coeff.recOn
+WeierstrassCurve.Coeff.toCtorIdx
+WeierstrassCurve.Jacobian.Point.fromAffine.congr_simp
+WeierstrassCurve.Universal.Affine.addX_smul_one_smul_one
+WeierstrassCurve.Universal.Affine.addY_smul_one_smul_one
+WeierstrassCurve.Universal.Affine.instAddGroupPointFieldToAffineBaseChangeMvPolynomialCoeffIntCurve
+WeierstrassCurve.Universal.Affine.nonsingular_smulX_smulY
+WeierstrassCurve.Universal.Affine.point
+WeierstrassCurve.Universal.Affine.slopeOne
+WeierstrassCurve.Universal.Affine.slopeOne_eq_neg_div
+WeierstrassCurve.Universal.Affine.smulX
+WeierstrassCurve.Universal.Affine.smulX_add
+WeierstrassCurve.Universal.Affine.smulX_eq
+WeierstrassCurve.Universal.Affine.smulX_eq_smulX_iff
+WeierstrassCurve.Universal.Affine.smulX_ne_smulX
+WeierstrassCurve.Universal.Affine.smulX_ne_zero
+WeierstrassCurve.Universal.Affine.smulX_neg
+WeierstrassCurve.Universal.Affine.smulX_one
+WeierstrassCurve.Universal.Affine.smulX_sub_smulX
+WeierstrassCurve.Universal.Affine.smulX_sub_sub_smulX_add
+WeierstrassCurve.Universal.Affine.smulX_two
+WeierstrassCurve.Universal.Affine.smulX_zero
+WeierstrassCurve.Universal.Affine.smulY
+WeierstrassCurve.Universal.Affine.smulY_add_sub_negY
+WeierstrassCurve.Universal.Affine.smulY_neg
+WeierstrassCurve.Universal.Affine.smulY_one
+WeierstrassCurve.Universal.Affine.smulY_one_ne_negY
+WeierstrassCurve.Universal.Affine.smulY_one_sub_negY
+WeierstrassCurve.Universal.Affine.smulY_sub_negY
+WeierstrassCurve.Universal.Affine.smulY_zero
+WeierstrassCurve.Universal.Affine.zsmul_point_eq_smulX_smulY
+WeierstrassCurve.Universal.Affine.zsmul_point_ne_zero
+WeierstrassCurve.Universal.Field
+WeierstrassCurve.Universal.Field.two_ne_zero
+WeierstrassCurve.Universal.Jacobian.addXYZ_smulField
+WeierstrassCurve.Universal.Jacobian.addXYZ_smulField₁
+WeierstrassCurve.Universal.Jacobian.addXYZ_smulRing
+WeierstrassCurve.Universal.Jacobian.addXYZ_smulRing₁
+WeierstrassCurve.Universal.Jacobian.addZ_smulPoly
+WeierstrassCurve.Universal.Jacobian.algebraMap_comp_smulRing
+WeierstrassCurve.Universal.Jacobian.dblXYZ_smulFieldIncrease in strong tech debt: (relative, absolute) = (3.75, 0.01)
| Current number | Change | Type (strong) |
|---|---|---|
| 506 | 4 | erw |
| 5682 | 1 | backward.isDefEq.respectTransparency |
Increase in weak tech debt: (relative, absolute) = (1.00, 0.25)
| Current number | Change | Type (weak) |
|---|---|---|
| 4984 | 3 | exposed public sections |
| 4 | 1 | large files |
Current commit f46c499f84
Reference commit caf2c7a120
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Five `ring` calls in EllipticDivisibilitySequence.lean closed their goals only via `ring`'s internal `ring_nf` fallback, emitting an info-level "Try this: ring_nf" suggestion each time. A plain `lake build` tolerates this, but mathlib CI runs `lake build --iofail`, which fails on any output. Call `ring_nf` directly so the goals close silently. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
| def preNormEDS' (b c d : R) : ℕ → R | ||
| | 0 => 0 | ||
| | 1 => 1 | ||
| | 2 => 1 | ||
| | 3 => c | ||
| | 4 => d | ||
| | (n + 5) => let m := n / 2 | ||
| | (n + 5) => letI m := n / 2 | ||
| have h4 : m + 4 < n + 5 := by change n / 2 + 4 < n + 5; omega | ||
| have h3 : m + 3 < n + 5 := by omega | ||
| have h2 : m + 2 < n + 5 := by omega | ||
| have h1 : m + 1 < n + 5 := by omega | ||
| if hn : Even n then | ||
| preNormEDS' (m + 4) * preNormEDS' (m + 2) ^ 3 * (if Even m then b else 1) - | ||
| preNormEDS' (m + 1) * preNormEDS' (m + 3) ^ 3 * (if Even m then 1 else b) | ||
| preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * | ||
| (if Even m then b else 1) - | ||
| preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * | ||
| (if Even m then 1 else b) | ||
| else | ||
| have : m + 5 < n + 5 := by | ||
| gcongr; exact Nat.div_lt_self (Nat.not_even_iff_odd.mp hn).pos one_lt_two | ||
| preNormEDS' (m + 2) ^ 2 * preNormEDS' (m + 3) * preNormEDS' (m + 5) - | ||
| preNormEDS' (m + 1) * preNormEDS' (m + 3) * preNormEDS' (m + 4) ^ 2 | ||
| have : 0 < n := by | ||
| rcases n with _ | n | ||
| · exact absurd ⟨0, rfl⟩ hn | ||
| · exact Nat.succ_pos n | ||
| change n / 2 + 5 < n + 5; omega | ||
| preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * | ||
| preNormEDS' b c d (m + 5) - | ||
| preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * | ||
| preNormEDS' b c d (m + 4) ^ 2 |
There was a problem hiding this comment.
Not sure why Claude made this much longer; this is already in mathlib and need not be changed.
3 participants
WIP / draft. This Claude-generated PR bumps #13782 (by @alreadydone) to current mathlib.
The formula$[n]P = (\phi_n(x,y) : \omega_n(x,y) : \psi_n(x,y))$ in Jacobian coordinates for $P = (x,y)$ a nonsingular point on a Weierstrass curve, as
WeierstrassCurve.zsmul_eq_smulEval.Co-authored-by: Junyan Xu junyanxumath@gmail.com
Co-authored-by: David Kurniadi Angdinata dka31@cantab.ac.uk