inductive Hex.ECPP.Cert : Type

Mathematical data to prove an integer prime by elliptic curve primality proving (ECPP). The data must pass Hex.ECPP.check before it proves anything.

base cert uses an existing HexPrimality certificate. In step n a b x y discrInv inverses child, the curve is y² = x³ + a*x + b modulo n, the point is (x,y), and child certifies the prime scalar used to multiply the point. discrInv witnesses that 4*a³ + 27*b² is invertible; inverses justifies the divisions in that scalar multiplication. The checker also verifies the curve equation and the strict size condition needed for Hasse's bound.

• base (cert : Nat.PrimeCert) : Cert
• step (n a b x y discrInv : Nat) (inverses : List Nat) (child : Cert) : Cert

@[instance_reducible]

instance Hex.ECPP.instReprCert : Repr Cert

Equations

• Hex.ECPP.instReprCert = { reprPrec := Hex.ECPP.instReprCert.repr }

def Hex.ECPP.instReprCert.repr : Cert → Nat → Std.Format

Equations

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

def Hex.ECPP.Cert.subject : Cert → Nat

The integer whose primality this certificate is intended to establish. Its primality follows only after the certificate passes the checker.

Equations

• (Hex.ECPP.Cert.base cert).subject = cert.subject
• (Hex.ECPP.Cert.step n a b x_1 y discrInv inverses child).subject = n