Prime powers and products as moduli

The sieve entry of a modulus m that the choice of the moduli makes (Ratpoints.primeEntry for a prime, Ratpoints.makeModulus for a composite modulus) holds its factors: a prime with its table, and a prime power p ^ e with the tables of examine_power (Ratpoints.Sieve.examinePower): the bit arrays of Ratpoints.modWords words of the residues at which f, and of the multiples of p at which the reversed polynomial, take square values, read from the bit array of the squares (Ratpoints.Sieve.setSquareBits_spec), and the inverses of the units, from the extended Euclidean algorithm (Ratpoints.Sieve.modinv) in a loop over the residues (Ratpoints.Sieve.unitInverses_spec), all in Ratpoints.Sieve.examinePower_spec, for either value of the flag pinf, which only the density reads. The tables of a prime power within the words of its bit arrays compute what they claim, and its rows let every point through (Ratpoints.Sieve.admits_run_examinePower_of_sq_eq): for p ∤ b, since f(a / b) is a square modulo p ^ e, and for p ∣ b, since then p ∤ a and the reversed polynomial takes a square value at b / a, both from the lemmas of Ratpoints.Proof.Tables for any commutative ring, here ZMod (p ^ e); the prime powers below Ratpoints.maxPrimeEven fit the words (Ratpoints.maxPrimeEven_le_sixty_four_mul_modWords). The values of examine_power stay in the range of their C types for the prime powers below Ratpoints.maxPrimeEven: the cofactors of the extended Euclidean algorithm (Ratpoints.Sieve.ModinvInvariant.natAbs_add_mul_le), the steps of Horner's rule and the squares (Ratpoints.mul_add_lt_two_pow_64_of_lt_maxPrimeEven, Ratpoints.mul_self_lt_two_pow_63_of_lt_maxPrimeEven), and the inverses (Ratpoints.Sieve.getElem!_inv_run_examinePower_lt_two_pow_16); these lemmas discharge the range obligations that the Deviation paragraphs of the model state, and no proof consumes them. A factor that divides m reads the residues modulo m as those of the numbers (Ratpoints.Sieve.Entry.admits_mod_of_dvd, Ratpoints.Sieve.Power.admits_mod_of_dvd, in Ratpoints.Proof.Words) and lets every point through (Ratpoints.Sieve.isSound_prime_examinePrime, Ratpoints.Sieve.isSound_power_run_examinePower); no Chinese remainder theorem is needed. The tables of inverses of its factors serve the scaling of the rows by a unit modulo m (Ratpoints.Sieve.Factor.HasInverses). An entry of an odd modulus whose factors are sound and multiply to m, with the bias of m and an inverse of Ratpoints.rbaLength modulo m, read from the table of a prime as examine_prime reads it (Ratpoints.inverses_mulMod_rbaLength_of_isSound) or computed with Ratpoints.Sieve.modinv, has what the packing of the numerators reads (Ratpoints.Sieve.SieveEntry.Packable), and with the reference to its table of rows and the kind of its builder that Ratpoints.Sieve.SieveEntry.refInit gives at its position it fits the rows of the references of the run (Ratpoints.IsModulusEntry.rowsFit_runRows).

Main definitions

• Ratpoints.Sieve.ModinvState, Ratpoints.Sieve.ModinvInvariant, Ratpoints.Sieve.SquareBitsInvariant, Ratpoints.Sieve.UnitInversesInvariant, Ratpoints.Sieve.FsqInvariant, Ratpoints.Sieve.GsqInvariant: the state of the loop of Ratpoints.Sieve.modinv and its invariant, and the invariants of the loops over the residues of Ratpoints.Sieve.setSquareBits and Ratpoints.Sieve.unitInverses, and of the loops of Ratpoints.Sieve.examinePower and Ratpoints.Sieve.setRevBits that set the bits of fsq and gsq.
• Ratpoints.Sieve.Factor.IsSound: a factor whose rows admit every point modulo m, whose tables of inverses serve the scaling, whose builder has what it needs and whose tables are those that Ratpoints.Sieve.examinePrime and Ratpoints.Sieve.examinePower compute.
• Ratpoints.IsModulusEntry: what the soundness of the run needs of the sieve entry of a modulus: the modulus, sound factors whose moduli multiply to it, and the fields of the packing.

Main statements

• Ratpoints.Sieve.modinv_spec: for x prime to m > 1, Ratpoints.Sieve.modinv gives the inverse of x modulo m, below m; Ratpoints.Sieve.ModinvInvariant.natAbs_add_mul_le: its cofactors stay between -m and m.
• Ratpoints.Sieve.setSquareBits_spec, Ratpoints.Sieve.unitInverses_spec: the bits of the squares and the inverses of the units of a prime power.
• Ratpoints.Sieve.examinePower_spec, with its plain forms Ratpoints.Sieve.getElem!_inv_run_examinePower_lt and Ratpoints.Sieve.mul_getElem!_inv_run_examinePower_mod: the inverses of a prime power are below it and hold the inverses of the units; Ratpoints.Sieve.bitAt_fsq_run_examinePower_of_isSquare, Ratpoints.Sieve.bitAt_gsq_run_examinePower_of_isSquare: its tables mark the residues at which f, or the reversed polynomial at a multiple of p, takes a square value.
• Ratpoints.Sieve.getElem!_inv_run_examinePower_lt_two_pow_16: the inverses of a prime power below Ratpoints.maxPrimeEven are below 2 ^ 16, the range of their C type.
• Ratpoints.Sieve.admits_run_examinePower_of_sq_eq: the rows of a prime power let every point through.
• Ratpoints.Sieve.isSound_prime_examinePrime, Ratpoints.Sieve.isSound_power_run_examinePower: a prime of the table, or a power of one, that divides m is a sound factor for m.
• Ratpoints.isModulusEntry_of_forall_isSound: an entry of an odd modulus with sound factors that multiply to it, its reciprocal, bias and an inverse of Ratpoints.rbaLength is Ratpoints.IsModulusEntry; Ratpoints.inverses_mulMod_rbaLength_of_isSound: the inverse that a prime reads from its table.
• Ratpoints.IsModulusEntry.admits_of_sq_eq, Ratpoints.IsModulusEntry.rowsFit_runRows: such an entry admits every point and fits the rows of the references of the run (Ratpoints.Sieve.runRows).
• Ratpoints.coprime_rbaLength_of_mod_two_eq_one: an odd modulus is prime to Ratpoints.rbaLength.

Implementation notes

The contracts of Ratpoints.Sieve.modinv, Ratpoints.Sieve.setSquareBits, Ratpoints.Sieve.unitInverses and Ratpoints.Sieve.examinePower are proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions, in a file with Mathlib, next to the soundness of the rows that they serve; the density of a prime power (Ratpoints.Sieve.powerDensity) is read through a private specification ⦃True⦄ x ⦃fun r ↦ r = Id.run x⦄, since no contract reads its value.

The inverse modulo m by the extended Euclidean algorithm

structure Ratpoints.Sieve.ModinvState (x m : ℕ) (exit : Bool) (s : ℕ × ℕ × ℤ × ℤ) : Prop

The state of the loop of Ratpoints.Sieve.modinv for x modulo m, on the remainders r₀, r₁ and the cofactors s₀, s₁, with the flag of the exit: rᵢ ≡ sᵢ x (mod m), gcd(r₀, r₁) = gcd(m, x), r₀ > 0, the cofactors are of opposite signs or one of them is 0, |s₀| r₁ + |s₁| r₀ = m, |s₀| ≤ m, and r₁ = 0 at the exit.

• natCast_fst_eq : ↑s.1 = ↑s.2.2.1 * ↑x

  r₀ ≡ s₀ x (mod m).

• natCast_snd_eq : ↑s.2.1 = ↑s.2.2.2 * ↑x

  r₁ ≡ s₁ x (mod m).

• gcd_eq : s.1.gcd s.2.1 = m.gcd x

  gcd(r₀, r₁) = gcd(m, x).

• fst_pos : 0 < s.1

  r₀ > 0.

• mul_nonpos : s.2.2.1 * s.2.2.2 ≤ 0

  The cofactors are of opposite signs, or one of them is 0.

• natAbs_mul_add_eq : s.2.2.1.natAbs * s.2.1 + s.2.2.2.natAbs * s.1 = m

  |s₀| r₁ + |s₁| r₀ = m.

• natAbs_le : s.2.2.1.natAbs ≤ m

  |s₀| ≤ m.

• snd_eq_zero : exit = true → s.2.1 = 0

  r₁ = 0 at the exit.

def Ratpoints.Sieve.ModinvInvariant (x m : ℕ) : Std.WP.WhileInvariant (ℕ × ℕ × ℤ × ℤ) Prop

The invariant of the loop of Ratpoints.Sieve.modinv for x modulo m (Ratpoints.Sieve.ModinvState).

Equations

• Ratpoints.Sieve.ModinvInvariant x m = Std.WP.WhileInvariant.mk (Ratpoints.Sieve.ModinvState x m)

theorem Ratpoints.Sieve.modinvInvariant_zero {x m : ℕ} (hm : 0 < m) : ModinvInvariant x m false (m, x % m, 0, 1)

theorem Ratpoints.Sieve.ModinvInvariant.sub_lt_and_sub_mul {x m r₀ r₁ : ℕ} {s₀ s₁ : ℤ} (h : ModinvInvariant x m false (r₀, r₁, s₀, s₁)) (hr : ¬r₁ = 0) : r₀ - r₀ / r₁ * r₁ < r₁ ∧ ModinvInvariant x m false (r₁, r₀ - r₀ / r₁ * r₁, s₁, s₀ - ↑(r₀ / r₁) * s₁)

The step of the loop of Ratpoints.Sieve.modinv, with the measure r₁.

theorem Ratpoints.Sieve.ModinvInvariant.natAbs_add_mul_le {x m r₀ r₁ : ℕ} {s₀ s₁ : ℤ} (h : ModinvInvariant x m false (r₀, r₁, s₀, s₁)) (hr : ¬r₁ = 0) : s₁.natAbs ≤ m ∧ s₀.natAbs + r₀ / r₁ * s₁.natAbs ≤ m

The range obligation of the cofactors of modinv (find_points.c:2246-2249): in each step of the loop, the product q s₁ and the new cofactor s₀ - q s₁, q = ⌊r₀ / r₁⌋, lie between -m and m, as s₀ and s₁ do, so that the longs do not overflow for m < 2 ^ 63.

theorem Ratpoints.Sieve.ModinvInvariant.exit {x m : ℕ} {s : ℕ × ℕ × ℤ × ℤ} (h : ModinvInvariant x m false s) (hr : ¬¬s.2.1 = 0) : ModinvInvariant x m true s

theorem Ratpoints.Sieve.ModinvInvariant.post {x m r₀ r₁ : ℕ} {s₀ s₁ : ℤ} (h : ModinvInvariant x m true (r₀, r₁, s₀, s₁)) (hm : 1 < m) (hx : x.Coprime m) : (if s₀ < 0 then s₀ + ↑m else s₀).toNat < m ∧ x * (if s₀ < 0 then s₀ + ↑m else s₀).toNat % m = 1

The exit of the loop of Ratpoints.Sieve.modinv for x prime to m > 1: r₀ = gcd(m, x) = 1, so that s₀ x ≡ 1 (mod m), and |s₀| ≤ m.

theorem Ratpoints.Sieve.modinv_spec (x m : ℕ) : ⦃ 1 < m ∧ x.Coprime m ⦄ modinv x m ⦃ fun (r : ℕ) => r < m ∧ x * r % m = 1 ⦄

The contract of Ratpoints.Sieve.modinv: for x prime to m > 1, the extended Euclidean algorithm gives the inverse of x modulo m, below m. The loop ends, since r₁ drops; the cofactors stay between -m and m (Ratpoints.Sieve.ModinvInvariant.natAbs_add_mul_le).

The tables of a prime power

def Ratpoints.Sieve.SquareBitsInvariant (m : ℕ) (pref : List ℕ) (sq : Array UInt64) : Prop

The invariant of the loop of Ratpoints.Sieve.setSquareBits after the residues pref, on the bit array: Ratpoints.modWords words, the bits of the squares x ^ 2 mod m of the residues x of pref set.

Equations

• Ratpoints.Sieve.SquareBitsInvariant m pref sq = (sq.size = Ratpoints.modWords ∧ ∀ x ∈ pref, Ratpoints.Sieve.bitAt sq (x * x % m) = true)

theorem Ratpoints.Sieve.squareBitsInvariant_nil {m : ℕ} {sq : Array UInt64} (h : sq.size = modWords ∧ m ≤ 64 * modWords) : SquareBitsInvariant m [] sq

theorem Ratpoints.Sieve.SquareBitsInvariant.push {m cur : ℕ} {pref suff : List ℕ} {sq₀ sq : Array UInt64} (pre : sq₀.size = modWords ∧ m ≤ 64 * modWords) (hl : ForIn.toList [:m] = pref ++ cur :: suff) (h : SquareBitsInvariant m pref sq) : SquareBitsInvariant m (pref ++ [cur]) (setBitAt sq (cur * cur % m))

The step of the loop of Ratpoints.Sieve.setSquareBits at the residue cur < m, within the words of the bit array.

theorem Ratpoints.Sieve.SquareBitsInvariant.post {m : ℕ} {sq : Array UInt64} (h : SquareBitsInvariant m (ForIn.toList [:m]) sq) : sq.size = modWords ∧ ∀ x < m, bitAt sq (x * x % m) = true

theorem Ratpoints.Sieve.setSquareBits_spec (m : ℕ) (sq : Array UInt64) : ⦃ sq.size = modWords ∧ m ≤ 64 * modWords ⦄ setSquareBits m sq ⦃ fun (sq' : Array UInt64) => sq'.size = modWords ∧ ∀ x < m, bitAt sq' (x * x % m) = true ⦄

The contract of Ratpoints.Sieve.setSquareBits on a bit array of Ratpoints.modWords words with room for m bits: the bits of the squares modulo m are set.

theorem Ratpoints.Sieve.bitAt_of_isSquare {m v : ℕ} {sq : Array UInt64} (h : ∀ x < m, bitAt sq (x * x % m) = true) (hv : v < m) (hsq : IsSquare ↑v) : bitAt sq v = true

A bit array in which the bits of the squares modulo m are set has the bit of every residue v < m that is a square modulo m.

theorem Ratpoints.Sieve.examinePower_eq_examinePower_false (c : List ℤ) (d p e : ℕ) (u pinf : Bool) : examinePower c d p e u pinf = examinePower c d p e false pinf

The path through longs, with the helper mod of the C code, and the path through GMP integers give the same tables of a prime power.

def Ratpoints.Sieve.UnitInversesInvariant (p m k : ℕ) (inv : Array ℕ) : Prop

The invariant of the loop of Ratpoints.Sieve.unitInverses over the residues 1, …, k modulo m, on the inverses inv: k + 1 entries, each below m, that of a residue not divisible by p its inverse modulo m.

Equations

• Ratpoints.Sieve.UnitInversesInvariant p m k inv = (inv.size = k + 1 ∧ ∀ x < inv.size, inv[x]! < m ∧ (x % p ≠ 0 → x * inv[x]! % m = 1))

theorem Ratpoints.Sieve.unitInversesInvariant_zero (p : ℕ) {m : ℕ} (hm : 0 < m) : UnitInversesInvariant p m 0 #[0]

theorem Ratpoints.Sieve.UnitInversesInvariant.push_zero {p m cur : ℕ} {pref suff : List ℕ} {inv : Array ℕ} (hl : ForIn.toList [1:m] = pref ++ cur :: suff) (h : UnitInversesInvariant p m pref.length inv) (hm : 0 < m) (hc : cur % p = 0) : UnitInversesInvariant p m (pref ++ [cur]).length (inv.push 0)

The step of the loop of Ratpoints.Sieve.unitInverses at a residue divisible by p, whose entry is 0.

theorem Ratpoints.Sieve.UnitInversesInvariant.push {p m cur r : ℕ} {pref suff : List ℕ} {inv : Array ℕ} (hl : ForIn.toList [1:m] = pref ++ cur :: suff) (h : UnitInversesInvariant p m pref.length inv) (hr : r < m ∧ cur * r % m = 1) : UnitInversesInvariant p m (pref ++ [cur]).length (inv.push r)

The step of the loop of Ratpoints.Sieve.unitInverses at a residue whose entry r is its inverse modulo m, as Ratpoints.Sieve.modinv gives it for a residue not divisible by p.

theorem Ratpoints.Sieve.UnitInversesInvariant.post {p m : ℕ} {inv : Array ℕ} (h : UnitInversesInvariant p m (ForIn.toList [1:m]).length inv) (hm : 0 < m) (x : ℕ) : inv[x]! < m ∧ (x < m → x % p ≠ 0 → x * inv[x]! % m = 1)

At the end of the loop of Ratpoints.Sieve.unitInverses, for m > 0: every entry of the inverses is below m, and that of a residue not divisible by p is its inverse modulo m.

theorem Ratpoints.Sieve.unitInverses_spec (p e : ℕ) : ⦃ Nat.Prime p ∧ 1 ≤ e ⦄ unitInverses p (p ^ e) ⦃ fun (inv : Array ℕ) => ∀ (x : ℕ), inv[x]! < p ^ e ∧ (x < p ^ e → x % p ≠ 0 → x * inv[x]! % p ^ e = 1) ⦄

The contract of Ratpoints.Sieve.unitInverses for a prime p and e ≥ 1: the inverses of the prime power p ^ e are below p ^ e, and that of a unit is its inverse modulo p ^ e, by the extended Euclidean algorithm (Ratpoints.Sieve.modinv_spec).

def Ratpoints.Sieve.FsqInvariant (c : List ℤ) (d m : ℕ) (pref : List ℕ) (fsq : Array UInt64) : Prop

The invariant of the loop of Ratpoints.Sieve.examinePower over the residues that sets the bits of fsq, after the residues pref, on the bit array: Ratpoints.modWords words, the bit of each residue x of pref at which f takes a square value modulo m set.

Equations

• Ratpoints.Sieve.FsqInvariant c d m pref fsq = (fsq.size = Ratpoints.modWords ∧ ∀ x ∈ pref, IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑x ^ k) → Ratpoints.Sieve.bitAt fsq x = true)

def Ratpoints.Sieve.GsqInvariant (c : List ℤ) (d p m : ℕ) : Std.WP.WhileInvariant (Array UInt64 × ℕ) Prop

The invariant of the loop of Ratpoints.Sieve.examinePower over the multiples t of p that sets the bits of gsq, on the bit array and the multiple: Ratpoints.modWords words, t a multiple of p, the bit of each multiple of p below t at which the reversed polynomial of the even degree D = d + d % 2 takes a square value modulo m set, and t ≥ m at the exit.

Equations

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

theorem Ratpoints.Sieve.fsqInvariant_nil (c : List ℤ) (d m : ℕ) {sq fsq gsq : Array UInt64} (h : (sq, fsq, gsq) = (Array.replicate modWords 0, Array.replicate modWords 0, Array.replicate modWords 0)) : FsqInvariant c d m [] fsq

theorem Ratpoints.Sieve.gsqInvariant_zero (c : List ℤ) (d p m : ℕ) {sq fsq gsq : Array UInt64} (h : (sq, fsq, gsq) = (Array.replicate modWords 0, Array.replicate modWords 0, Array.replicate modWords 0)) : GsqInvariant c d p m false (gsq, 0)

theorem Ratpoints.Sieve.FsqInvariant.push {c : List ℤ} {d p e cur : ℕ} {pref : List ℕ} {sq fsq : Array UInt64} (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) (hsq : sq.size = modWords ∧ ∀ x < p ^ e, bitAt sq (x * x % p ^ e) = true) (h : FsqInvariant c d (p ^ e) pref fsq) (hb : bitAt sq (evalMod (List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1))) (p ^ e) cur) = true → bitAt fsq cur = true) : FsqInvariant c d (p ^ e) (pref ++ [cur]) fsq

The step of the loop that sets the bits of fsq at the residue cur, its bit set when f(cur) is a square modulo m, read from the bits of the squares.

theorem Ratpoints.Sieve.FsqInvariant.push_setBitAt {c : List ℤ} {d p e cur : ℕ} {pref suff : List ℕ} {sq fsq : Array UInt64} (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) (hsq : sq.size = modWords ∧ ∀ x < p ^ e, bitAt sq (x * x % p ^ e) = true) (hl : ForIn.toList [:p ^ e] = pref ++ cur :: suff) (h : FsqInvariant c d (p ^ e) pref fsq) : bitAt sq (evalMod (List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1))) (p ^ e) cur) = true → FsqInvariant c d (p ^ e) (pref ++ [cur]) (setBitAt fsq cur)

theorem Ratpoints.Sieve.FsqInvariant.push_of_not {c : List ℤ} {d p e cur : ℕ} {pref : List ℕ} {sq fsq : Array UInt64} (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) (hsq : sq.size = modWords ∧ ∀ x < p ^ e, bitAt sq (x * x % p ^ e) = true) (h : FsqInvariant c d (p ^ e) pref fsq) (hb : ¬bitAt sq (evalMod (List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1))) (p ^ e) cur) = true) : FsqInvariant c d (p ^ e) (pref ++ [cur]) fsq

theorem Ratpoints.Sieve.GsqInvariant.push {c : List ℤ} {d p e t : ℕ} {sq gsq gsq' : Array UInt64} (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) (hsq : sq.size = modWords ∧ ∀ x < p ^ e, bitAt sq (x * x % p ^ e) = true) (ht : t < p ^ e) (h : GsqInvariant c d p (p ^ e) false (gsq, t)) (hs : gsq'.size = modWords) (hold : ∀ t' < t, bitAt gsq t' = true → bitAt gsq' t' = true) (hb : bitAt sq (evalMod (if d % 2 = 1 then List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1)) ++ [0] else List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1))).reverse (p ^ e) t) = true → bitAt gsq' t = true) : p ^ e - (t + p) < p ^ e - t ∧ GsqInvariant c d p (p ^ e) false (gsq', t + p)

The step of the loop that sets the bits of gsq at the multiple t < m of p, its bit set when the reversed polynomial takes a square value modulo m at t, read from the bits of the squares, with the measure m - t.

theorem Ratpoints.Sieve.GsqInvariant.push_setBitAt {c : List ℤ} {d p e t mb : ℕ} {sq gsq : Array UInt64} (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) (hsq : sq.size = modWords ∧ ∀ x < p ^ e, bitAt sq (x * x % p ^ e) = true) (ht : t < p ^ e) (h : p ^ e - t = mb ∧ GsqInvariant c d p (p ^ e) false (gsq, t)) : bitAt sq (evalMod (if d % 2 = 1 then List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1)) ++ [0] else List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1))).reverse (p ^ e) t) = true → p ^ e - (t + p) < mb ∧ GsqInvariant c d p (p ^ e) false (setBitAt gsq t, t + p)

theorem Ratpoints.Sieve.GsqInvariant.push_of_not {c : List ℤ} {d p e t mb : ℕ} {sq gsq : Array UInt64} (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) (hsq : sq.size = modWords ∧ ∀ x < p ^ e, bitAt sq (x * x % p ^ e) = true) (ht : t < p ^ e) (h : p ^ e - t = mb ∧ GsqInvariant c d p (p ^ e) false (gsq, t)) (hb : ¬bitAt sq (evalMod (if d % 2 = 1 then List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1)) ++ [0] else List.map (fun (k : ℕ) => (c.getD k 0 % ↑(p ^ e)).toNat) (List.range (d + 1))).reverse (p ^ e) t) = true) : p ^ e - (t + p) < mb ∧ GsqInvariant c d p (p ^ e) false (gsq, t + p)

theorem Ratpoints.Sieve.GsqInvariant.exit {c : List ℤ} {d p m t mb : ℕ} {gsq : Array UInt64} (ht : ¬t < m) (h : m - t = mb ∧ GsqInvariant c d p m false (gsq, t)) : GsqInvariant c d p m true (gsq, t)

theorem Ratpoints.Sieve.setSquareBits_pre {sq fsq gsq : Array UInt64} {p e : ℕ} (h : (sq, fsq, gsq) = (Array.replicate modWords 0, Array.replicate modWords 0, Array.replicate modWords 0)) (pre : Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords) : sq.size = modWords ∧ p ^ e ≤ 64 * modWords

The precondition of Ratpoints.Sieve.setSquareBits in Ratpoints.Sieve.examinePower.

theorem Ratpoints.Sieve.examinePower_post {c : List ℤ} {d p m : ℕ} {fsq gsq : Array UInt64} {t : ℕ} {inv : Array ℕ} (hinv : ∀ (x : ℕ), inv[x]! < m ∧ (x < m → x % p ≠ 0 → x * inv[x]! % m = 1)) (hf : FsqInvariant c d m (ForIn.toList [:m]) fsq) (hg : GsqInvariant c d p m true (gsq, t)) : (∀ (x : ℕ), inv[x]! < m ∧ (x < m → x % p ≠ 0 → x * inv[x]! % m = 1)) ∧ (∀ x < m, IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑x ^ k) → bitAt fsq x = true) ∧ ∀ t' < m, t' % p = 0 → IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑t' ^ (d + d % 2 - k)) → bitAt gsq t' = true

The end of Ratpoints.Sieve.examinePower: the inverses of the units, and the bits of fsq and gsq of the residues and the multiples of p at which the polynomial and the reversed polynomial take square values modulo m.

theorem Ratpoints.Sieve.examinePower_spec (c : List ℤ) (d p e : ℕ) (u pinf : Bool) : ⦃ Nat.Prime p ∧ 1 ≤ e ∧ p ^ e ≤ 64 * modWords ⦄ examinePower c d p e u pinf ⦃ fun (pw : Power) => (∀ (x : ℕ), pw.inv[x]! < p ^ e ∧ (x < p ^ e → x % p ≠ 0 → x * pw.inv[x]! % p ^ e = 1)) ∧ (∀ x < p ^ e, IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑x ^ k) → bitAt pw.fsq x = true) ∧ ∀ t < p ^ e, t % p = 0 → IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑t ^ (d + d % 2 - k)) → bitAt pw.gsq t = true ⦄

The contract of Ratpoints.Sieve.examinePower for a prime p, e ≥ 1 and p ^ e within the words of its bit arrays: the inverses of the prime power p ^ e are below p ^ e, and that of a unit is its inverse modulo p ^ e (Ratpoints.Sieve.unitInverses_spec); bit x of fsq is set when f(x) is a square modulo p ^ e, and bit t of gsq, for p ∣ t, when the reversed polynomial of the even degree D = d + d % 2 takes a square value at t, read from the bits of the squares (Ratpoints.Sieve.setSquareBits_spec).

theorem Ratpoints.Sieve.getElem!_inv_run_examinePower_lt {c : List ℤ} {d p e : ℕ} (u pinf : Bool) (hp : Nat.Prime p) (he : 1 ≤ e) (x : ℕ) : (examinePower c d p e u pinf).run.inv[x]! < p ^ e

theorem Ratpoints.Sieve.mul_getElem!_inv_run_examinePower_mod {c : List ℤ} {d p e : ℕ} (u pinf : Bool) (hp : Nat.Prime p) (he : 1 ≤ e) {x : ℕ} (hx : x < p ^ e) (hpx : x % p ≠ 0) : x * (examinePower c d p e u pinf).run.inv[x]! % p ^ e = 1

Entry x of the inverses of the prime power p ^ e, for a unit x, is its inverse modulo p ^ e, by Ratpoints.Sieve.modinv.

theorem Ratpoints.Sieve.getElem!_inv_run_examinePower_lt_two_pow_16 {c : List ℤ} {d p e : ℕ} (u pinf : Bool) (hp : Nat.Prime p) (he : 1 ≤ e) (hm : p ^ e < maxPrimeEven) (x : ℕ) : (examinePower c d p e u pinf).run.inv[x]! < 2 ^ 16

The range obligation of the inverses of examine_power (find_points.c:2303), which it casts to the unsigned short entries of inv (rp-private.h:533): for a prime power p ^ e < maxPrimeEven, they are below p ^ e (Ratpoints.Sieve.getElem!_inv_run_examinePower_lt), so below 2 ^ 10 (Ratpoints.maxPrimeEven_le_two_pow_10) and below 2 ^ 16: the cast keeps them.

theorem Ratpoints.Sieve.bitAt_fsq_run_examinePower_of_isSquare {c : List ℤ} {d p e : ℕ} (u pinf : Bool) (hp : Nat.Prime p) (he : 1 ≤ e) (hm : p ^ e ≤ 64 * modWords) {x : ℕ} (hx : x < p ^ e) (h : IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑x ^ k)) : bitAt (examinePower c d p e u pinf).run.fsq x = true

Bit x of the table Ratpoints.Sieve.Power.fsq of m = p ^ e (Ratpoints.Sieve.examinePower), for m within the words of its bit arrays, is set when f(x) is a square modulo m.

theorem Ratpoints.Sieve.bitAt_gsq_run_examinePower_of_isSquare {c : List ℤ} {d p e : ℕ} (u pinf : Bool) (hp : Nat.Prime p) (he : 1 ≤ e) (hm : p ^ e ≤ 64 * modWords) {t : ℕ} (ht : t < p ^ e) (htp : t % p = 0) (h : IsSquare (∑ k ∈ Finset.range (d + 1), ↑(c.getD k 0) * ↑t ^ (d + d % 2 - k))) : bitAt (examinePower c d p e u pinf).run.gsq t = true

Bit t of the table Ratpoints.Sieve.Power.gsq of m = p ^ e (Ratpoints.Sieve.examinePower), for m within the words of its bit arrays and p ∣ t, is set when the reversed polynomial ∑ cₖ t ^ (D - k) of the even degree D = d + d % 2 takes a square value modulo m at t.

The rows of a prime power let every point through

theorem Ratpoints.Sieve.admits_run_examinePower_of_sq_eq {c : List ℤ} {p e : ℕ} (u pinf : Bool) (hp : Nat.Prime p) (he : 1 ≤ e) (hm : p ^ e ≤ 64 * modWords) {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (examinePower c (degree c) p e u pinf).run.admits b a = true

The row of the denominator b for the prime power p ^ e, e ≥ 1, within the words of its bit arrays, admits the numerator a of every point (a, y, b) with gcd(a, b) = 1: for p ∤ b, since f(a / b) is a square modulo p ^ e, and for p ∣ b, since p ∤ a and the reversed polynomial takes a square value at b / a (Ratpoints.isSquare_sum_mul_pow_sub_of_sq_eq_binaryForm).

The sieve entry of a modulus

structure Ratpoints.Sieve.Factor.IsSound (c : List ℤ) (m : ℕ) (f : Factor) : Prop

A factor that the choice of the moduli makes for the modulus m of the curve y ^ 2 = F(x, z) with the coefficient list c (Ratpoints.makeModulus, Ratpoints.primeEntry): it admits every point (a, y, b) with gcd(a, b) = 1 at the residues of b and a modulo m, its tables of inverses serve the scaling of the rows by a unit modulo m (Ratpoints.Sieve.Factor.HasInverses), its builder has what it needs (Ratpoints.Sieve.Factor.Buildable), and its table or tables are those that Ratpoints.Sieve.examinePrime computes for a prime and Ratpoints.Sieve.examinePower on the path of GMP integers for a prime power, which both paths give (Ratpoints.Sieve.examinePower_eq_examinePower_false), with either value of the flag pinf, which only the density reads.

• admits_of_sq_eq ⦃a y : ℤ⦄ ⦃b : ℕ⦄ (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : f.admits (b % m) (a % ↑m) = true

  The factor admits every point at the residues modulo m.

• hasInverses : f.HasInverses m

  The tables of inverses serve the scaling of the rows by a unit modulo m.

• buildable : f.Buildable

  The builder of the rows has what it needs.

• prime_eq (t : Entry) (h : f = prime t) : t = examinePrime c (degree c) t.p

  A prime has the table that Ratpoints.Sieve.examinePrime computes.

• power_eq (pw : Power) (h : f = power pw) : ∃ (pinf : Bool), pw = (examinePower c (degree c) pw.p pw.e false pinf).run

  A prime power has the tables that Ratpoints.Sieve.examinePower computes.

theorem Ratpoints.Sieve.Factor.IsSound.inverses_eq {c : List ℤ} {m : ℕ} {f : Factor} (hf : IsSound c m f) {t : Entry} (h : f = prime t) : t.inverses = inversesMod t.p

A prime factor has the inverses that Ratpoints.Sieve.inversesMod computes.

theorem Ratpoints.Sieve.mod_sixty_four_ne_zero_of_prime {p : ℕ} (hp : Nat.Prime p) : p % 64 ≠ 0

A prime is no multiple of 64, as CODE_INIT_SIEVE2 needs of a prime above 64.

theorem Ratpoints.Sieve.isSound_prime_examinePrime {c : List ℤ} {m pn : ℕ} (hpn : pn < numPrimes) (hd : primeTable[pn]! ∣ m) : Factor.IsSound c m (Factor.prime (examinePrime c (degree c) primeTable[pn]!))

The factor of a prime p = primeTable[pn] of the table that divides m, with its table.

theorem Ratpoints.Sieve.isSound_power_run_examinePower {c : List ℤ} {m pn e : ℕ} (u pinf : Bool) (hm0 : 0 < m) (hm : m < maxPrimeEven) (hpn : pn < numPrimes) (he : 1 ≤ e) (hd : primeTable[pn]! ^ e ∣ m) : Factor.IsSound c m (Factor.power (examinePower c (degree c) primeTable[pn]! e u pinf).run)

The factor of a prime power primeTable[pn] ^ e, e ≥ 1, of the table that divides a modulus 0 < m < maxPrimeEven, with its tables, for either path of the reduction and either value of the flag pinf.

structure Ratpoints.IsModulusEntry (c : List ℤ) (m : ℕ) (s : Sieve.SieveEntry) : Prop

What the choice of the moduli makes of the sieve entry s of the modulus m for the curve with the coefficient list c (Ratpoints.makeModulus, Ratpoints.primeEntry): its modulus is m, its factors are sound for m (Ratpoints.Sieve.Factor.IsSound) and their moduli multiply to m, and it has the fields that the packing reads (Ratpoints.Sieve.SieveEntry.Packable); so it admits every point (Ratpoints.IsModulusEntry.admits_of_sq_eq) and fits the rows of the references of the run (Ratpoints.IsModulusEntry.rowsFit_runRows).

• p_eq : s.p = m

  The modulus is m.

• isSound_of_mem (f : Sieve.Factor) : f ∈ s.factors → Sieve.Factor.IsSound c m f

  The factors are sound for m.

• packable : s.Packable

  The entry has the fields that the packing reads.

• prod_modulus : (List.map Sieve.Factor.modulus s.factors).prod = m

  The moduli of the factors multiply to m.

theorem Ratpoints.IsModulusEntry.admits_of_sq_eq {c : List ℤ} {m : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) ⦃a y : ℤ⦄ ⦃b : ℕ⦄ (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : s.admits b a = true

The sieve entry of m as the choice makes it admits every point (a, y, b) with gcd(a, b) = 1, since its factors admit it at the residues modulo m.

theorem Ratpoints.IsModulusEntry.hasInverses {c : List ℤ} {m : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) (f : Sieve.Factor) : f ∈ s.factors → f.HasInverses m

theorem Ratpoints.IsModulusEntry.buildable {c : List ℤ} {m : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) (f : Sieve.Factor) : f ∈ s.factors → f.Buildable

theorem Ratpoints.isModulusEntry_of_forall_isSound {c : List ℤ} {m : ℕ} {factors : List Sieve.Factor} {x : ℕ} (hm : 1 < m ∧ m < maxPrimeEven ∧ m % 2 = 1) (hs : ∀ f ∈ factors, Sieve.Factor.IsSound c m f) (hp : (List.map Sieve.Factor.modulus factors).prod = m) (hx : x * rbaLength % m = 1 ∧ x < m) (ref : Sieve.EntryRef) (init : Sieve.RowInit) (r : Float) (nf : ℤ) : IsModulusEntry c m { p := m, factors := factors, magic := Sieve.magic m, bias := m * ((rowBias + m - 1) / m), rbainv := x, dinv := #[], ref := ref, init := init, r := r, nf := nf }

The sieve entry of an odd modulus 1 < m < maxPrimeEven with factors that are sound for m and whose moduli multiply to m, the reciprocal and the bias of m, an inverse x < m of Ratpoints.rbaLength modulo m and any reference, kind of builder, density and count of factors is an entry of m as the choice makes it.

theorem Ratpoints.coprime_rbaLength_of_mod_two_eq_one {m : ℕ} (hm : m % 2 = 1) : rbaLength.Coprime m

Ratpoints.rbaLength, a power of 2 (Ratpoints.rbaLength_eq_two_pow_rbaShift), is prime to every odd modulus.

theorem Ratpoints.rbaLength_mul_lt_two_pow_64 {m : ℕ} (hm : m ≤ 2 ^ 32) : rbaLength * m < 2 ^ 64

The product of Ratpoints.rbaLength < 2 ^ 32 (Ratpoints.rbaShift_lt_thirty_two) and a modulus m ≤ 2 ^ 32 is below 2 ^ 64, so that the remainder of Ratpoints.rbaLength by the reciprocal of m is exact.

theorem Ratpoints.inverses_mulMod_rbaLength_of_isSound {c : List ℤ} {m : ℕ} {t : Sieve.Entry} (hm : 1 < m ∧ m < maxPrimeEven ∧ m % 2 = 1) (hs : Sieve.Factor.IsSound c m (Sieve.Factor.prime t)) (hp : t.p = m) : t.inverses[Sieve.mulMod rbaLength m (Sieve.magic m)]! * rbaLength % m = 1 ∧ t.inverses[Sieve.mulMod rbaLength m (Sieve.magic m)]! < m

The inverse of Ratpoints.rbaLength modulo an odd prime modulus 1 < m < maxPrimeEven, read from its table, sound for m, with the remainder of rbaLength by the reciprocal of m, as examine_prime reads it.

theorem Ratpoints.one_lt_and_coprime_rbaLength_mod {m : ℕ} (hm : 1 < m) (hm2 : m % 2 = 1) : 1 < m ∧ (rbaLength % m).Coprime m

The precondition of Ratpoints.Sieve.modinv for the inverse of Ratpoints.rbaLength modulo an odd modulus m > 1.

theorem Ratpoints.mul_rbaLength_mod_and_lt {m r : ℕ} (h : r < m ∧ rbaLength % m * r % m = 1) : r * rbaLength % m = 1 ∧ r < m

The inverse of Ratpoints.rbaLength that Ratpoints.Sieve.modinv gives, in the form of Ratpoints.Sieve.SieveEntry.Packable.

theorem Ratpoints.IsModulusEntry.factors_ne_nil {c : List ℤ} {m : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) : s.factors ≠ []

The factors of the sieve entry of m as the choice makes it are not empty, since their moduli multiply to m > 1.

theorem Ratpoints.IsModulusEntry.p_eq_modulus {c : List ℤ} {m : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) {f : Sieve.Factor} (hf : s.factors = [f]) : s.p = f.modulus

A sieve entry with one factor as the choice makes it has the modulus of its factor.

theorem Ratpoints.IsModulusEntry.rowsFit_runRows {c : List ℤ} {m n : ℕ} {s : Sieve.SieveEntry} (h : IsModulusEntry c m s) (href : (s.ref, s.init) = Sieve.SieveEntry.refInit n s.factors) {es : List Sieve.SieveEntry} (hn : es[n]? = some s) : s.RowsFit (Sieve.runRows c (degree c) es) n

The sieve entry of m that the choice makes at the position n of the entries es of a run fits the rows of the references of the run (Ratpoints.Sieve.runRows): its reference and kind of builder are those of Ratpoints.Sieve.SieveEntry.refInit, its factors have what their builders need and the tables that Ratpoints.Sieve.examinePrime and Ratpoints.Sieve.examinePower compute.