def ECPrimality.shortWeierstrass (R : Type u_1) [CommRing R] (A B : R) : WeierstrassCurve R

The short Weierstrass curve $y^2 = x^3 + Ax + B$ over a commutative ring $R$.

def ECPrimality.curveModN (n : ℕ) (A B : ℤ) : WeierstrassCurve.Affine (ZMod n)

The affine short Weierstrass curve $y^2 = x^3 + Ax + B$ reduced modulo $n$.

structure PrimalityCertificate : Type

A Goldwasser-Kilian primality certificate (Definition 11.14) for a positive integer $p > 1$. It bundles:

• short Weierstrass coefficients $A, B \in \mathbb{Z}$ defining a curve $E$,
• an affine point $(x_1, y_1)$ on $E$,
• an integer $q > (p^{1/4} + 1)^2$,
• a proof that the discriminant $-16(4A^3 + 27B^2)$ is coprime to $p$,
• a proof that the reduction of $(x_1, y_1)$ mod $p$ is nonsingular, and
• a proof that $q \cdot (x_1, y_1) = O$ in $E(\mathbb{Z}/p\mathbb{Z})$ whenever $p$ is prime.

By Theorem 11.13 the existence of such a certificate implies $p$ is prime.

• p : ℤ
• A : ℤ
• B : ℤ
• x₁ : ℤ
• y₁ : ℤ
• q : ℤ
• hp : 1 < self.p
• hq : ↑self.q > (↑self.p ^ (1 / 4) + 1) ^ 2
• on_curve : self.y₁ ^ 2 = self.x₁ ^ 3 + self.A * self.x₁ + self.B
• coprime_disc : self.p.gcd (-16 * (4 * self.A ^ 3 + 27 * self.B ^ 2)) = 1
• point_nonsingular : (ECPrimality.curveModN self.p.toNat self.A self.B).Nonsingular ↑self.x₁ ↑self.y₁
• hqP_zero (hp_prime : Nat.Prime self.p.toNat) : self.q • WeierstrassCurve.Affine.Point.some ↑self.x₁ ↑self.y₁ ⋯ = 0