Coordinates of scalar multiplication through the division polynomials

The Nagell–Lutz route expresses n • (X, Y) on the universal curve through the division polynomials: the affine X-coordinate is φₙ/ψₙ² and the Y-coordinate is ωₙ/ψₙ³, as elements of Universal.Field. This file defines those two rational functions, smulX and smulY, develops the smulX calculus — values at 0, 1 and 2, the offset ψₙ₊₁ψₙ₋₁/ψₙ² from the X-coordinate, evenness in n, nonvanishing, the difference smulX m - smulX n as a single quotient, and the separation statement smulX m = smulX n ↔ m = n ∨ m = -n — and then proves the identification itself: zsmul_point_eq_smulX_smulY says that (smulX n, smulY n) really are the affine coordinates of n • (X, Y), for every n ≠ 0. smulY's own sign rule is here too: negating a nonzero index negates the point, so smulY (-n) is the negY of (smulX n, smulY n).

The middle of the file turns that calculus on the pair (smulX 1, smulY 1), which is the distinguished point (X, Y) itself. For n ≠ 0 the vertical gap smulY n - negY (smulX n) (smulY n) is ψ₂ₙ/ψₙ⁴, hence nonzero, so smulY n never equals the negY of its own pair. The quotient formula genuinely needs n ≠ 0, since ψ₀ = 0 leaves it meaningless; smulY_ne_negY carries the same hypothesis because it is derived from that formula, not because it fails at n = 0 — there it reads 0 ≠ -a₃, which holds. At n = 1 the gap is ψ₂, which selects the tangent branch of Mathlib's Affine.slope and gives the tangent slope slopeOne the closed form -Wₓ/ψ₂. Feeding that slope to Mathlib's affine addition formula sends (smulX 1, smulY 1) to (smulX 2, smulY 2): addX … = smulX 2 and addY … = smulY 2. Those two are the n = 2 base case of the induction; smulX_add and smulY_add_sub_negY, the chord formulas relating the values at n + m, n - m, n and m, are its step.

With the identification in hand the geometric consequences are immediate: the distinguished point is not torsion (zsmul_point_ne_zero), and n ↦ n • point is injective (Jacobian.zsmul_point_injective). Next comes the Jacobian form of the identification, where the three division polynomials appear as honest homogeneous coordinates (φₙ : ωₙ : ψₙ) and the statement needs no hypothesis on n at all: at n = 0 the triple is the point at infinity.

That Jacobian form is what lets Mathlib's doubling and addition formulas be run on the triple directly. dblXYZ_smulField and addXYZ_smulField say that dblXYZ and addXYZ carry (φₙ : ωₙ : ψₙ) to (φ₂ₙ : ω₂ₙ : ψ₂ₙ) and (φₘ : ωₘ : ψₘ), (φₙ : ωₙ : ψₙ) to (φₙ₊ₘ : ωₙ₊ₘ : ψₙ₊ₘ) scaled by ψₙ₋ₘ — as equalities of triples, not merely of the points they represent, which is what makes them usable as rewrite rules. Both descend to Universal.Ring, where they are identities between polynomials modulo the Weierstrass polynomial.

The file closes by specializing. A point (x, y) on a curve W over any commutative ring induces Universal.ringEval, and ringEval_comp_smulRing says it carries the universal triple to smulEval W x y n, the division polynomials of W evaluated at (x, y). The three identities above therefore hold for W at (x, y), and feeding them to an even-odd induction proves zsmul_point_eq_smulEval: over a field, n • (x, y) has Jacobian coordinates (φₙ(x,y) : ωₙ(x,y) : ψₙ(x,y)), for every n and with no hypothesis on the characteristic. That is the statement the Nagell–Lutz layer consumes.

Main definitions

• WeierstrassCurve.Universal.Affine.smulX: the rational function φₙ/ψₙ².
• WeierstrassCurve.Universal.Affine.smulY: the rational function ωₙ/ψₙ³.
• WeierstrassCurve.Universal.Affine.slopeOne: the slope of the tangent at (X, Y).
• WeierstrassCurve.Universal.Jacobian.smulPoly, .smulRing, .smulField: the triple (φₙ, ωₙ, ψₙ) as a Fin 3 → _, over the polynomial ring, the universal ring and the universal field respectively.
• WeierstrassCurve.smulEval: the same triple for a concrete curve W, evaluated at a point (x, y) of the affine plane over any commutative ring.

Main results

• WeierstrassCurve.Universal.Affine.smulX_eq: smulX n = smulX 1 - ψₙ₊₁ψₙ₋₁/ψₙ² for n ≠ 0, the offset from the X-coordinate that smulX_two and smulX_sub_smulX both run through.
• WeierstrassCurve.Universal.Affine.smulX_sub_smulX: smulX m - smulX n as a single quotient, by the elliptic-sequence relation of the universal ψ family.
• WeierstrassCurve.Universal.Affine.smulX_ne_zero: smulX n ≠ 0 for n ≠ 0.
• WeierstrassCurve.Universal.Affine.smulX_eq_smulX_iff: smulX m = smulX n ↔ m = n ∨ m = -n, the field-level form of the fact that x-coordinates separate multiples up to sign.
• WeierstrassCurve.Universal.Affine.smulY_neg: for n ≠ 0, smulY (-n) is the negY of the coordinates at n — the long-Weierstrass correction that ω_neg carries, in the universal field.
• WeierstrassCurve.Universal.Affine.smulY_sub_negY: the gap smulY n - negY (smulX n) (smulY n) is ψ₂ₙ/ψₙ⁴, whence smulY_ne_negY — the gap never vanishes for n ≠ 0.
• WeierstrassCurve.Universal.Affine.slopeOne_eq_neg_div: the tangent slope at (X, Y) is -Wₓ/ψ₂, the ratio of the two partial derivatives of the Weierstrass polynomial.
• WeierstrassCurve.Universal.Affine.addX_smul_one_smul_one, .addY_smul_one_smul_one: doubling (X, Y) along that tangent with Mathlib's affine addition formula returns (smulX 2, smulY 2) — the base case of the scalar-multiplication induction.
• WeierstrassCurve.Universal.Affine.smulX_add, .smulY_add_sub_negY: the chord formulas, giving smulX (n + m) and the vertical gap at n + m in terms of the values at n, m and n - m — the induction step.
• WeierstrassCurve.Universal.Affine.zsmul_point_eq_smulX_smulY: the identification. For n ≠ 0 the pair (smulX n, smulY n) is nonsingular and n • (X, Y) is the affine point it names.
• WeierstrassCurve.Universal.Affine.zsmul_point_ne_zero and WeierstrassCurve.Universal.Jacobian.zsmul_point_ne_zero: the distinguished point is not torsion, in affine and in Jacobian coordinates; whence Jacobian.zsmul_point_injective, that n ↦ n • point is injective.
• WeierstrassCurve.Universal.Jacobian.zsmul_point_eq_smulField: the Jacobian identification, (n • point).point = ⟦(φₙ : ωₙ : ψₙ)⟧, with no hypothesis on n.
• WeierstrassCurve.Universal.Jacobian.dblXYZ_smulField, .addXYZ_smulField: Mathlib's Jacobian doubling and addition formulas evaluated on the universal triples, as equalities of triples. .dblXYZ_smulRing and .addXYZ_smulRing are the same over Universal.Ring.
• WeierstrassCurve.Universal.Jacobian.dblZ_smulPoly, .addZ_smulPoly: the Z-coordinates of those two formulas, ψ₂ₙ and ψₙ₊ₘψₙ₋ₘ, already in the polynomial ring — no reduction modulo the Weierstrass polynomial is needed for the third coordinate.
• WeierstrassCurve.Universal.Jacobian.smulPoly_neg, .smulRing_neg, .smulField_neg: negating the index is Mathlib's Jacobian negation rescaled by -1.
• WeierstrassCurve.Universal.ringEval_comp_smulRing: smulEval is the specialization of smulRing along the homomorphism a point of W induces — the bridge from the universal identities to a concrete curve, and what dblXYZ_smulEval and addXYZ_smulEval are proved through.
• WeierstrassCurve.zsmul_point_eq_smulEval: the headline. Over a field, n • (x, y) in Jacobian coordinates is (φₙ(x,y) : ωₙ(x,y) : ψₙ(x,y)), for every nonsingular (x, y) and every n.
• WeierstrassCurve.zsmul_eq_zero_of_evalEval_ψ_eq_zero: the converse — a vanishing ψₙ at a nonsingular point forces n • P = 0. Unrestricted in n, and so an annihilation statement rather than a torsion one: at n = 0 both sides hold of every point.
• WeierstrassCurve.addOrderOf_eq_two_iff_evalEval_ψ₂_eq_zero: those two directions packaged as the characterisation of two-torsion, addOrderOf P = 2 ↔ ψ₂(x, y) = 0. Its contrapositive is what discharges the addOrderOf ≠ 2 guard the Nagell–Lutz theorems carry.

Provenance

Ported from J. Xu and D. K. Angdinata's projects/NagellLutz/LutzNagell/ZSMul.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, main @ 1c1c74664e40071c2c2165bc55ca2616a67ccd6b): smulX (:164), smulY (:168), the value lemmas (:171–:174), smulX_eq (:176), smulX_two (:183), smulX_sub_smulX (:186), smulX_neg (:201), smulX_ne_zero (:203), smulX_ne_smulX (:206), smulX_eq_smulX_iff (:217), and smulY_neg (:290), pulled forward from the slope slice's range so that smulY does not ship without its negative-index rule. The source's ψᵤ abbreviation is dropped in favour of polyToField (curve.ψ n), the DivisionPolynomial/Universal.lean convention.

Five departures beyond that respelling. The elliptic-sequence step of smulX_sub_smulX is respelt through IsEllipticNet.rel and linear_combination (the source converts against its isEllSequence_ψᵤ, a statement shape Mathlib has since replaced). The equation lemmas smulX_def and smulY_def are added for consumers in other modules, as in Omega.lean. smulY_neg reads its coordinate identity off Mathlib's Jacobian.negY_of_Z_ne_zero at (φₙ : ωₙ : ψₙ) instead of the source's private field-level auxiliary (:286), still naming its ring hom (map_neg polyToField) where the source unfolds ψᵤ, because an unnamed map_neg does not fire on a polyToField application in this direction. smulX_eq meets that same direction problem — the source's forward simp only [φ, ψᵤ, map_sub, map_mul, map_pow, ← add_div] does not fire here — so it instead maps a polynomial-level identity with congrArg polyToField and clears the denominator with field_simp and linear_combination. Finally @[simp] is added to smulX_neg, smulY_neg, smulX_ne_zero and smulX_eq_smulX_iff; the source tags only the four value lemmas.

The tangent-and-doubling block below adds, at the same revision, smulY_sub_negY (:227), slopeOne (:241), slopeOne_eq_neg_div (:244), addX_smul_one_smul_one (:261) and addY_smul_one_smul_one (:277), with the same ψᵤ respelling and one added equation lemma, slopeOne_def.

One statement is generalised rather than transcribed, and the source's two n = 1 wrappers go with it. The source proves only smulY_one_ne_negY (:237); here smulY_ne_negY states it for every n ≠ 0, which smulY_sub_negY already gives — the gap ψ₂ₙ/ψₙ⁴ is a quotient of nonzero elements. Given the general form, both of the source's specialisations are dropped rather than ported: smulY_one_ne_negY (:237) is smulY_ne_negY one_ne_zero and is written that way at its two call sites, and smulY_one_sub_negY (:233) is smulY_sub_negY one_ne_zero followed by the collapse of ψ₂ₙ to ψ₂ and ψₙ⁴ to 1, which its one consumer slopeOne_eq_neg_div carries as a local have.

None of the source's four private field-level auxiliaries in that range is ported, because none of them has a consumer left here.

• smulY_sub_negY_aux (:222) is not needed: smulY_sub_negY runs through this file's own smulY_neg — negating the index negates the point — which already reads its coordinate identity off Mathlib's Jacobian.negY_of_Z_ne_zero. What is left is ω_neg, ω_spec and ψ_mul_ψc, with no field-level algebra to package.
• addX_smul_one_smul_one_aux (:252) has no call site in the source either: at 1c1c7466 the name occurs exactly once repo-wide per copy, its own definition.
• addX_smul_ring_identity (:257) and addY_smul_one_smul_one_aux (:271) each package the residue of one field_simp in the source's normal form. Both residues differ here, and linear_combination against the mapped certificate, respectively ring, closes each in a line.

Two further departures. Mathlib's Affine.slope is defined by cases, and the source supplies the decidability it needs with a namespace-wide attribute [local instance] Classical.propDecidable (:159, and again at :406). Nothing of the kind is needed here: Mathlib carries FractionRing.instDecidableEq, so DecidableEq Universal.Field synthesizes outright — checked with #synth, which returns that instance — and every declaration in this file mentioning slope or the Jacobian group law elaborates without any Classical. And the map-direction problem recorded above for smulX_eq recurs at every proof in the block. Measured against the unusedSimpArgs linter at this pin: bare map_sub and map_neg fire at no site, while bare map_mul, map_add, map_pow and map_ofNat fire at all of them — the unexposed instances are Sub and Neg. Each map_* names its hom regardless, for uniformity with the rest of the file. Naming alone is not enough in the last three proofs, which state their polynomial-level certificate as a have and map it with congrArg polyToField, the shape smulX_eq uses: polyToField_apply is @[simp] here, so field_simp shatters polyToField (C X) into algebraMap _ _ (AdjoinRoot.of _ X) while leaving polyToField curve.polynomialX folded, and the two sides of the goal then share no atoms.

The identification block below adds, at the same revision, smulX_add (:300), smulY_add_sub_negY (:324), eq_of_sub_negY_eq (:345), zsmul_point_eq_smulX_smulY (:353), Affine.zsmul_point_ne_zero (:398), Jacobian.zsmul_point_ne_zero (:411), Jacobian.zsmul_point_injective (:416), smulPoly, smulRing and smulField (:423–:427), algebraMap_comp_smulRing (:429) and Jacobian.zsmul_point_eq_smulField (:433). The first three come from before the previous slice's range: they are the chord formulas, and the headline induction step cannot be stated without them. The source's curveField has no counterpart here and is spelled pointedCurve.toAffine.

One prerequisite is strengthened rather than transcribed, in DivisionPolynomial/Universal.lean: what was isEllipticSequence_polyToField_ψ is now isEllipticNet_polyToField_ψ, the source's net_ψᵤ (:140) rather than its isEllSequence_ψᵤ (:139). smulY_add_sub_negY needs the elliptic-net relation at the nonzero shift s = m, which an elliptic sequence — the s = 0 case — does not give; isEllipticNet_normEDS was already available, so the change is two tokens, and smulX_sub_smulX, the one existing call site, takes the s = 0 instance.

eq_of_sub_negY_eq is the first consumer of (2 : Universal.Field) ≠ 0. No instance is added for it: Mathlib's charZero for a fraction ring carries CharZero Universal.Field from CharZero Universal.Ring, and EllipticCurve/Universal.lean imports Algebra/CharP/Algebra.lean so that it is in scope.

One statement is restated. The source's zsmul_point_ne (:416) is the pairwise form m ≠ n → m • point ≠ n • point; here it is zsmul_point_injective, the equivalent Function.Injective fun n : ℤ ↦ n • Jacobian.point, which says the same thing in the idiom the rest of the library uses and composes with the Function.Injective API.

Five departures inside the block itself. The source's some_eq_some_iff (used at :372) is not added: Mathlib's spelling is the auto-generated Affine.Point.some.injEq, which Mathlib itself uses, and EllipticCurve/Universal.lean records that this repository declines Iff wrappers around auto-generated injEqs. The source's two erws (:363, :372) are both gone: the first only bridged ((0 + 1 + 1 : ℕ) : ℤ) to (2 : ℤ), which an explicit cast rewrite does, and the second additionally saw through Affine.Point.neg_some, which is a named rfl lemma and can simply be cited. The n = 1 instance of the induction hypothesis is obtained at an ascribed type so that its index cast is normalised before the pair is destructured: afterwards the nonsingularity witness mentions the cast, and no rewrite of the equation alone is type-correct. And the two chord formulas are stated without the source's cosmetic let ψ₂ x y := y - negY x y binder, which the source immediately removes again with change. And of the block's two candidate @[simp] lemmas only algebraMap_comp_smulRing carries the tag. zsmul_point_eq_smulField cannot: Jacobian.point_def and Affine.point_def are both @[simp], so simpNF reports the left-hand side (n • Jacobian.point).point as not in normal form — it reduces to (Point.fromAffine (Affine.Point.mk ⋯)).point before the lemma could fire. It was tagged and rejected by a full lint-env run before being left untagged.

Three declarations of the source's are not ported. Its smulX_add_aux (:295) and smulY_add_sub_negY_aux (:317) each package the residue of one field_simp; both residues differ here and are closed in place. Its net_add_sub_iff, which lives in LutzNagell/EllipticDivisibilitySequence.lean rather than in this file, is inlined as the local key of smulY_add_sub_negY — normalising the eight index sums of IsEllipticNet.rel needs linear_combination (norm := ring_nf), since ring1 does not reduce inside curve.ψ's argument. The source's instance : AddGroup ((curve.baseChange Universal.Field).toAffine.Point) (:341) is an inferInstance cache and is not needed, and neither is its second attribute [local instance] Classical.propDecidable (:406), for the reason already given.

The final block below completes the port of the source file, adding, at the same revision, dblZ_smulPoly (:446), nonsingular_smulField (:454), dblXYZ_smulField (:469), dblXYZ_smulRing (:480), addZ_smulPoly (:484), smulPoly_neg (:496), smulRing_neg (:499), smulField_neg (:502), smulPoly_zero and smulField_zero (:505–:506), addXYZ_smulField (:508), addXYZ_smulRing (:533), then smulEval (:560), ringEval_comp_smulRing (:566), dblXYZ_smulEval (:577), addXYZ_smulEval (:581) and zsmul_eq_smulEval (:599), the last ported under the name zsmul_point_eq_smulEval because its conclusion is about the .point projection. The three ₁-suffixed adjacent-index lemmas (:539, :546, :589) are in the source's range but are not ported, for the reason given below. The two zero lemmas are moved ahead of dblXYZ_smulField, which uses smulField_zero to identify the n = 0 triple; the source proves that case by unfolding dblXYZ instead. ringEval_comp_smulRing is placed in the Universal namespace rather than at WeierstrassCurve level as upstream, matching where EllipticCurve/Universal.lean keeps the rest of the ringEval API. The source's curveRing_map_ringEval is this repository's map_ringEval. The source's ringEval_ψ (:572) is not ported: it is the third coordinate of ringEval_comp_smulRing, used once, so it lives as a typed local have in addXYZ_smulEval rather than as public API. The source's ω_neg_eq_neg_negY (:489) is not ported: it is ω_neg followed by negY_eq and ring, and smulPoly_neg — its only advertised consumer — discharges the middle coordinate through the default simp set instead, so the intermediate lemma has no caller.

None of the source's three ₁-suffixed adjacent-index lemmas is ported (:539, :546, :589). Each is its addXYZ_smul{Field,Ring,Eval} parent followed by add_sub_cancel_left, ψ_one, map_one/evalEval_one and one_smul — the scaling factor at adjacent indices is ψ of a gap of 1. Only the Eval form ever had a consumer, and only one, so those four rewrites are appended to that call site's own rw chain instead; the intermediate specialisations earn nothing.

point_point (:420) is not ported at all, and the previous slice's copy of it is deleted here. That slice predicted this block would supply a consumer; it does not. At 1c1c7466 the source's point_point occurs exactly once per copy — its own definition — so nothing consumes it upstream either, and it restates Jacobian.point_def, Affine.point_def and Point.fromAffine_some without adding content. algebraMap_comp_smulRing (:429), predicted alongside it, is consumed — cited four times across dblXYZ_smulRing, addXYZ_smulRing and smulField_neg. It is load-bearing rather than decorative: upstream algebraMap _ _ ∘ smulRing n = smulField n holds by rfl, and here it does not, polyToField's body being unexposed.

One prerequisite is added, in EllipticCurve/Universal.lean: map_polyToField, for the same reason. Upstream curveField = curvePoly.map polyToField definitionally, so a curve-dependent transport such as map_dblZ lands on curveField with no further step; here it lands on curvePoly.map polyToField and the identification has to be cited. Both proofs that cite it do so after map_dblZ. map_addZ is not in that class: addZ takes no curve argument, so its transport never mentions a mapped curve. map_polyToField carries @[simp], as does ringEval_comp_smulRing: both are map-specialization normal forms, reducing a mapped universal object to the concrete one it names, and neither loops. api-design asked for both tags in round three, over an initial judgement here that two explicit call sites did not warrant the global surface; the normal-form reading is the better one, and a full lint-env confirms neither tag introduces a simpNF violation.

Two of the source's proofs are replaced rather than transcribed, both because a tactic upstream relies on is unavailable over Poly = ℤ[A₁,⋯,A₆][X][Y]. Instance search gives up on that triple-nested polynomial ring — IsRightCancelAdd Poly and HasDistribNeg Poly both fail to synthesize in this import closure, while their two-level analogues succeed and raising synthInstance.maxSize does not help. So addZ_smulPoly discharges its elliptic-sequence certificate through sub_eq_zero and ring where the source uses convert, and smulPoly_neg is proved coordinatewise with ring where the source uses a single simp carrying Odd.neg_pow. ring itself works over Poly; it is the additive-cancellation and sign lemmas that are out of reach.

ringEval_comp_smulRing is also proved differently. The source threads a nine-lemma conv_rhs chain that ends by unfolding polyEval; that definition's body is unexposed here. The proof instead runs coordinatewise through ringEval_mk and evalEval_φ/evalEval_ω/evalEval_ψ, which DivisionPolynomial/Universal.lean already carries — the source's own :99–:106, ported in an earlier slice and, before this proof, cited nowhere outside their own file.

Finally the source's two private helpers in this range, two_zsmul_point_eq_dblXYZ (:458) and add_point_of_ne_eq_addXYZ (:463), are not ported as declarations. Each has exactly one call site and one instantiation, so each is inlined as a typed local have — h2 in dblXYZ_smulField and hadd in addXYZ_smulField — which keeps both proofs inside the length cap. The source's zsmul_point_ne, which add_point_of_ne_eq_addXYZ consumes, is this file's zsmul_point_injective, so the distinctness side condition is discharged through injectivity.

noncomputable def WeierstrassCurve.Universal.Affine.smulX (n : ℤ) : Universal.Field

The rational function φₙ/ψₙ² in the universal field. For n ≠ 0 it is the affine X-coordinate of n • (X, Y) on the universal curve, by zsmul_point_eq_smulX_smulY below.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WeierstrassCurve.Universal.Affine.smulY (n : ℤ) : Universal.Field

The rational function ωₙ/ψₙ³ in the universal field. For n ≠ 0 it is the affine Y-coordinate of n • (X, Y) on the universal curve, by zsmul_point_eq_smulX_smulY below.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Universal.Affine.smulX_def (n : ℤ) : smulX n = polyToField (WeierstrassCurve.φ curve n) / polyToField (WeierstrassCurve.ψ curve n) ^ 2

The defining formula for smulX. The definition body is not exposed, so this equation lemma is how a consumer in another module computes with it.

theorem WeierstrassCurve.Universal.Affine.smulY_def (n : ℤ) : smulY n = polyToField (WeierstrassCurve.ω curve n) / polyToField (WeierstrassCurve.ψ curve n) ^ 3

The defining formula for smulY. The definition body is not exposed, so this equation lemma is how a consumer in another module computes with it.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulX_zero : smulX 0 = 0

smulX at 0 is 0.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulY_zero : smulY 0 = 0

smulY at 0 is 0.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulX_one : smulX 1 = polyToField (Polynomial.C Polynomial.X)

smulX at 1 is the X-coordinate itself.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulY_one : smulY 1 = polyToField Polynomial.X

smulY at 1 is the Y-coordinate itself.

theorem WeierstrassCurve.Universal.Affine.smulX_eq {n : ℤ} (hn : n ≠ 0) : smulX n = smulX 1 - polyToField (WeierstrassCurve.ψ curve (n + 1)) * polyToField (WeierstrassCurve.ψ curve (n - 1)) / polyToField (WeierstrassCurve.ψ curve n) ^ 2

smulX n differs from the X-coordinate by ψₙ₊₁ψₙ₋₁/ψₙ².

theorem WeierstrassCurve.Universal.Affine.smulX_two : smulX 2 = smulX 1 - polyToField (WeierstrassCurve.ψ curve 3) / polyToField (WeierstrassCurve.ψ curve 2) ^ 2

smulX at 2, in terms of the X-coordinate and ψ₃/ψ₂².

theorem WeierstrassCurve.Universal.Affine.smulX_sub_smulX {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) : smulX m - smulX n = polyToField (WeierstrassCurve.ψ curve (n + m)) * polyToField (WeierstrassCurve.ψ curve (n - m)) / (polyToField (WeierstrassCurve.ψ curve n) * polyToField (WeierstrassCurve.ψ curve m)) ^ 2

The difference of two values of smulX as a single quotient: the numerator is ψₙ₊ₘψₙ₋ₘ, by the elliptic-sequence relation of the universal ψ family.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulX_neg {n : ℤ} : smulX (-n) = smulX n

smulX is even in n.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulY_neg {n : ℤ} (h0 : n ≠ 0) : smulY (-n) = pointedCurve.toAffine.negY (smulX n) (smulY n)

Negating a nonzero index negates the point: smulY (-n) is the long-Weierstrass negY of the coordinates (smulX n, smulY n).

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulX_ne_zero {n : ℤ} (h0 : n ≠ 0) : smulX n ≠ 0

smulX n is nonzero for n ≠ 0.

theorem WeierstrassCurve.Universal.Affine.smulX_ne_smulX {m n : ℤ} (ne : m ≠ n) (ne_neg : m ≠ -n) : smulX m ≠ smulX n

smulX separates indices that agree in neither order nor sign.

@[simp]

theorem WeierstrassCurve.Universal.Affine.smulX_eq_smulX_iff {m n : ℤ} : smulX m = smulX n ↔ m = n ∨ m = -n

Two values of smulX agree exactly when the indices agree up to sign.

theorem WeierstrassCurve.Universal.Affine.smulY_sub_negY {n : ℤ} (h0 : n ≠ 0) : smulY n - pointedCurve.toAffine.negY (smulX n) (smulY n) = polyToField (WeierstrassCurve.ψ curve (2 * n)) / polyToField (WeierstrassCurve.ψ curve n) ^ 4

The gap between smulY n and the negY of its own pair is ψ₂ₙ/ψₙ⁴. Being a quotient of nonzero ψ's it never vanishes, which is what puts the pair (smulX n, smulY n) in the tangent branch of Affine.slope.

theorem WeierstrassCurve.Universal.Affine.smulY_ne_negY {n : ℤ} (h0 : n ≠ 0) : smulY n ≠ pointedCurve.toAffine.negY (smulX n) (smulY n)

smulY n never equals the negY of its own pair, for n ≠ 0. The gap computed above is ψ₂ₙ/ψₙ⁴, a quotient of nonzero elements.

noncomputable def WeierstrassCurve.Universal.Affine.slopeOne : Universal.Field

The slope of the tangent line to pointedCurve at its distinguished point (X, Y): Mathlib's Affine.slope at the coincident pair (X, Y), (X, Y).

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Universal.Affine.slopeOne_def : slopeOne = pointedCurve.toAffine.slope (smulX 1) (smulX 1) (smulY 1) (smulY 1)

The defining formula for slopeOne. The definition body is not exposed, so this equation lemma is how a consumer in another module computes with it.

theorem WeierstrassCurve.Universal.Affine.slopeOne_eq_neg_div : slopeOne = -polyToField curve.polynomialX / polyToField (WeierstrassCurve.ψ curve 2)

The tangent slope in closed form: -Wₓ/ψ₂, the ratio of the two partial derivatives of the Weierstrass polynomial at (X, Y).

theorem WeierstrassCurve.Universal.Affine.addX_smul_one_smul_one : pointedCurve.toAffine.addX (smulX 1) (smulX 1) slopeOne = smulX 2

Mathlib's addX at (smulX 1, smulX 1) along the tangent slope is smulX 2. The affine addition formula run on the distinguished point against itself lands on the value at 2.

theorem WeierstrassCurve.Universal.Affine.addY_smul_one_smul_one : pointedCurve.toAffine.addY (smulX 1) (smulX 1) (smulY 1) slopeOne = smulY 2

The same for addY: it returns smulY 2. Together with the previous lemma this is the n = 2 base case of zsmul_point_eq_smulX_smulY below, which is what makes (smulX 2, smulY 2) the coordinates of 2 • (X, Y).

theorem WeierstrassCurve.Universal.Affine.smulX_sub_sub_smulX_add {m n : ℤ} (add_ne : n + m ≠ 0) (sub_ne : n - m ≠ 0) : smulX (n - m) - smulX (n + m) = polyToField (WeierstrassCurve.ψ curve (2 * n)) * polyToField (WeierstrassCurve.ψ curve (2 * m)) / (polyToField (WeierstrassCurve.ψ curve (n + m)) * polyToField (WeierstrassCurve.ψ curve (n - m))) ^ 2

The difference smulX (n - m) - smulX (n + m) as a single quotient, with numerator ψ₂ₙψ₂ₘ: this is smulX_sub_smulX at the pair (n - m, n + m), whose index sum and difference collapse to 2n and 2m.

theorem WeierstrassCurve.Universal.Affine.smulX_add {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) (add_ne : n + m ≠ 0) (sub_ne : n - m ≠ 0) : smulX (n + m) = smulX (n - m) - (smulY n - pointedCurve.toAffine.negY (smulX n) (smulY n)) * (smulY m - pointedCurve.toAffine.negY (smulX m) (smulY m)) / (smulX m - smulX n) ^ 2

The addition formula for the X-coordinate. smulX (n + m) is smulX (n - m) less the product of the two vertical gaps, divided by the square of the horizontal one — the classical chord construction, written in the smulX/smulY calculus.

theorem WeierstrassCurve.Universal.Affine.smulY_add_sub_negY {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) (add_ne : n + m ≠ 0) (sub_ne : n - m ≠ 0) : smulY (n + m) - pointedCurve.toAffine.negY (smulX (n + m)) (smulY (n + m)) = ((smulY m - pointedCurve.toAffine.negY (smulX m) (smulY m)) * (smulX n - smulX (n + m)) - (smulY n - pointedCurve.toAffine.negY (smulX n) (smulY n)) * (smulX m - smulX (n + m))) / (smulX m - smulX n)

The addition formula for the vertical gap. The gap at n + m is a difference of the gaps at m and at n, each weighted by a horizontal distance, over the horizontal distance between n and m.

theorem WeierstrassCurve.Universal.Affine.zsmul_point_eq_smulX_smulY {n : ℤ} : n ≠ 0 → ∃ (h : pointedCurve.toAffine.Nonsingular (smulX n) (smulY n)), n • point = Affine.Point.some (smulX n) (smulY n) h

The affine coordinates of n • (X, Y) are (smulX n, smulY n). This is the theorem the whole smulX/smulY calculus above was built for: the rational functions φₙ/ψₙ² and ωₙ/ψₙ³ really are the coordinates of the n-fold multiple of the distinguished point on the universal curve, for every nonzero n.

theorem WeierstrassCurve.Universal.Affine.zsmul_point_ne_zero {n : ℤ} (h0 : n ≠ 0) : n • point ≠ 0

The distinguished point (X, Y) on the universal curve is not torsion. Every nonzero multiple of it has affine coordinates, so none of them is the point at infinity.

theorem WeierstrassCurve.Universal.Jacobian.zsmul_point_ne_zero {n : ℤ} (h0 : n ≠ 0) : n • point ≠ 0

No nonzero multiple of the distinguished point vanishes in Jacobian coordinates. This is Affine.zsmul_point_ne_zero moved along Point.toAffineAddEquiv, which is exactly how Jacobian.point is defined from Affine.point.

theorem WeierstrassCurve.Universal.Jacobian.zsmul_point_injective : Function.Injective fun (n : ℤ) => n • point

The multiples of the distinguished point are pairwise distinct: n ↦ n • point is injective. Distinct integers therefore give distinct points, so the subgroup generated by the distinguished point is a free abelian group of rank one — the point has infinite order.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.Jacobian.smulPoly (n : ℤ) : Fin 3 → Poly

The three families of universal division polynomials as a 3-tuple.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.Jacobian.smulRing (n : ℤ) : Fin 3 → Universal.Ring

The three families of division polynomials as elements of the universal ring.

Equations

• WeierstrassCurve.Universal.Jacobian.smulRing n = ⇑(AdjoinRoot.mk WeierstrassCurve.Universal.curve.polynomial) ∘ WeierstrassCurve.Universal.Jacobian.smulPoly n

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.Jacobian.smulField (n : ℤ) : Fin 3 → Universal.Field

The three families of division polynomials as elements of the universal field.

Equations

• WeierstrassCurve.Universal.Jacobian.smulField n = ⇑WeierstrassCurve.Universal.polyToField ∘ WeierstrassCurve.Universal.Jacobian.smulPoly n

theorem WeierstrassCurve.Universal.Jacobian.smulField_Z (n : ℤ) : smulField n 2 = polyToField (WeierstrassCurve.ψ curve n)

The Z coordinate of smulField n is ψₙ. The third component of the universal-field triple is the division polynomial itself, carried across by polyToField, with no denominator.

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.algebraMap_comp_smulRing (n : ℤ) : ⇑(algebraMap Universal.Ring Universal.Field) ∘ smulRing n = smulField n

smulField is smulRing pushed into the field of fractions, coordinate by coordinate.

theorem WeierstrassCurve.Universal.Jacobian.zsmul_point_eq_smulField {n : ℤ} : (n • point).point = ⟦smulField n⟧

The Jacobian coordinates of n • (X, Y) are (φₙ : ωₙ : ψₙ). The Jacobian form of Affine.zsmul_point_eq_smulX_smulY: where the affine statement divides by ψₙ² and ψₙ³, the Jacobian one carries ψₙ as the third coordinate and holds for n = 0 as well, the triple becoming (1 : 1 : 0), the point at infinity.

For n ≠ 0 the two triples differ by the scalar ψₙ⁻¹, which is what Quotient.sound needs: Jacobian coordinates scale as (u²x, u³y, uz), and those are precisely the powers by which smulX and smulY divide.

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.smulPoly_zero : smulPoly 0 = ![1, 1, 0]

smulPoly at 0 is the triple (1, 1, 0).

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.smulRing_zero : smulRing 0 = ![1, 1, 0]

smulRing at 0 is the triple (1, 1, 0), the universal-ring representation of the point at infinity.

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.smulField_zero : smulField 0 = ![1, 1, 0]

smulField at 0 is the triple (1 : 1 : 0), the point at infinity.

theorem WeierstrassCurve.Universal.Jacobian.dblZ_smulPoly {n : ℤ} : Jacobian.dblZ curvePoly (smulPoly n) = WeierstrassCurve.ψ curve (2 * n)

The Z-coordinate of Mathlib's Jacobian doubling formula at (φₙ, ωₙ, ψₙ) is ψ₂ₙ — already in the polynomial ring, with no reduction modulo the Weierstrass polynomial.

theorem WeierstrassCurve.Universal.Jacobian.nonsingular_smulField {n : ℤ} : Jacobian.Nonsingular pointedCurve (smulField n)

The triple (φₙ : ωₙ : ψₙ) is a nonsingular Jacobian point representative of the universal curve, for every n — it represents n • (X, Y), which is a point of the curve.

theorem WeierstrassCurve.Universal.Jacobian.dblXYZ_smulField {n : ℤ} : Jacobian.dblXYZ pointedCurve (smulField n) = smulField (2 * n)

Mathlib's Jacobian doubling formula sends (φₙ : ωₙ : ψₙ) to (φ₂ₙ : ω₂ₙ : ψ₂ₙ), as an equality of triples and not merely of the points they represent.

theorem WeierstrassCurve.Universal.Jacobian.dblXYZ_smulRing {n : ℤ} : Jacobian.dblXYZ curveRing (smulRing n) = smulRing (2 * n)

The doubling identity over the universal ring, where it is a statement about polynomials modulo the Weierstrass polynomial rather than about rational functions.

theorem WeierstrassCurve.Universal.Jacobian.addZ_smulPoly {m n : ℤ} : Jacobian.addZ (smulPoly m) (smulPoly n) = WeierstrassCurve.ψ curve (n + m) * WeierstrassCurve.ψ curve (n - m)

The Z-coordinate of Mathlib's Jacobian addition formula at (φₘ, ωₘ, ψₘ) and (φₙ, ωₙ, ψₙ) is ψₙ₊ₘψₙ₋ₘ, again already in the polynomial ring.

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.smulPoly_neg {n : ℤ} : smulPoly (-n) = -1 • Jacobian.neg curvePoly (smulPoly n)

Negating the index negates the point: the triple at -n is Mathlib's Jacobian negation of the triple at n, rescaled by -1.

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.smulRing_neg {n : ℤ} : smulRing (-n) = -1 • Jacobian.neg curveRing (smulRing n)

The negation rule over the universal ring.

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.smulField_neg {n : ℤ} : smulField (-n) = -1 • Jacobian.neg pointedCurve (smulField n)

The negation rule over the universal field.

theorem WeierstrassCurve.Universal.Jacobian.addXYZ_smulField {m n : ℤ} : Jacobian.addXYZ pointedCurve (smulField m) (smulField n) = polyToField (WeierstrassCurve.ψ curve (n - m)) • smulField (n + m)

Mathlib's Jacobian addition formula at (φₘ : ωₘ : ψₘ) and (φₙ : ωₙ : ψₙ) returns (φₙ₊ₘ : ωₙ₊ₘ : ψₙ₊ₘ), scaled by ψₙ₋ₘ. The scaling is genuine: addXYZ is homogeneous, and the representative it produces is the canonical triple only up to that factor.

theorem WeierstrassCurve.Universal.Jacobian.addXYZ_smulRing {m n : ℤ} : Jacobian.addXYZ curveRing (smulRing m) (smulRing n) = (AdjoinRoot.mk curve.polynomial) (WeierstrassCurve.ψ curve (n - m)) • smulRing (n + m)

The addition identity over the universal ring. addXYZ carries the triples at m and n to the triple at n + m, scaled by ψₙ₋ₘ: an equality in Universal.Ring, not merely of the points the triples represent. The scaling factor is genuine — addXYZ is homogeneous, so the representative it returns is the canonical triple only up to that factor.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.smulEval {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) (n : ℤ) : Fin 3 → R

The division polynomials of W evaluated at a point (x, y), as a Jacobian triple (φₙ(x,y), ωₙ(x,y), ψₙ(x,y)). The definition needs only a commutative ring. Over a field, and for a nonsingular (x, y), these are the Jacobian coordinates of n • (x, y) — that reading is zsmul_point_eq_smulEval below, which assumes [Field F], and it is not claimed over a general R.

Equations

• W.smulEval x y n = Polynomial.evalEval x y ∘ ![W.φ n, W.ω n, W.ψ n]

@[simp]

theorem WeierstrassCurve.smulEval_zero {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : W.smulEval x y 0 = ![1, 1, 0]

smulEval at 0 is (1, 1, 0), the Jacobian triple of the point at infinity.

@[simp]

theorem WeierstrassCurve.smulEval_one {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : W.smulEval x y 1 = ![x, y, 1]

smulEval at 1 is (x, y, 1): the point (x, y) itself, in Jacobian coordinates.

@[simp]

theorem WeierstrassCurve.Universal.ringEval_comp_smulRing {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) (n : ℤ) : ⇑(ringEval eqn) ∘ Jacobian.smulRing n = W.smulEval x y n

smulEval is the specialization of smulRing: the universal triple (φₙ, ωₙ, ψₙ), pushed along the homomorphism a point of W induces, is that point's evaluated triple. This is what turns each identity over curveRing into the same identity for W at (x, y).

@[simp]

theorem WeierstrassCurve.smulEval_neg {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (n : ℤ) : W.smulEval x y (-n) = -1 • Jacobian.neg W (W.smulEval x y n)

smulEval at -n: negating the index negates the triple, in the same (-1) • neg form as smulPoly_neg, smulRing_neg and smulField_neg. This is an identity of polynomial evaluations and needs no equation on (x, y).

theorem WeierstrassCurve.dblXYZ_smulEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) (n : ℤ) : Jacobian.dblXYZ W (W.smulEval x y n) = W.smulEval x y (2 * n)

The doubling formula for a concrete curve: dblXYZ_smulRing specialized along the point (x, y) of W.

theorem WeierstrassCurve.addXYZ_smulEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) (m n : ℤ) : Jacobian.addXYZ W (W.smulEval x y m) (W.smulEval x y n) = Polynomial.evalEval x y (W.ψ (n - m)) • W.smulEval x y (n + m)

The addition formula for a concrete curve: addXYZ_smulRing specialized along (x, y), scaling factor and all.

theorem WeierstrassCurve.zsmul_point_eq_smulEval {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (h : Affine.Nonsingular W x y) (n : ℤ) : (n • Jacobian.Point.fromAffine (Affine.Point.some x y h)).point = ⟦W.smulEval x y n⟧

The integer multiples of a nonsingular rational point are given by the division polynomials. For every n, the Jacobian coordinates of n • (x, y) on a Weierstrass curve over a field are (φₙ(x,y) : ωₙ(x,y) : ψₙ(x,y)).

Stated for a nonsingular (x, y) on a curve over a field, with no hypothesis on n and none on the characteristic.

theorem WeierstrassCurve.nonsingular_smulEval {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (h : Affine.Nonsingular W x y) (n : ℤ) : (toJacobian W.toAffine).Nonsingular (W.smulEval x y n)

The coordinate triple (φₙ : ωₙ : ψₙ) evaluated at a nonsingular affine point is a nonsingular Jacobian point. It is n • P written in coordinates, and a point of the curve is nonsingular by construction.

theorem WeierstrassCurve.zsmul_eq_zero_of_evalEval_ψ_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (hns : W.toAffine.Nonsingular x y) (n : ℤ) (hψ : Polynomial.evalEval x y (W.ψ n) = 0) : n • Jacobian.Point.fromAffine (Affine.Point.some x y hns) = 0

A root of ψₙ is annihilated by n, the converse of evalEval_ψ_eq_zero_of_zsmul_eq_zero. If ψₙ vanishes at P then n • P = 0.

Stated as annihilation rather than torsion, and deliberately left unrestricted in n. At n = 0 it is tautological on both sides — ψ₀ = 0 vanishes at every point and 0 • P = 0 for every P — so that case exhibits no torsion and the equation carries no content there. Genuine torsion at an index needs n ≠ 0 in addition.

theorem WeierstrassCurve.evalEval_ψ_eq_zero_of_zsmul_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (hns : W.toAffine.Nonsingular x y) (n : ℤ) (htors : n • Jacobian.Point.fromAffine (Affine.Point.some x y hns) = 0) : Polynomial.evalEval x y (W.ψ n) = 0

A torsion point is a root of its division polynomial. If n • P = 0 in the Jacobian point group, then ψₙ vanishes at P.

This is where zsmul_point_eq_smulEval is consumed: it identifies n • P with the class of (φₙ(x,y) : ωₙ(x,y) : ψₙ(x,y)), and a Jacobian class is the point at infinity exactly when its Z-coordinate vanishes.

theorem WeierstrassCurve.eval_ΨSq_eq_zero_iff_zsmul_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (hns : W.toAffine.Nonsingular x y) (n : ℤ) : Polynomial.eval x (W.ΨSq n) = 0 ↔ n • Jacobian.Point.fromAffine (Affine.Point.some x y hns) = 0

A point is n-torsion exactly when ΨSqₙ vanishes at its abscissa.

ΨSqₙ is the square of Ψₙ, which on the curve is ψₙ, so this is the ψ-criterion above read through the two evaluation bridges. Both directions hold pointwise, for a supplied y completing x to a point: no closure assumption is needed, because the point is given rather than produced, and no ellipticity, because neither bridge uses it.

theorem WeierstrassCurve.zsmul_fromAffine_eq_zero_iff_zsmul_eq_zero {F : Type u_1} [Field F] [DecidableEq F] {E : WeierstrassCurve F} {P : E.toAffine.Point} {n : ℤ} : n • Jacobian.Point.fromAffine P = 0 ↔ n • P = 0

Torsion transports between the affine and Jacobian point groups. n • P = 0 affinely, with n : ℕ, is the same statement as (n : ℤ) • P = 0 on the Jacobian side.

Stated as an iff because both directions are wanted: addOrderOf is ℕ-valued and affine while the theorems above take their torsion hypothesis on Jacobian.Point.fromAffine, so a vanishing statement travels forwards and a non-vanishing one backwards. The proof is the additive equivalence alone, so P ranges over every affine point, the point at infinity included.

The integer-scalar form zsmul_fromAffine_eq_zero_iff_zsmul_eq_zero is the one this rests on; the ℕ-cast reading below is its specialisation, and is what a consumer holding an ℕ-torsion hypothesis wants.

Not a simp lemma. Its left-hand side is not in simp normal form: natCast_zsmul rewrites (n : ℤ) • Q to n • Q, so tagging it @[simp] fails simpNF. The ℤ-cast orientation is nevertheless the useful one, because every consumer's torsion hypothesis is a ℤ-scalar multiple; stating it in ℕ-normal form would only move the cast to each call site.

theorem WeierstrassCurve.zsmul_fromAffine_eq_zero_iff {F : Type u_1} [Field F] [DecidableEq F] {E : WeierstrassCurve F} {P : E.toAffine.Point} {n : ℕ} : ↑n • Jacobian.Point.fromAffine P = 0 ↔ n • P = 0

theorem WeierstrassCurve.addOrderOf_eq_two_iff_evalEval_ψ₂_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [DecidableEq F] {x y : F} (hns : W.toAffine.Nonsingular x y) : addOrderOf (Affine.Point.some x y hns) = 2 ↔ Polynomial.evalEval x y W.ψ₂ = 0

Two-torsion is exactly the vanishing of ψ₂. For a nonsingular affine point, having order two and ψ₂ vanishing there are the same condition. Forwards, order two gives 2 • P = 0 and evalEval_ψ_eq_zero_of_zsmul_eq_zero at n = 2 reads off the vanishing; backwards, zsmul_eq_zero_of_evalEval_ψ_eq_zero at n = 2 gives 2 • P = 0, so the order divides 2, and a .some point is never 0, which rules out 1. Both directions cross between ψ 2 and ψ₂ by ψ_two.

Stated over the point's own field, with no arithmetic on the coefficients: consumers working over a fraction field transport their hypothesis across algebraMap at the call site.

Not a simp lemma. Neither side is a normal form the other should rewrite towards, and both directions are wanted — the ≠-form below is what discharges Nagell–Lutz's guard, while the = 2 direction is what an order computation wants.