The monic model of a Montgomery curve

A Montgomery curve is the plane cubic B y² = x³ + A x² + x. Its leading coefficient in y is B rather than 1, so it is not itself a Weierstrass equation; the substitution x' = B x, y' = B² y turns it into the monic equation

y'² = x'³ + A B x'² + B² x',

the Weierstrass curve TauCeti.Montgomery.model A B with coefficients (0, A B, 0, B², 0). Its discriminant is 16 B⁶ (A² - 4), so over a field it is elliptic exactly when 2, B and A² - 4 are nonzero. Points of a Montgomery curve are taken to be the native points (model A B).toAffine.Point of the monic model, with Mathlib's group law; no second group law is introduced.

When B ≠ 0 the affine point (0, 0) of the monic model is nonsingular and has order two; this is the distinguished point of order two TauCeti.Montgomery.twoTorsionPoint, through which every Montgomery curve has a rational point of order two. Over a domain with B ≠ 0, (x, y) solves the Montgomery equation exactly when its image (B x, B² y) under the substitution above solves the equation of the monic model, and likewise for nonsingular points; no square root of B is needed. Over a field this substitution is therefore a bijection between the two solution sets.

This is the setting of Montgomery's x-only arithmetic, used in Lenstra's elliptic-curve factorization method: the projective x-coordinate of a native point determines it up to sign, and doubling and differential addition can be computed on it alone.

Main definitions

• TauCeti.Montgomery.model A B: the Weierstrass curve y² = x³ + A B x² + B² x.
• TauCeti.Montgomery.twoTorsionPoint: the native point (0, 0) of model A B over a domain, for B ≠ 0.

Main results

• TauCeti.Montgomery.model_Δ: the discriminant of model A B is 16 B⁶ (A² - 4).
• TauCeti.Montgomery.isElliptic_model_iff: model A B is elliptic exactly when 2, B and A² - 4 are units; TauCeti.Montgomery.isElliptic_model_iff_ne_zero is the field version.
• TauCeti.Montgomery.map_model: base change of model A B along a ring homomorphism f is model (f A) (f B).
• TauCeti.Montgomery.model_eq_model_iff: two models agree exactly when their A B and B² coefficients do; over a domain with B ≠ 0, TauCeti.Montgomery.model_eq_model_iff_of_ne_zero says this happens exactly for (A', B') = (A, B) and (A', B') = (-A, -B).
• TauCeti.Montgomery.some_eq_twoTorsionPoint_iff: it is the only affine point with x-coordinate 0.
• TauCeti.Montgomery.addOrderOf_twoTorsionPoint: over a field, (0, 0) has order two.
• TauCeti.Montgomery.add_self_eq_twoTorsionPoint_iff: over a field, an affine point (x, y) satisfies P + P = (0, 0) exactly when x² = B².
• TauCeti.Montgomery.equation_model_iff and TauCeti.Montgomery.nonsingular_model_iff: for B ≠ 0 over a domain, (x, y) satisfies B y² = x³ + A x² + x (and is a nonsingular point of that cubic) exactly when (B x, B² y) satisfies the equation of model A B (and is a nonsingular point of it).

References

• P. L. Montgomery, Speeding the Pollard and elliptic curve methods of factorization, Math. Comp. 48 (1987), 243–264, §10.3.1, equation (10.3.1.1).

def TauCeti.Montgomery.model {R : Type u_1} [CommRing R] (A B : R) : WeierstrassCurve R

The monic model of the Montgomery curve B y² = x³ + A x² + x: the Weierstrass curve y² = x³ + A B x² + B² x, reached by x' = B x, y' = B² y. Its coefficients are (a₁, a₂, a₃, a₄, a₆) = (0, A B, 0, B², 0).

@[simp]

theorem TauCeti.Montgomery.model_a₁ {R : Type u_1} [CommRing R] (A B : R) : (model A B).a₁ = 0

@[simp]

theorem TauCeti.Montgomery.model_a₂ {R : Type u_1} [CommRing R] (A B : R) : (model A B).a₂ = A * B

@[simp]

theorem TauCeti.Montgomery.model_a₃ {R : Type u_1} [CommRing R] (A B : R) : (model A B).a₃ = 0

@[simp]

theorem TauCeti.Montgomery.model_a₄ {R : Type u_1} [CommRing R] (A B : R) : (model A B).a₄ = B ^ 2

@[simp]

theorem TauCeti.Montgomery.model_a₆ {R : Type u_1} [CommRing R] (A B : R) : (model A B).a₆ = 0

@[simp]

theorem TauCeti.Montgomery.model_b₂ {R : Type u_1} [CommRing R] (A B : R) : (model A B).b₂ = 4 * (A * B)

@[simp]

theorem TauCeti.Montgomery.model_b₄ {R : Type u_1} [CommRing R] (A B : R) : (model A B).b₄ = 2 * B ^ 2

@[simp]

theorem TauCeti.Montgomery.model_b₆ {R : Type u_1} [CommRing R] (A B : R) : (model A B).b₆ = 0

@[simp]

theorem TauCeti.Montgomery.model_b₈ {R : Type u_1} [CommRing R] (A B : R) : (model A B).b₈ = -B ^ 4

@[simp]

theorem TauCeti.Montgomery.model_c₄ {R : Type u_1} [CommRing R] (A B : R) : (model A B).c₄ = 16 * B ^ 2 * (A ^ 2 - 3)

The c₄ of the monic model is 16 B² (A² - 3).

@[simp]

theorem TauCeti.Montgomery.model_c₆ {R : Type u_1} [CommRing R] (A B : R) : (model A B).c₆ = -32 * A * B ^ 3 * (2 * A ^ 2 - 9)

The c₆ of the monic model is -32 A B³ (2 A² - 9).

@[simp]

theorem TauCeti.Montgomery.model_Δ {R : Type u_1} [CommRing R] (A B : R) : (model A B).Δ = 16 * B ^ 6 * (A ^ 2 - 4)

The discriminant of the monic Montgomery model is 16 B⁶ (A² - 4).

@[simp]

theorem TauCeti.Montgomery.map_model {R : Type u_1} [CommRing R] (A B : R) {S : Type u_2} [CommRing S] (f : R →+* S) : (model A B).map f = model (f A) (f B)

The image of the monic model under a ring homomorphism is the monic model of the images.

theorem TauCeti.Montgomery.isElliptic_model_iff {R : Type u_1} [CommRing R] (A B : R) : (model A B).IsElliptic ↔ IsUnit 2 ∧ IsUnit B ∧ IsUnit (A ^ 2 - 4)

The monic Montgomery model is elliptic exactly when 2, B and A² - 4 are units.

theorem TauCeti.Montgomery.model_eq_model_iff {R : Type u_1} [CommRing R] {A B A' B' : R} : model A B = model A' B' ↔ A * B = A' * B' ∧ B ^ 2 = B' ^ 2

Two monic models are equal exactly when their a₂ = A B and a₄ = B² coefficients agree.

theorem TauCeti.Montgomery.nonsingular_model_zero_zero {R : Type u_1} [CommRing R] (A B : R) : (model A B).toAffine.Nonsingular 0 0 ↔ B ^ 2 ≠ 0

The affine point (0, 0) of the monic model is nonsingular exactly when B² ≠ 0: the partial derivative of the equation in x there is -B².

theorem TauCeti.Montgomery.model_eq_model_iff_of_ne_zero {R : Type u_1} [CommRing R] [NoZeroDivisors R] {A B : R} (hB : B ≠ 0) {A' B' : R} : model A B = model A' B' ↔ A' = A ∧ B' = B ∨ A' = -A ∧ B' = -B

Over a domain, two monic models with B ≠ 0 are equal exactly when (A', B') is (A, B) or (-A, -B).

theorem TauCeti.Montgomery.equation_model_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {A B : R} (hB : B ≠ 0) (x y : R) : (model A B).toAffine.Equation (B * x) (B ^ 2 * y) ↔ B * y ^ 2 = x ^ 3 + A * x ^ 2 + x

The Montgomery equation and the monic model. For B ≠ 0 over a domain, (x, y) satisfies B y² = x³ + A x² + x exactly when (B x, B² y) lies on model A B.

theorem TauCeti.Montgomery.nonsingular_model_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {A B : R} (hB : B ≠ 0) (x y : R) : (model A B).toAffine.Nonsingular (B * x) (B ^ 2 * y) ↔ B * y ^ 2 = x ^ 3 + A * x ^ 2 + x ∧ (3 * x ^ 2 + 2 * A * x + 1 ≠ 0 ∨ 2 * B * y ≠ 0)

Nonsingularity on the Montgomery curve and on the monic model. For B ≠ 0 over a domain, (x, y) is a nonsingular point of B y² = x³ + A x² + x, that is, it lies on the curve and one of the partial derivatives 3 x² + 2 A x + 1 and 2 B y is nonzero, exactly when (B x, B² y) is a nonsingular point of model A B.

def TauCeti.Montgomery.twoTorsionPoint {R : Type u_1} [CommRing R] [NoZeroDivisors R] (A : R) {B : R} (hB : B ≠ 0) : (model A B).toAffine.Point

The distinguished point of order two T₀ of the monic Montgomery model, the affine point (0, 0), defined when B ≠ 0.

theorem TauCeti.Montgomery.twoTorsionPoint_def {R : Type u_1} [CommRing R] [NoZeroDivisors R] (A : R) {B : R} (hB : B ≠ 0) : twoTorsionPoint A hB = WeierstrassCurve.Affine.Point.some 0 0 ⋯

The distinguished point of order two is the affine point (0, 0) of the monic model.

theorem TauCeti.Montgomery.some_eq_twoTorsionPoint_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {A B : R} (hB : B ≠ 0) {x y : R} (h : (model A B).toAffine.Nonsingular x y) : WeierstrassCurve.Affine.Point.some x y h = twoTorsionPoint A hB ↔ x = 0

An affine point of the monic model is the distinguished point of order two exactly when its x-coordinate is 0: the equation forces y² = 0 there.

theorem TauCeti.Montgomery.twoTorsionPoint_ne_zero {R : Type u_1} [CommRing R] [NoZeroDivisors R] (A : R) {B : R} (hB : B ≠ 0) : twoTorsionPoint A hB ≠ 0

The distinguished point of order two is not the point at infinity.

@[simp]

theorem TauCeti.Montgomery.neg_twoTorsionPoint {R : Type u_1} [CommRing R] [NoZeroDivisors R] (A : R) {B : R} (hB : B ≠ 0) : -twoTorsionPoint A hB = twoTorsionPoint A hB

The distinguished point of order two is its own negative.

theorem TauCeti.Montgomery.isElliptic_model_iff_ne_zero {K : Type u_1} [Field K] {A B : K} : (model A B).IsElliptic ↔ 2 ≠ 0 ∧ B ≠ 0 ∧ A ^ 2 ≠ 4

The monic Montgomery model over a field is elliptic exactly when 2, B and A² - 4 are nonzero.

@[simp]

theorem TauCeti.Montgomery.twoTorsionPoint_add_self {K : Type u_1} [Field K] (A : K) {B : K} [DecidableEq K] (hB : B ≠ 0) : twoTorsionPoint A hB + twoTorsionPoint A hB = 0

The distinguished point of order two is killed by 2.

@[simp]

theorem TauCeti.Montgomery.addOrderOf_twoTorsionPoint {K : Type u_1} [Field K] (A : K) {B : K} [DecidableEq K] (hB : B ≠ 0) : addOrderOf (twoTorsionPoint A hB) = 2

The distinguished point (0, 0) has order two in the native group of the monic model.

theorem TauCeti.Montgomery.add_self_eq_twoTorsionPoint_iff {K : Type u_1} [Field K] {A B : K} [DecidableEq K] (hB : B ≠ 0) {x y : K} (h : (model A B).toAffine.Nonsingular x y) : WeierstrassCurve.Affine.Point.some x y h + WeierstrassCurve.Affine.Point.some x y h = twoTorsionPoint A hB ↔ x ^ 2 = B ^ 2

The halves of the distinguished point of order two. An affine point (x, y) of the monic model satisfies P + P = (0, 0) exactly when x² = B², that is, when its Montgomery coordinate x / B is ±1.