The sieving parameters: the table and the array size

Every entry of Ratpoints.primeTable is a prime, which norm_num checks one entry at a time, the table lists every odd prime below 1022 in increasing order, which decide checks, so that its first Ratpoints.numPrimes entries are below Ratpoints.maxPrimeEven, a bound that keeps the accumulator of Horner's rule in examine_prime and the values of examine_power in the range of their C types (the lemmas on the values of examine_power discharge the range obligations that the Deviation paragraphs of the model state, and no proof consumes them); and the pieces of the numerators have at least one bit array.

Main statements

• Ratpoints.prime_of_mem_primeTable, Ratpoints.prime_getElem!_primeTable: every entry of Ratpoints.primeTable is a prime; Ratpoints.getElem!_primeTable_mod_two_eq_one: an odd one.
• Ratpoints.pairwise_lt_toList_primeTable, Ratpoints.lt_of_mem_primeTable, Ratpoints.mem_primeTable_of_prime: the table lists every odd prime below 1022, and nothing larger, in increasing order, which decide checks; Ratpoints.mem_of_toList_primeTable_eq: so it lists every odd prime below an entry before it; Ratpoints.le_of_toList_primeTable_eq_append_cons_cons: no prime lies between two neighbours; Ratpoints.forIn_toList_primeTable, Ratpoints.eq_of_toList_primeTable_eq_append_singleton: it begins with 3 and ends with 1021.
• Ratpoints.getElem!_primeTable_lt_maxPrimeEven: the first Ratpoints.numPrimes primes of the table are below Ratpoints.maxPrimeEven.
• Ratpoints.mul_add_lt_two_pow_64_of_lt_maxPrimeEven, Ratpoints.mul_self_lt_two_pow_63_of_lt_maxPrimeEven: the values of examine_power stay in the range of their C types, the moduli being below 2 ^ 10 (Ratpoints.maxPrimeEven_le_two_pow_10); Ratpoints.pow_hornerSteps_add_one_lt: so does the accumulator of Horner's rule in examine_prime between two reductions, since hornerSteps + 1 = 64 / maxBitsInPrime (Ratpoints.hornerSteps_add_one).
• Ratpoints.one_le_arraySizeAt, Ratpoints.Params.one_le_arraySizeAt: for a height bound H ≥ 1 a piece of the numerators has at least one bit array.

theorem Ratpoints.prime_of_mem_primeTable {p : ℕ} (h : p ∈ primeTable) : Nat.Prime p

theorem Ratpoints.pairwise_lt_toList_primeTable : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) primeTable.toList

theorem Ratpoints.lt_of_mem_primeTable {p : ℕ} (hp : p ∈ primeTable) : p < 1022

theorem Ratpoints.mem_primeTable_of_prime {q : ℕ} (hq : Nat.Prime q) (h2 : q ≠ 2) (h : q < 1022) : q ∈ primeTable

The table holds every odd prime below 1022, which decide checks: every odd number below 1022 that it does not hold has a divisor 1 < d < 32.

theorem Ratpoints.mem_of_toList_primeTable_eq {pref suff : List ℕ} {cur q : ℕ} (hl : primeTable.toList = pref ++ cur :: suff) (hq : Nat.Prime q) (h2 : q ≠ 2) (hlt : q < cur) : q ∈ pref

The table lists every odd prime below its entry cur before it, since it holds every odd prime below 1022 in increasing order: the cofactor that Ratpoints.Setup.factorLcf has left when it reaches cur has no prime factor below cur.

theorem Ratpoints.forIn_toList_primeTable : ForIn.toList primeTable = 3 :: primeTable.toList.tail

The table begins with 3, the first prime of the loop of Ratpoints.Setup.factorLcf.

theorem Ratpoints.two_lt_of_mem_toList_primeTable {q : ℕ} (hq : q ∈ primeTable.toList) : 2 < q

theorem Ratpoints.eq_of_toList_primeTable_eq_append_singleton {pref : List ℕ} {cur : ℕ} (hl : primeTable.toList = pref ++ [cur]) : cur = 1021

The last prime of the table is 1021.

theorem Ratpoints.le_of_toList_primeTable_eq_append_cons_cons {pref suff : List ℕ} {cur next p : ℕ} (hl : primeTable.toList = pref ++ cur :: next :: suff) (hp : Nat.Prime p) (hcp : cur < p) : next ≤ p

No prime lies strictly between two neighbours of the table, which lists every odd prime below 1022 in increasing order.

theorem Ratpoints.numPrimes_le_size_primeTable : numPrimes ≤ primeTable.size

The primes of the table by their positions

theorem Ratpoints.prime_getElem!_primeTable {pn : ℕ} (h : pn < primeTable.size) : Nat.Prime primeTable[pn]!

theorem Ratpoints.one_lt_getElem!_primeTable {pn : ℕ} (h : pn < numPrimes) : 1 < primeTable[pn]!

theorem Ratpoints.getElem!_primeTable_mod_two_eq_one {pn : ℕ} (h : pn < primeTable.size) : primeTable[pn]! % 2 = 1

theorem Ratpoints.getElem!_primeTable_lt_maxPrimeEven {pn : ℕ} (h : pn < numPrimes) : primeTable[pn]! < maxPrimeEven

The first Ratpoints.numPrimes primes of the table are below Ratpoints.maxPrimeEven, since the table increases.

The moduli in the range of the C types

theorem Ratpoints.mul_add_lt_two_pow_64_of_lt_maxPrimeEven {m v x c : ℕ} (hm : m < maxPrimeEven) (hv : v < m) (hx : x < m) (hc : c < m) : v * x + c < 2 ^ 64

The range obligation of the steps of Horner's rule in examine_power: for a modulus m < maxPrimeEven, the steps v x + c (find_points.c:2291, find_points.c:2298), with v, x and c below m, are below m ^ 2 ≤ 2 ^ 64 (Ratpoints.maxPrimeEven_le_two_pow_32): the unsigned longs do not wrap. The square of a residue, a product of longs, is Ratpoints.mul_self_lt_two_pow_63_of_lt_maxPrimeEven.

theorem Ratpoints.mul_self_lt_two_pow_63_of_lt_maxPrimeEven {x : ℕ} (hx : x < maxPrimeEven) : x * x < 2 ^ 63

The range obligation of the square x x of a residue in examine_power (find_points.c:2284), a product of longs: for x below a modulus, so below maxPrimeEven ≤ 2 ^ 10 (Ratpoints.maxPrimeEven_le_two_pow_10), it is below 2 ^ 20, so below 2 ^ 63: the signed product does not overflow.

theorem Ratpoints.hornerSteps_add_one : hornerSteps + 1 = 64 / maxBitsInPrime

The defining formula hornerSteps = 64 / maxBitsInPrime - 1 without the truncated subtraction, since 1 ≤ hornerSteps (Ratpoints.one_le_hornerSteps).

theorem Ratpoints.pow_hornerSteps_add_one_lt {p : ℕ} (hp : p < maxPrimeEven) : p ^ (hornerSteps + 1) < 2 ^ 64

The bound of the schedule of Horner's rule in examine_prime: p ^ (hornerSteps + 1) < 2 ^ 64 for p < maxPrimeEven, since hornerSteps + 1 = 64 / maxBitsInPrime (Ratpoints.hornerSteps_add_one) and maxBitsInPrime (64 / maxBitsInPrime) ≤ 64.

theorem Ratpoints.one_le_arraySizeAt (a : ℕ) {H : ℕ} (hH : 1 ≤ H) : 1 ≤ arraySizeAt a H

The pieces of the numerators are not empty, so that the loop over the pieces of a denominator advances; this reads off only that Ratpoints.defaultArraySize, Ratpoints.maxArraySize and the chunk Ratpoints.chunk are positive, the rounding up to a multiple of the chunk keeping the size at least 1.

theorem Ratpoints.Params.one_le_arraySizeAt (P : Params) {H : ℕ} (hH : 1 ≤ H) : 1 ≤ P.arraySizeAt H