Suyama's family of Montgomery curves

Suyama's parametrization supplies a Montgomery curve together with a rational point. Put u = σ² - 5 and v = 4σ. The parameter suyamaA σ is chosen so that its scaled doubling constants have polynomial expressions; suyamaB σ makes (u³/v³, 1) a point on the curve.

The main result isElliptic_model_suyama_iff describes the exact exceptional set, over any field of characteristic different from two, including characteristic three. The only standing restrictions on the parameter are σ ≠ 0 and σ² ≠ 5, which keep the denominators nonzero. The factorization of suyamaB and of suyamaA² - 4 explains all five exceptional factors.

References

• P. Zimmermann, 20 years of ECM, ANTS VII (2006), author's submitted version, §1, p. 3, for Suyama's parametrization.

def TauCeti.Montgomery.suyamaU {R : Type u_1} [CommRing R] (σ : R) : R

The auxiliary polynomial u = σ² - 5 in Suyama's parametrization.

def TauCeti.Montgomery.suyamaV {R : Type u_1} [CommRing R] (σ : R) : R

The auxiliary polynomial v = 4σ in Suyama's parametrization.

@[simp]

theorem TauCeti.Montgomery.suyamaU_def {R : Type u_1} [CommRing R] (σ : R) : suyamaU σ = σ ^ 2 - 5

@[simp]

theorem TauCeti.Montgomery.suyamaV_def {R : Type u_1} [CommRing R] (σ : R) : suyamaV σ = 4 * σ

theorem TauCeti.Montgomery.suyamaV_sub_suyamaU {R : Type u_1} [CommRing R] (σ : R) : suyamaV σ - suyamaU σ = -(σ - 5) * (σ + 1)

The first linear factorization used in the numerator of A + 2.

theorem TauCeti.Montgomery.suyamaV_add_suyamaU {R : Type u_1} [CommRing R] (σ : R) : suyamaV σ + suyamaU σ = (σ + 5) * (σ - 1)

The first linear factorization used in the numerator of A - 2.

theorem TauCeti.Montgomery.three_mul_suyamaU_add_suyamaV {R : Type u_1} [CommRing R] (σ : R) : 3 * suyamaU σ + suyamaV σ = (3 * σ - 5) * (σ + 3)

The second linear factorization used in the numerator of A + 2.

theorem TauCeti.Montgomery.suyamaV_sub_three_mul_suyamaU {R : Type u_1} [CommRing R] (σ : R) : suyamaV σ - 3 * suyamaU σ = -(3 * σ + 5) * (σ - 3)

The second linear factorization used in the numerator of A - 2.

def TauCeti.Montgomery.suyamaA {K : Type u_1} [Field K] (σ : K) : K

Suyama's Montgomery parameter A, in the (A + 2)/4 doubling convention.

def TauCeti.Montgomery.suyamaX {K : Type u_1} [Field K] (σ : K) : K

The Montgomery x-coordinate u³/v³ of Suyama's supplied point.

theorem TauCeti.Montgomery.suyamaX_def {K : Type u_1} [Field K] (σ : K) : suyamaX σ = suyamaU σ ^ 3 / suyamaV σ ^ 3

The supplied affine coordinate in terms of the auxiliary polynomials.

def TauCeti.Montgomery.suyamaB {K : Type u_1} [Field K] (σ : K) : K

Suyama's parameter B, chosen so that (suyamaX σ, 1) lies on the Montgomery curve.

theorem TauCeti.Montgomery.suyamaB_def {K : Type u_1} [Field K] (σ : K) : suyamaB σ = suyamaX σ ^ 3 + suyamaA σ * suyamaX σ ^ 2 + suyamaX σ

The supplied Montgomery point satisfies the curve equation, even at exceptional parameters.

theorem TauCeti.Montgomery.suyamaV_ne_zero {K : Type u_1} [Field K] {σ : K} (hB : suyamaB σ ≠ 0) : suyamaV σ ≠ 0

Nonzero B forces the denominator auxiliary polynomial v to be nonzero.

theorem TauCeti.Montgomery.suyama_denominator_ne_zero {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) : 4 * suyamaU σ ^ 3 * suyamaV σ ≠ 0

The denominator in Suyama's formula is nonzero under the standing parameter restrictions.

theorem TauCeti.Montgomery.suyamaA_add_two {K : Type u_1} [Field K] (σ : K) : suyamaA σ + 2 = (suyamaV σ - suyamaU σ) ^ 3 * (3 * suyamaU σ + suyamaV σ) / (4 * suyamaU σ ^ 3 * suyamaV σ)

The factored formula for A + 2.

theorem TauCeti.Montgomery.suyamaA_sub_two {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) : suyamaA σ - 2 = (suyamaV σ + suyamaU σ) ^ 3 * (suyamaV σ - 3 * suyamaU σ) / (4 * suyamaU σ ^ 3 * suyamaV σ)

The factored formula for A - 2.

theorem TauCeti.Montgomery.suyama_doubling_relation {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) : 4 * ((suyamaV σ - suyamaU σ) ^ 3 * (3 * suyamaU σ + suyamaV σ)) = (suyamaA σ + 2) * (16 * suyamaU σ ^ 3 * suyamaV σ)

The polynomial numerator and denominator give valid scaled doubling constants.

theorem TauCeti.Montgomery.suyamaB_eq {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) : suyamaB σ = suyamaU σ * (σ ^ 2 - 1) ^ 2 * (σ ^ 2 - 25) ^ 2 * (σ ^ 4 - 25) ^ 2 / suyamaV σ ^ 9

The factorization of B isolates the parameters where the supplied model degenerates.

theorem TauCeti.Montgomery.suyamaA_sq_sub_four {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) : suyamaA σ ^ 2 - 4 = (σ ^ 2 - 1) ^ 3 * (σ ^ 2 - 25) ^ 3 * (9 * σ ^ 2 - 25) * (σ ^ 2 - 9) / (16 * suyamaU σ ^ 6 * suyamaV σ ^ 2)

The factorization of A² - 4, without excluding characteristic three.

theorem TauCeti.Montgomery.isElliptic_model_suyama_iff {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) : (model (suyamaA σ) (suyamaB σ)).IsElliptic ↔ (σ ^ 2 - 1) * (σ ^ 2 - 9) * (σ ^ 2 - 25) * (9 * σ ^ 2 - 25) * (σ ^ 2 + 5) ≠ 0

Suyama's exact ellipticity criterion. Under the denominator restrictions, precisely these five factors detect singular models. No odd characteristic is excluded.

theorem TauCeti.Montgomery.nonsingular_suyama {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0) (hB : suyamaB σ ≠ 0) : (model (suyamaA σ) (suyamaB σ)).toAffine.Nonsingular (suyamaB σ * suyamaX σ) (suyamaB σ ^ 2)

When B is nonzero, Suyama's supplied point becomes a nonsingular point of the monic model under x' = Bx, y' = B². This does not require ellipticity of the model.