Documentation

Elligator.Elligator1.Curve1174Prime

Primality of the Curve1174 characteristic #

Curve1174 of [bernstein2013a], Section 4, is defined over the prime field F_q with q = 2^251 - 9. This file establishes Nat.Prime q.

The proof runs the Pratt certificate machinery of Elligator.PrimalityCertificate: the factorisation

q - 1 = 2 * 19 * 3121 * p_6

is completed by recursively certifying the large prime factors p_1, …, p_6, each of which is again handled by Elligator.PrimalityCertificate.prime_of_pratt. All modular exponentiations are carried out with powMod, so the numerical side conditions are closed by decide and are checked by the Lean kernel.

Main results #

References #

See [bernstein2013a], Section 4.1.

source
theorem Elligator.Elligator1.Curve1174.prime_2032236244151 :
Nat.Prime 2032236244151

An auxiliary prime occurring in the Pratt certificate for q, verified by the Pratt certificate with base 7.

source
theorem Elligator.Elligator1.Curve1174.prime_20387630040577 :
Nat.Prime 20387630040577

An auxiliary prime occurring in the Pratt certificate for q, verified by the Pratt certificate with base 5.

source
theorem Elligator.Elligator1.Curve1174.prime_297581916939273464475253 :
Nat.Prime 297581916939273464475253

An auxiliary prime occurring in the Pratt certificate for q, verified by the Pratt certificate with base 5.

source
theorem Elligator.Elligator1.Curve1174.prime_2151858718037429125511251 :
Nat.Prime 2151858718037429125511251

An auxiliary prime occurring in the Pratt certificate for q, verified by the Pratt certificate with base 2.

source
theorem Elligator.Elligator1.Curve1174.prime_22645347980446549950250344634517843 :
Nat.Prime 22645347980446549950250344634517843

An auxiliary prime occurring in the Pratt certificate for q, verified by the Pratt certificate with base 2.

source
theorem Elligator.Elligator1.Curve1174.prime_30510656070643106182115999270826633842178510774222732476374386585332681 :
Nat.Prime 30510656070643106182115999270826633842178510774222732476374386585332681

An auxiliary prime occurring in the Pratt certificate for q, verified by the Pratt certificate with base 6.

source
theorem Elligator.Elligator1.Curve1174.q1174_prime :
Nat.Prime 3618502788666131106986593281521497120414687020801267626233049500247285301239

The characteristic q = 2 ^ 251 - 9 of the Curve1174 base field is prime, verified by the Pratt certificate with base 7.