The marks of the denominators of the fast search

The fast search finds its denominators by marks in byte arrays (Ratpoints.Fast.denominators), and Ratpoints.Fast.collectMarked lists the marked ones in ascending order (Ratpoints.Fast.collectMarked_eq_filter). For even degree, Ratpoints.Fast.forbiddenDens marks only multiples of an odd q with J(c_d | q) = -1 (Ratpoints.Fast.exists_dvd_of_getElem!_forbiddenDens_ne_zero): it marks the multiples of p when Ratpoints.Fast.jacobiNat gives -1, which it gives only for J(c_d | p) = -1 (Ratpoints.Fast.jacobiNatAux_eq_zero_or_eq, Ratpoints.Fast.jacobiNat_eq_zero_or_eq); that p is a prime, as the sieve of Eratosthenes makes it, is not needed. For odd degree, Ratpoints.Fast.squareDens n hi marks every s k ^ 2 ≤ hi with s dividing n ≠ 0 and k ≥ 1 (Ratpoints.Fast.getElem!_squareDens).

Main statements

• Ratpoints.Fast.collectMarked_eq_filter: the marked numbers in ascending order.
• Ratpoints.Fast.exists_dvd_of_getElem!_forbiddenDens_ne_zero: what a mark of Ratpoints.Fast.forbiddenDens means.
• Ratpoints.Fast.getElem!_squareDens: the marks of Ratpoints.Fast.squareDens.

Marked numbers

theorem Ratpoints.Fast.collectMarked_eq_filter (m : ByteArray) (v : UInt8) {lo : ℕ} (hlo : 1 ≤ lo) (n : ℕ) (acc : List ℕ) : collectMarked m v lo n acc = List.filter (fun (x : ℕ) => m[x]! == v) (List.range' lo (n + 1 - lo)) ++ acc

theorem Ratpoints.Fast.collectMarked_sublist (m : ByteArray) (v : UInt8) {lo : ℕ} (hlo : 1 ≤ lo) (n : ℕ) : (collectMarked m v lo n []).Sublist (List.range' lo (n + 1 - lo))

theorem Ratpoints.Fast.mem_collectMarked_iff {m : ByteArray} {v : UInt8} {lo : ℕ} (hlo : 1 ≤ lo) {n b : ℕ} : b ∈ collectMarked m v lo n [] ↔ b ∈ List.range' lo (n + 1 - lo) ∧ m[b]! = v

theorem Ratpoints.Fast.of_getElem!_markMultiples {a : ByteArray} {n j hi b : ℕ} (h : (markMultiples a n j hi)[b]! ≠ 0) : a[b]! ≠ 0 ∨ ∃ (k : ℕ), b = j + n * k

The Jacobi symbol

theorem Ratpoints.Fast.ite_mul_jacobiSym_div_two {a n : ℕ} (ha : a % 2 = 0) (hn : n % 2 = 1) (s : ℤ) : (if (n % 8 == 3 || n % 8 == 5) = true then -s else s) * jacobiSym (↑(a / 2)) n = s * jacobiSym (↑a) n

Halving an even a against an odd n multiplies the symbol by (2 / n).

theorem Ratpoints.Fast.ite_mul_jacobiSym_mod {a n : ℕ} (ha : a % 2 = 1) (hn : n % 2 = 1) (s : ℤ) : (if (a % 4 == 3 && n % 4 == 3) = true then -s else s) * jacobiSym (↑(n % a)) a = s * jacobiSym (↑a) n

Exchanging the odd a and n, with n reduced modulo a, multiplies the symbol by the sign of the reciprocity.

theorem Ratpoints.Fast.jacobiNatAux_eq_zero_or_eq (fuel a : ℕ) {n : ℕ} (hn : n % 2 = 1) (s : ℤ) : jacobiNatAux fuel a n s = 0 ∨ jacobiNatAux fuel a n s = s * jacobiSym (↑a) n

Ratpoints.Fast.jacobiNatAux computes s J(a | n) for odd n, or gives up with 0.

theorem Ratpoints.Fast.jacobiNat_eq_zero_or_eq (a : ℕ) {n : ℕ} (hn : n % 2 = 1) : jacobiNat a n = 0 ∨ jacobiNat a n = jacobiSym (↑a) n

theorem Ratpoints.Fast.jacobiSym_eq_neg_one_of_jacobiNat_eq_neg_one {a n : ℕ} (hn : n % 2 = 1) (h : jacobiNat a n = -1) : jacobiSym (↑a) n = -1

theorem Ratpoints.Fast.jacobiSym_toNat_emod (a : ℤ) {n : ℕ} (hn : n ≠ 0) : jacobiSym (↑(a % ↑n).toNat) n = jacobiSym a n

The denominators of even degree

theorem Ratpoints.Fast.exists_dvd_of_getElem!_forbiddenDensFrom_ne_zero {lc : ℤ} {hi : ℕ} {comp forb : ByteArray} {p : ℕ} (hp : p % 2 = 1) (hforb : ∀ (b : ℕ), forb[b]! ≠ 0 → ∃ (q : ℕ), q % 2 = 1 ∧ q ∣ b ∧ jacobiSym lc q = -1) {b : ℕ} (h : (forbiddenDensFrom lc hi comp forb p)[b]! ≠ 0) : ∃ (q : ℕ), q % 2 = 1 ∧ q ∣ b ∧ jacobiSym lc q = -1

The invariant of the loop of Ratpoints.Fast.forbiddenDensFrom: every marked denominator is a multiple of an odd q with J(lc | q) = -1; that q is a prime, as the sieve of Eratosthenes makes it, is not needed.

theorem Ratpoints.Fast.exists_dvd_of_getElem!_forbiddenDens_ne_zero {lc : ℤ} {hi b : ℕ} (h : (forbiddenDens lc hi)[b]! ≠ 0) : ∃ (q : ℕ), q % 2 = 1 ∧ q ∣ b ∧ jacobiSym lc q = -1

The denominators of odd degree

theorem Ratpoints.Fast.size_markSquares (a : ByteArray) (s k hi : ℕ) : (markSquares a s k hi).size = a.size

theorem Ratpoints.Fast.getElem!_markSquares {a : ByteArray} {s k hi b : ℕ} (hb : b < a.size) (h : a[b]! = 1 ∨ ∃ k₀ ≥ k, k₀ ≤ hi ∧ b = s * k₀ * k₀ ∧ b ≤ hi) : (markSquares a s k hi)[b]! = 1

Ratpoints.Fast.markSquares keeps the marks of a and marks s k₀ ^ 2 ≤ hi for k ≤ k₀.

theorem Ratpoints.Fast.getElem!_foldl_markSquares {n hi b : ℕ} (l : List ℕ) {a : ByteArray} (hb : b < a.size) (h : a[b]! = 1 ∨ ∃ s ∈ l, n % s = 0 ∧ ∃ k ≥ 1, k ≤ hi ∧ b = s * k * k ∧ b ≤ hi) : (List.foldl (fun (a : ByteArray) (s : ℕ) => if (n % s == 0) = true then markSquares a s 1 hi else a) a l)[b]! = 1

theorem Ratpoints.Fast.getElem!_squareDens {n hi s k : ℕ} (hn : n ≠ 0) (hs : s ∣ n) (hk : 1 ≤ k) (hb : s * k * k ≤ hi) : (squareDens n hi)[s * k * k]! = 1