The fast search finds exactly the points

Ratpoints.Fast.fastPoints c H bLow bHigh tu lists only normalized points of height at most H on y ^ 2 = F(x, z) whose denominator is 0 or lies in the range of bLow and bHigh (Ratpoints.Fast.isPoint_and_inRegion_of_mem_fastPoints), each once (Ratpoints.Fast.nodup_fastPoints), and, assuming Sturm's theorem, all of them (Ratpoints.Fast.mem_fastPoints_of_isPoint, Ratpoints.Fast.mem_fastPoints_iff), for every setting tu of its parameters.

The sieve is a sound filter: a point (a, y, b) makes (a, b) a candidate (Ratpoints.Fast.IsCandidate), and the residues of a candidate modulo every m pass the table Ratpoints.Fast.admitTable (Ratpoints.Fast.admitTable_spec; a row prime to m is row 1 permuted, Ratpoints.Fast.getElem!_admitTable, Ratpoints.Fast.getElem!_permRow), so the bit of a survives in the row of every family (Ratpoints.Fast.Family.IsSound, Ratpoints.Fast.mkFamily_isSound), in that row shifted to the start of each chunk and moved to the part of the chunk that is searched (Ratpoints.Fast.Family.IsSound.testBit_shiftRight) and in the sieve (Ratpoints.Fast.testBit_sieve); Ratpoints.Fast.setBits lists the bits that survive (Ratpoints.Fast.mem_setBits), and the exact check of Ratpoints.BruteForce.pointsOfDen keeps the points among them. The slots, the chunks of the classes modulo G, cover each numerator once (Ratpoints.Fast.exists_mem_slots, Ratpoints.Fast.pairwise_slots), and the part of a chunk holds the numerators of the chunk within the bounds of the region (Ratpoints.Fast.exists_part_eq_some, Ratpoints.Fast.add_le_and_dvd_of_part_eq_some), so the search of a part (Ratpoints.Fast.of_mem_partPoints, Ratpoints.Fast.mem_partPoints), of a denominator (Ratpoints.Fast.of_mem_denPoints, Ratpoints.Fast.mem_denPoints_of, Ratpoints.Fast.nodup_denPoints) and the whole search list the points of its denominators with their numerators within the bounds, each once (Ratpoints.Fast.of_mem_search, Ratpoints.Fast.mem_search_of, Ratpoints.Fast.nodup_search); a denominator for which a family has the row 0 carries no candidate (Ratpoints.Fast.any_rows_eq_false).

Assuming Sturm's theorem, the bounds of the region hold the numerator a of every point (Ratpoints.Fast.exists_bounds_region): one of the intervals that the Sturm step keeps holds a / b (Ratpoints.Fast.exists_mem_sturmIntervals, from Ratpoints.Sturm.covers_computeSturm), and the bounds that Ratpoints.Fast.endFrac makes of the ends of the interval (Ratpoints.Fast.div_le_of_endFrac_eq_some, Ratpoints.Fast.le_div_of_endFrac_eq_some) bound a (Ratpoints.Fast.fst_numRange_le, Ratpoints.Fast.le_snd_numRange, Ratpoints.Fast.exists_bounds_of_mem). The denominators that the search leaves out carry no point (Ratpoints.Fast.mem_denominators_of_isCandidate): for odd degree it takes those of the form s k ^ 2 with s dividing the leading coefficient, which Ratpoints.Fast.squareDens marks (Ratpoints.Fast.getElem!_squareDens_of_isCandidate, from Ratpoints.exists_eq_mul_mul_of_sq_eq_binaryForm_of_odd), and for even degree it leaves out those that Ratpoints.Fast.forbiddenDens marks, multiples of an odd q with J(c_d | q) = -1 (Ratpoints.Fast.exists_dvd_of_getElem!_forbiddenDens_ne_zero), while the symbol is 1 on every divisor of the denominator of a point prime to c_d (Ratpoints.Sieve.jacobiSym_eq_one_of_sq_eq_binaryForm, Ratpoints.Fast.getElem!_forbiddenDens_eq_zero).

When no range of the denominators is given, Ratpoints.Fast.fastPoints runs Ratpoints.Fast.sievePoints on the coefficients that Ratpoints.Fast.reversed hands on: when it reverses them, the region is the whole box and the binary form is that of c with x and z exchanged (Ratpoints.Fast.isFullBox_and_binaryForm_eq_of_reversed_eq), so that Ratpoints.Sieve.swapPoint maps the points of the reversed list one to one onto those of c (Ratpoints.Sieve.isPoint_swapPoint, Ratpoints.Sieve.swapPoint_inj), which all lie in the whole box (Ratpoints.IsNormalizedPair.inRegion_of_isFullBox).

Main statements

• Ratpoints.Fast.isPoint_and_inRegion_of_mem_fastPoints: the list holds only points of the region.
• Ratpoints.Fast.mem_fastPoints_iff: assuming Sturm's theorem, it holds exactly the points of the region.
• Ratpoints.Fast.nodup_fastPoints: each of them once.

The positions of the bits

theorem Ratpoints.Fast.testBit_iff_eq_log2_or {n t : ℕ} (h : n ≠ 0) : n.testBit t = true ↔ t = n.log2 ∨ (n - 2 ^ n.log2).testBit t = true

The bits of a positive number are its highest bit, at Nat.log2 n, and the bits of the rest.

theorem Ratpoints.Fast.mem_setBitsSmall {n t : ℕ} : t ∈ setBitsSmall n ↔ n.testBit t = true

theorem Ratpoints.Fast.nodup_setBitsSmall (n : ℕ) : (setBitsSmall n).Nodup

theorem Ratpoints.Fast.or_testBit_iff {o h n t : ℕ} : o + h ≤ t ∧ n.testBit (h + (t - (o + h))) = true ∨ o ≤ t ∧ t - o < h ∧ n.testBit (t - o) = true ↔ o ≤ t ∧ n.testBit (t - o) = true

theorem Ratpoints.Fast.mem_setBitsAux {o n k t : ℕ} : t ∈ setBitsAux o n k ↔ o ≤ t ∧ n.testBit (t - o) = true

theorem Ratpoints.Fast.nodup_setBitsAux (o n k : ℕ) : (setBitsAux o n k).Nodup

theorem Ratpoints.Fast.mem_setBits {n t : ℕ} : t ∈ setBits n ↔ n.testBit t = true

theorem Ratpoints.Fast.nodup_setBits (n : ℕ) : (setBits n).Nodup

The residues that allow a point

def Ratpoints.Fast.IsCandidate (c : List ℤ) (a : ℤ) (b : ℕ) : Prop

(a, b) can carry a point: gcd(a, b) = 1 and F(a, b) is a square.

Equations

• Ratpoints.Fast.IsCandidate c a b = (a.gcd ↑b = 1 ∧ ∃ (y : ℤ), y ^ 2 = Ratpoints.binaryForm c a ↑b)

theorem Ratpoints.Fast.hornerMod_modEq {m : ℕ} {w w' : List ℤ} (hw : List.Forall₂ (↑m).ModEq w w') {x x' : ℤ} (hx : x ≡ x' [ZMOD ↑m]) : hornerMod w x m ≡ BruteForce.horner w' x' [ZMOD ↑m]

theorem Ratpoints.Fast.powMod_eq (r m e : ℕ) : powMod r m e = r ^ e % m

theorem Ratpoints.Fast.forall₂_scaledCoeffsMod (c : List ℤ) (d m r : ℕ) : List.Forall₂ (↑m).ModEq (scaledCoeffsMod c d m r) (BruteForce.scaledCoeffs c d ↑r)

theorem Ratpoints.Fast.hornerMod_scaledCoeffsMod_modEq (c : List ℤ) (m r x : ℕ) : (hornerMod (scaledCoeffsMod c (BruteForce.degree c) m r) (↑x) m * if BruteForce.degree c % 2 = 1 then ↑r else 1) ≡ binaryForm c ↑x ↑r [ZMOD ↑m]

theorem Ratpoints.Fast.binaryForm_modEq (c : List ℤ) {m : ℕ} {a a' b b' : ℤ} (ha : a ≡ a' [ZMOD ↑m]) (hb : b ≡ b' [ZMOD ↑m]) : binaryForm c a b ≡ binaryForm c a' b' [ZMOD ↑m]

theorem Ratpoints.Fast.binaryForm_mul_self (c : List ℤ) (u b : ℤ) : binaryForm c (u * b) b = b ^ (degree c + degree c % 2) * binaryForm c u 1

The binary form is homogeneous of degree D = d + d % 2.

theorem Ratpoints.Fast.sqTable_sq {m : ℕ} (hm : 0 < m) (y : ℤ) : (sqTable m)[(y ^ 2 % ↑m).toNat]! = true

theorem Ratpoints.Fast.natGcd_eq (a b : ℕ) : natGcd a b = a.gcd b

theorem Ratpoints.Fast.coprimeWith_of_gcd_eq_one {a : ℤ} {b m : ℕ} (hm : 0 < m) (hab : a.gcd ↑b = 1) : coprimeWith ((b % m).gcd m) (a % ↑m).toNat = true

theorem Ratpoints.Fast.getElem!_map_range {α : Type u_1} [Inhabited α] (f : ℕ → α) {n i : ℕ} (hi : i < n) : (Array.map f (List.range n).toArray)[i]! = f i

theorem Ratpoints.Fast.sqTable_of_modEq {m : ℕ} (hm : 0 < m) {v y : ℤ} (h : v ≡ y ^ 2 [ZMOD ↑m]) : (sqTable m)[(v % ↑m).toNat]! = true

theorem Ratpoints.Fast.getElem!_admitRow {c : List ℤ} {m r x : ℕ} (hm : 0 < m) (hx : x < m) (hg : coprimeWith (r.gcd m) x = true) {y : ℤ} (hy : binaryForm c ↑x ↑r ≡ y ^ 2 [ZMOD ↑m]) : (admitRow c (BruteForce.degree c) m (sqTable m) r)[x]! = true

theorem Ratpoints.Fast.intCast_mul_modEq_one {b u m : ℕ} (h : b % m * u % m = 1 % m) : ↑b * ↑u ≡ 1 [ZMOD ↑m]

theorem Ratpoints.Fast.binaryForm_mul_modEq_sq {c : List ℤ} {m : ℕ} {a y : ℤ} {b u x : ℕ} (hy : y ^ 2 = binaryForm c a ↑b) (hxa : ↑x ≡ a [ZMOD ↑m]) (hru : b % m * u % m = 1 % m) : binaryForm c ↑(x * u % m) ↑1 ≡ (y * ↑u ^ ((degree c + degree c % 2) / 2)) ^ 2 [ZMOD ↑m]

For b u ≡ 1 modulo m, F(x u, 1) is a square modulo m for every x ≡ a with F(a, b) a square, F being homogeneous of even degree (Ratpoints.Fast.binaryForm_mul_self).

theorem Ratpoints.Fast.admitTable.go_eq_append (c : List ℤ) (d m : ℕ) (sq one : Array Bool) (inv : Array ℕ) (r : ℕ) (acc : Array (Array Bool)) : go c d m sq one inv r acc = acc ++ (List.map (fun (r : ℕ) => if (r * inv[r]! % m == 1 % m && decide (inv[r]! < m)) = true then permRow one m inv[r]! else admitRow c d m sq r) (List.range' r (m - r))).toArray

The loop of Ratpoints.Fast.admitTable appends the rows from r on to acc.

theorem Ratpoints.Fast.ite_add_lt_eq_mul_mod {m u x i : ℕ} (hi : i = x * u % m) (hu : u < m) : (if i + u < m then i + u else i + u - m) = (x + 1) * u % m

The index i = x u modulo m, stepped by u < m with one conditional subtraction, is (x + 1) u modulo m.

theorem Ratpoints.Fast.permRow.go_eq_append (one : Array Bool) {m u : ℕ} (hu : u < m) (x i : ℕ) (acc : Array Bool) (hi : i = x * u % m) : go one m u x i acc = acc ++ (List.map (fun (x : ℕ) => one[x * u % m]!) (List.range' x (m - x))).toArray

The loop of Ratpoints.Fast.permRow appends the entries from x on to acc, for the index i = x u modulo m.

theorem Ratpoints.Fast.getElem!_permRow (one : Array Bool) {m u x : ℕ} (hu : u < m) (hx : x < m) : (permRow one m u)[x]! = one[x * u % m]!

theorem Ratpoints.Fast.getElem!_admitTable (c : List ℤ) (d : ℕ) {m r : ℕ} (hr : r < m) : (admitTable c d m)[r]! = if (r * (invTable m)[r]! % m == 1 % m && decide ((invTable m)[r]! < m)) = true then permRow (admitRow c d m (sqTable m) 1) m (invTable m)[r]! else admitRow c d m (sqTable m) r

theorem Ratpoints.Fast.admitTable_spec {c : List ℤ} {m : ℕ} (hm : 0 < m) {a : ℤ} {b : ℕ} (h : IsCandidate c a b) : (admitTable c (BruteForce.degree c) m)[b % m]![(a % ↑m).toNat]! = true

Bit masks

theorem Ratpoints.Fast.testBit_foldl_pattern (f : ℕ → Bool) (l : List ℕ) (P j : ℕ) : (List.foldl (fun (P j' : ℕ) => if f j' = true then P ||| 1 <<< j' else P) P l).testBit j = (P.testBit j || decide (j ∈ l) && f j)

theorem Ratpoints.Fast.testBit_pattern (m : ℕ) (f : ℕ → Bool) (j : ℕ) : (pattern m f).testBit j = (decide (j < m) && f j)

theorem Ratpoints.Fast.testBit_repeatPattern {P m j : ℕ} (k : ℕ) (hj : j < m * 2 ^ k) (h : P.testBit (j % m) = true) : (repeatPattern P m k).testBit j = true

theorem Ratpoints.Fast.le_mul_two_pow_doublings {m : ℕ} (hm : 0 < m) (N : ℕ) : N < m * 2 ^ doublings m N

theorem Ratpoints.Fast.testBit_baseRow {T : Array (Array Bool)} {m G N r j : ℕ} (hm : 0 < m) (hj : j < N) (h : T[r]![G * j % m]! = true) : (baseRow T m G N r).testBit j = true

Families

structure Ratpoints.Fast.Family.IsSound (c : List ℤ) (G L : ℕ) (F : Family) : Prop

The family F is sound for the step G and chunks of at most L numerators: it has a row for every residue modulo F.M > 0, F.ginv inverts G modulo F.M, and the row of b has the bit j < L + 8 F.M set for every candidate (a, b) with a ≡ G j modulo F.M.

• size_eq : F.rows.size = F.M

  A row for every residue.

• pos : 0 < F.M

  The modulus is positive.

• mul_ginv : G * F.ginv % F.M = 1 % F.M

  F.ginv inverts G.

• testBit (a : ℤ) (b j : ℕ) : j < L + 8 * F.M → IsCandidate c a b → ↑F.M ∣ a - ↑G * ↑j → F.rows[b % F.M]!.testBit j = true

  The row of b keeps the bit j of every candidate (a, b) with a ≡ G j.

theorem Ratpoints.Fast.foldl_mul_fst {α : Type u_1} (ts : List (ℕ × α)) (k : ℕ) : List.foldl (fun (x1 : ℕ) (x2 : ℕ × α) => x1 * x2.1) k ts = k * (List.map (fun (x : ℕ × α) => x.1) ts).prod

theorem Ratpoints.Fast.testBit_foldl_and {α : Type u_1} (g : α → ℕ) (l : List α) {init j : ℕ} (hi : init.testBit j = true) (hl : ∀ x ∈ l, (g x).testBit j = true) : (List.foldl (fun (acc : ℕ) (x : α) => acc &&& g x) init l).testBit j = true

theorem Ratpoints.Fast.natMod_eq_toNat_of_dvd {m : ℕ} {a : ℤ} {k : ℕ} (h : ↑m ∣ a - ↑k) : k % m = (a % ↑m).toNat

theorem Ratpoints.Fast.foldl_mul_fst_pos {α : Type u_1} {ts : List (ℕ × α)} (h : ∀ t ∈ ts, 0 < t.1) : 0 < List.foldl (fun (x1 : ℕ) (x2 : ℕ × α) => x1 * x2.1) 1 ts

theorem Ratpoints.Fast.dvd_foldl_mul_fst {α : Type u_1} {ts : List (ℕ × α)} {t : ℕ × α} (ht : t ∈ ts) : t.1 ∣ List.foldl (fun (x1 : ℕ) (x2 : ℕ × α) => x1 * x2.1) 1 ts

theorem Ratpoints.Fast.testBit_baseRows {c : List ℤ} {m M G N j : ℕ} (hm : 0 < m) (hmM : m ∣ M) (hj : j < N) {a : ℤ} {b : ℕ} (hc : IsCandidate c a b) (hdvd : ↑M ∣ a - ↑G * ↑j) : (Array.map (baseRow (admitTable c (BruteForce.degree c) m) m G N) (List.range m).toArray)[b % M % m]!.testBit j = true

The rows of one modulus m ∣ M keep the bit j of every candidate (a, b) with a ≡ G j modulo M.

theorem Ratpoints.Fast.mkFamily_isSound {c : List ℤ} {G L : ℕ} {ts : List (ℕ × Array (Array Bool))} (hts : ∀ t ∈ ts, t.2 = admitTable c (BruteForce.degree c) t.1) {F : Family} (h : mkFamily G L ts = some F) : Family.IsSound c G L F

The shift

theorem Ratpoints.Fast.Family.shift_lt (F : Family) (hF : 0 < F.M) (a₀ : ℤ) : F.shift a₀ < 8 * F.M

theorem Ratpoints.Fast.Family.IsSound.dvd_sub_shift {c : List ℤ} {G L : ℕ} {F : Family} (hF : IsSound c G L F) (a₀ : ℤ) : ↑F.M ∣ a₀ - ↑G * ↑(F.shift a₀)

theorem Ratpoints.Fast.Family.IsSound.testBit_shiftRight {c : List ℤ} {G L : ℕ} {F : Family} (hF : IsSound c G L F) {a₀ : ℤ} {b o t : ℕ} (ht : o + t < L) (hc : IsCandidate c (a₀ + ↑G * (↑o + ↑t)) b) : (F.rows[b % F.M]! >>> (F.shift a₀ + o)).testBit t = true

The row of b, shifted to the chunk that starts at a₀ and moved by o, keeps the bit t of every candidate (a₀ + G (o + t), b) with o + t < L.

theorem Ratpoints.Fast.Family.IsSound.rows_ne_zero {c : List ℤ} {G L : ℕ} {F : Family} (hF : IsSound c G L F) {a : ℤ} {b : ℕ} (hc : IsCandidate c a b) : F.rows[b % F.M]! ≠ 0

The sieve

theorem Ratpoints.Fast.testBit_foldl_sieve {α : Type u_1} (g : α → ℕ) (l : List α) {mask t : ℕ} (hmask : mask.testBit t = true) (hl : ∀ x ∈ l, (g x).testBit t = true) : (List.foldl (fun (acc : ℕ) (x : α) => if (acc == 0) = true then 0 else acc &&& g x) mask l).testBit t = true

theorem Ratpoints.Fast.testBit_of_testBit_foldl_sieve {α : Type u_1} {g : α → ℕ} {l : List α} {mask t : ℕ} (h : (List.foldl (fun (acc : ℕ) (x : α) => if (acc == 0) = true then 0 else acc &&& g x) mask l).testBit t = true) : mask.testBit t = true

theorem Ratpoints.Fast.testBit_sieve {rs sh : Array ℕ} {o mask t : ℕ} (hmask : mask.testBit t = true) (h : ∀ i < rs.size, (rs[i]! >>> (sh[i]! + o)).testBit t = true) : (sieve rs sh o mask).testBit t = true

theorem Ratpoints.Fast.testBit_of_testBit_sieve {rs sh : Array ℕ} {o mask t : ℕ} (h : (sieve rs sh o mask).testBit t = true) : mask.testBit t = true

The points of a chunk

theorem Ratpoints.Fast.of_mem_chunkPoints {c : List ℤ} {G : ℕ} {rs sh : Array ℕ} {o : ℕ} {a₀ : ℤ} {len b : ℕ} {p : ℤ × ℤ × ℤ} (h : p ∈ chunkPoints c (BruteForce.degree c) G rs sh o a₀ len b) : p.2.2 = ↑b ∧ (∃ t < len, p.1 = a₀ + ↑G * ↑t) ∧ p.1.gcd p.2.2 = 1 ∧ p.2.1 ^ 2 = binaryForm c p.1 p.2.2

theorem Ratpoints.Fast.mem_chunkPoints {c : List ℤ} {G : ℕ} {rs sh : Array ℕ} {o : ℕ} {a₀ : ℤ} {len b : ℕ} (hrs : ∀ t < len, IsCandidate c (a₀ + ↑G * ↑t) b → ∀ i < rs.size, (rs[i]! >>> (sh[i]! + o)).testBit t = true) {p : ℤ × ℤ × ℤ} : p ∈ chunkPoints c (BruteForce.degree c) G rs sh o a₀ len b ↔ p.2.2 = ↑b ∧ (∃ t < len, p.1 = a₀ + ↑G * ↑t) ∧ p.1.gcd p.2.2 = 1 ∧ p.2.1 ^ 2 = binaryForm c p.1 p.2.2

theorem Ratpoints.Fast.nodup_chunkPoints (c : List ℤ) {G : ℕ} (hG : 0 < G) (rs sh : Array ℕ) (o : ℕ) (a₀ : ℤ) (len b : ℕ) : (chunkPoints c (BruteForce.degree c) G rs sh o a₀ len b).Nodup

The parts of the chunks

theorem Ratpoints.Fast.add_le_and_dvd_of_part_eq_some {G : ℕ} {lo hi a₀ : ℤ} {len t₁ len₁ : ℕ} (h : part G lo hi a₀ len = some (t₁, len₁)) : t₁ + len₁ ≤ len ∧ 64 ∣ t₁ ∧ (t₁ + len₁ = len ∨ 64 ∣ t₁ + len₁)

The part of a chunk lies in the chunk, starts at a multiple of 64 and ends at the end of the chunk or at a multiple of 64.

theorem Ratpoints.Fast.exists_part_eq_some {G : ℕ} (hG : 0 < G) {lo hi a₀ : ℤ} {len t : ℕ} (ht : t < len) (hlo : lo ≤ a₀ + ↑G * ↑t) (hhi : a₀ + ↑G * ↑t ≤ hi) : ∃ (t₁ : ℕ) (len₁ : ℕ), part G lo hi a₀ len = some (t₁, len₁) ∧ t₁ ≤ t ∧ t < t₁ + len₁

Every numerator of the chunk from lo to hi lies in the part of the chunk.

Chunks and classes

theorem Ratpoints.Fast.mem_chunks_iff {cnt L t₀ len : ℕ} : (t₀, len) ∈ chunks cnt L ↔ ∃ k < (cnt + L - 1) / L, t₀ = k * L ∧ len = min L (cnt - k * L)

theorem Ratpoints.Fast.exists_mem_chunks {cnt L u : ℕ} (hL : 0 < L) (hu : u < cnt) : ∃ (t₀ : ℕ) (len : ℕ), (t₀, len) ∈ chunks cnt L ∧ t₀ = u / L * L ∧ u % L < len

theorem Ratpoints.Fast.le_of_mem_chunks {cnt L t₀ len : ℕ} (h : (t₀, len) ∈ chunks cnt L) : t₀ + len ≤ cnt ∧ len ≤ L ∧ t₀ % L = 0

theorem Ratpoints.Fast.add_mul_lt_of_lt_classCount {n G ρ u : ℕ} (hG : 0 < G) (h : u < classCount n G ρ) : ρ + G * u < n

theorem Ratpoints.Fast.lt_classCount {n G ρ u : ℕ} (hG : 0 < G) (h : ρ + G * u < n) : u < classCount n G ρ

theorem Ratpoints.Fast.eq_sub_add_mul_of_natCast_eq {i G L H : ℕ} {x : ℤ} (hi : ↑i = x + ↑H) : x = ↑(i % G + G * (i / G / L * L)) - ↑H + ↑G * ↑(i / G % L)

The numerator x with x + H = i in the chunk of the class i % G that holds it.

theorem Ratpoints.Fast.eq_of_add_mul_eq {G ρ ρ' u u' : ℕ} (hρ : ρ < G) (hρ' : ρ' < G) (h : ρ + G * u = ρ' + G * u') : ρ = ρ' ∧ u = u'

theorem Ratpoints.Fast.eq_of_add_mul_add_eq {G L ρ k k' t t' : ℕ} (hG : 0 < G) (hL : 0 < L) (ht : t < L) (ht' : t' < L) (h : ρ + G * (k * L + t) = ρ + G * (k' * L + t')) : k = k'

The slots

theorem Ratpoints.Fast.le_of_mem_slots {H G L r len : ℕ} {a₀ : ℤ} (h : (r, a₀, len) ∈ slots H G L) : len ≤ L

theorem Ratpoints.Fast.abs_add_mul_le_of_mem_slots {H G L r len : ℕ} {a₀ : ℤ} (hG : 0 < G) (h : (r, a₀, len) ∈ slots H G L) {t : ℕ} (ht : t < len) : |a₀ + ↑G * ↑t| ≤ ↑H

theorem Ratpoints.Fast.exists_mem_slots {H G L : ℕ} (hG : 0 < G) (hL : 0 < L) {x : ℤ} (hx : |x| ≤ ↑H) : ∃ (a₀ : ℤ) (len : ℕ), ((x % ↑G).toNat, a₀, len) ∈ slots H G L ∧ ∃ t < len, x = a₀ + ↑G * ↑t

Every numerator x with |x| ≤ H lies in a slot, with the residue of x modulo G.

theorem Ratpoints.Fast.pairwise_slots (H : ℕ) {G L : ℕ} (hG : 0 < G) (hL : 0 < L) : List.Pairwise (fun (s s' : ℕ × ℤ × ℕ) => ∀ t < s.2.2, ∀ t' < s'.2.2, s.2.1 + ↑G * ↑t ≠ s'.2.1 + ↑G * ↑t') (slots H G L)

Two slots have no numerator in common.

The region

theorem Ratpoints.Fast.div_le_of_endFrac_eq_some {H : ℕ} {x : Double} {n : ℤ} {q : ℕ} (h : endFrac H x = some (n, q)) {v : ℚ} (hv : |v| ≤ ↑H) (hx : doubleValue x.bits ≤ WithBotTop.coe v) : ↑n / ↑q ≤ v

The bound n / q that Ratpoints.Fast.endFrac makes of a lower end x lies below every v with |v| ≤ H above the value of x: it is that value when it lies in [-H, H], -(H + 1) when it lies below, and H + 1 only when it lies above H, where no such v is.

theorem Ratpoints.Fast.le_div_of_endFrac_eq_some {H : ℕ} {x : Double} {n : ℤ} {q : ℕ} (h : endFrac H x = some (n, q)) {v : ℚ} (hv : |v| ≤ ↑H) (hx : WithBotTop.coe v ≤ doubleValue x.bits) : v ≤ ↑n / ↑q

The bound n / q that Ratpoints.Fast.endFrac makes of an upper end x lies above every v with |v| ≤ H below the value of x: it is that value when it lies in [-H, H], H + 1 when it lies above, and -(H + 1) only when it lies below -H, where no such v is.

theorem Ratpoints.Fast.pos_of_endFrac_eq_some {H : ℕ} {x : Double} {n : ℤ} {q : ℕ} (h : endFrac H x = some (n, q)) : 0 < q

The denominator of the bound that Ratpoints.Fast.endFrac makes of an end is positive: a power of 2 divided by a divisor of it, or 1.

theorem Ratpoints.Fast.fst_numRange_le {H b : ℕ} (hb : 0 < b) {a : ℤ} (ha : |a| ≤ ↑H) {l : Double} (hl : doubleValue l.bits ≤ WithBotTop.coe (↑a / ↑b)) (e : Option (ℤ × ℕ)) : (numRange H b (endFrac H l, e)).1 ≤ a

The first numerator of the range of an interval lies below every a with |a| ≤ H and a / b above the lower end of the interval.

theorem Ratpoints.Fast.le_snd_numRange {H b : ℕ} (hb : 0 < b) {a : ℤ} (ha : |a| ≤ ↑H) {u : Double} (hu : WithBotTop.coe (↑a / ↑b) ≤ doubleValue u.bits) (e : Option (ℤ × ℕ)) : a ≤ (numRange H b (e, endFrac H u)).2

The last numerator of the range of an interval lies above every a with |a| ≤ H and a / b below the upper end of the interval.

theorem Ratpoints.Fast.exists_bounds_of_mem {H b : ℕ} {a : ℤ} {ivs : Array (Option (ℤ × ℕ) × Option (ℤ × ℕ))} {iv : Option (ℤ × ℕ) × Option (ℤ × ℕ)} (hiv : iv ∈ ivs) (h1 : (numRange H b iv).1 ≤ a) (h2 : a ≤ (numRange H b iv).2) : ∃ (lo : ℤ) (hi : ℤ), bounds H b (some ivs) = some (lo, hi) ∧ lo ≤ a ∧ a ≤ hi

The hull of the ranges of the intervals holds every numerator of the range of one of them.

theorem Ratpoints.Fast.exists_mem_sturmIntervals (hS : SturmTheorem) {c : List ℤ} {H depth : ℕ} {ivs : Array (Double × Double)} (h : sturmIntervals c (degree c) H depth = some ivs) {a : ℤ} {b : ℕ} (hb : 0 < b) (ha : |a| ≤ ↑H) (hF : 0 ≤ binaryForm c a ↑b) : ∃ iv ∈ ivs, doubleValue iv.1.bits ≤ WithBotTop.coe (↑a / ↑b) ∧ WithBotTop.coe (↑a / ↑b) ≤ doubleValue iv.2.bits

Assuming Sturm's theorem, the intervals of the Sturm step on the whole line hold every a / b with |a| ≤ H, b > 0 and F(a, b) ≥ 0 (Ratpoints.Sturm.covers_computeSturm).

theorem Ratpoints.Fast.exists_bounds_region (hS : SturmTheorem) {c : List ℤ} {H depth b : ℕ} (hb : 0 < b) {a : ℤ} (ha : |a| ≤ ↑H) (hF : 0 ≤ binaryForm c a ↑b) : ∃ (lo : ℤ) (hi : ℤ), bounds H b (region c (degree c) H depth) = some (lo, hi) ∧ lo ≤ a ∧ a ≤ hi

Assuming Sturm's theorem, the numerators of the denominator b > 0 that the search takes (Ratpoints.Fast.bounds) include every a with |a| ≤ H and F(a, b) ≥ 0.

The search

theorem Ratpoints.Fast.testBit_rows_shiftRight {c : List ℤ} {G L : ℕ} {fams : Array Family} (hfams : ∀ F ∈ fams, Family.IsSound c G L F) {a₀ : ℤ} {b o t : ℕ} (ht : o + t < L) (hc : IsCandidate c (a₀ + ↑G * (↑o + ↑t)) b) {i : ℕ} (hi : i < (Array.map (fun (F : Family) => F.rows[b % F.M]!) fams).size) : ((Array.map (fun (F : Family) => F.rows[b % F.M]!) fams)[i]! >>> ((Array.map (fun (x : Family) => x.shift a₀) fams)[i]! + o)).testBit t = true

The rows of sound families for the denominator b, shifted to the chunk that starts at a₀ and moved by o, keep the bit t of every candidate (a₀ + G (o + t), b) with o + t < L.

theorem Ratpoints.Fast.of_mem_partPoints {c : List ℤ} {G : ℕ} {rs sh : Array ℕ} {lo hi a₀ : ℤ} {len b : ℕ} {p : ℤ × ℤ × ℤ} (h : p ∈ partPoints c (BruteForce.degree c) G rs sh lo hi a₀ len b) : p.2.2 = ↑b ∧ (∃ t < len, p.1 = a₀ + ↑G * ↑t) ∧ p.1.gcd p.2.2 = 1 ∧ p.2.1 ^ 2 = binaryForm c p.1 p.2.2

theorem Ratpoints.Fast.mem_partPoints {c : List ℤ} {G L : ℕ} (hG : 0 < G) {fams : Array Family} (hfams : ∀ F ∈ fams, Family.IsSound c G L F) {lo hi a₀ : ℤ} {len b t : ℕ} (hlen : len ≤ L) (ht : t < len) {p : ℤ × ℤ × ℤ} (hx : p.1 = a₀ + ↑G * ↑t) (hlo : lo ≤ p.1) (hhi : p.1 ≤ hi) (hz : p.2.2 = ↑b) (hg : p.1.gcd p.2.2 = 1) (hy : p.2.1 ^ 2 = binaryForm c p.1 p.2.2) : p ∈ partPoints c (BruteForce.degree c) G (Array.map (fun (F : Family) => F.rows[b % F.M]!) fams) (Array.map (fun (x : Family) => x.shift a₀) fams) lo hi a₀ len b

A point of the chunk with its numerator from lo to hi lies in the part of the chunk.

theorem Ratpoints.Fast.nodup_partPoints (c : List ℤ) {G : ℕ} (hG : 0 < G) (rs sh : Array ℕ) (lo hi a₀ : ℤ) (len b : ℕ) : (partPoints c (BruteForce.degree c) G rs sh lo hi a₀ len b).Nodup

theorem Ratpoints.Fast.of_mem_denPoints {c : List ℤ} {H G : ℕ} {fams : Array Family} {reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))} {sl : List (ℕ × ℤ × ℕ × Array ℕ)} {b : ℕ} {p : ℤ × ℤ × ℤ} (h : p ∈ denPoints c (BruteForce.degree c) H G fams reg sl b) : p.2.2 = ↑b ∧ (∃ s ∈ sl, ∃ t < s.2.2.1, p.1 = s.2.1 + ↑G * ↑t) ∧ p.1.gcd p.2.2 = 1 ∧ p.2.1 ^ 2 = binaryForm c p.1 p.2.2

theorem Ratpoints.Fast.any_rows_eq_false {c : List ℤ} {G L : ℕ} {fams : Array Family} (hfams : ∀ F ∈ fams, Family.IsSound c G L F) {a : ℤ} {b : ℕ} (hc : IsCandidate c a b) : ((Array.map (fun (F : Family) => F.rows[b % F.M]!) fams).any fun (x : ℕ) => x == 0) = false

No row of sound families is 0 for the denominator of a candidate (Ratpoints.Fast.Family.IsSound.rows_ne_zero).

theorem Ratpoints.Fast.mem_denPoints_of {c : List ℤ} {H G L : ℕ} (hG : 0 < G) {fams : Array Family} (hfams : ∀ F ∈ fams, Family.IsSound c G L F) {reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))} {sl : List (ℕ × ℤ × ℕ × Array ℕ)} {r len t b : ℕ} {a₀ : ℤ} (hs : (r, a₀, len, Array.map (fun (x : Family) => x.shift a₀) fams) ∈ sl) (hlen : len ≤ L) (ht : t < len) {p : ℤ × ℤ × ℤ} (hx : p.1 = a₀ + ↑G * ↑t) (hz : p.2.2 = ↑b) (hg : p.1.gcd p.2.2 = 1) (hy : p.2.1 ^ 2 = binaryForm c p.1 p.2.2) {lo hi : ℤ} (hbd : bounds H b reg = some (lo, hi)) (hlo : lo ≤ p.1) (hhi : p.1 ≤ hi) : p ∈ denPoints c (BruteForce.degree c) H G fams reg sl b

A point of a chunk of sl with its numerator within the bounds of the region lies in the search of its denominator.

theorem Ratpoints.Fast.nodup_flatMap_of_pairwise {α : Type u_1} {β : Type u_2} {G : ℕ} {l : List (α × ℤ × ℕ × β)} (hl : List.Pairwise (fun (s s' : α × ℤ × ℕ × β) => ∀ t < s.2.2.1, ∀ t' < s'.2.2.1, s.2.1 + ↑G * ↑t ≠ s'.2.1 + ↑G * ↑t') l) {g : α × ℤ × ℕ × β → List (ℤ × ℤ × ℤ)} (hg : ∀ s ∈ l, (g s).Nodup) (hs : ∀ s ∈ l, ∀ p ∈ g s, ∃ t < s.2.2.1, p.1 = s.2.1 + ↑G * ↑t) : (List.flatMap g l).Nodup

The points of chunks without a numerator in common, chunk by chunk, each once, when the points of each chunk are without duplicates and lie in the chunk.

theorem Ratpoints.Fast.nodup_denPoints (c : List ℤ) (H : ℕ) {G : ℕ} (hG : 0 < G) (fams : Array Family) (reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))) {sl : List (ℕ × ℤ × ℕ × Array ℕ)} (hsl : List.Pairwise (fun (s s' : ℕ × ℤ × ℕ × Array ℕ) => ∀ t < s.2.2.1, ∀ t' < s'.2.2.1, s.2.1 + ↑G * ↑t ≠ s'.2.1 + ↑G * ↑t') sl) (b : ℕ) : (denPoints c (BruteForce.degree c) H G fams reg sl b).Nodup

theorem Ratpoints.Fast.of_mem_search {c : List ℤ} {H G L : ℕ} {fams : Array Family} {reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))} {dens : List ℕ} (hG : 0 < G) {p : ℤ × ℤ × ℤ} (h : p ∈ search c (BruteForce.degree c) H G L fams reg dens) : (∃ b ∈ dens, p.2.2 = ↑b) ∧ |p.1| ≤ ↑H ∧ p.1.gcd p.2.2 = 1 ∧ p.2.1 ^ 2 = binaryForm c p.1 p.2.2

theorem Ratpoints.Fast.mem_search_of {c : List ℤ} {H G L : ℕ} {fams : Array Family} {reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))} {dens : List ℕ} (hG : 0 < G) (hL : 0 < L) (hfams : ∀ F ∈ fams, Family.IsSound c G L F) {p : ℤ × ℤ × ℤ} {b : ℕ} (hb : b ∈ dens) (hz : p.2.2 = ↑b) (ha : |p.1| ≤ ↑H) (hg : p.1.gcd p.2.2 = 1) (hy : p.2.1 ^ 2 = binaryForm c p.1 p.2.2) {lo hi : ℤ} (hbd : bounds H b reg = some (lo, hi)) (hlo : lo ≤ p.1) (hhi : p.1 ≤ hi) : p ∈ search c (BruteForce.degree c) H G L fams reg dens

theorem Ratpoints.Fast.nodup_search (c : List ℤ) (H : ℕ) {G L : ℕ} (fams : Array Family) (reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))) {dens : List ℕ} (hG : 0 < G) (hL : 0 < L) (hdens : dens.Nodup) : (search c (BruteForce.degree c) H G L fams reg dens).Nodup

The denominators

theorem Ratpoints.Fast.getElem!_forbiddenDens_eq_zero {c : List ℤ} (hd : degree c % 2 = 0) {a : ℤ} {b : ℕ} (hc : IsCandidate c a b) (hi : ℕ) : (forbiddenDens (c.getD (degree c) 0) hi)[b]! = 0

theorem Ratpoints.Fast.getElem!_squareDens_of_isCandidate {c : List ℤ} (hd : degree c % 2 = 1) {a : ℤ} {b hi : ℕ} (hb : 1 ≤ b) (hbhi : b ≤ hi) (hc : IsCandidate c a b) : (squareDens (c.getD (degree c) 0).natAbs hi)[b]! = 1

For odd degree, the denominator b of a candidate is s k ^ 2 with s dividing the leading coefficient (Ratpoints.exists_eq_mul_mul_of_sq_eq_binaryForm_of_odd), which Ratpoints.Fast.squareDens marks.

theorem Ratpoints.Fast.denominators_sublist (c : List ℤ) (d H : ℕ) (bLow bHigh : ℤ) : (denominators c d H bLow bHigh).Sublist (List.range' (max 1 bLow.toNat) ((if bHigh < 1 then H else min H bHigh.toNat) + 1 - max 1 bLow.toNat))

The denominators of the search lie in the range of bLow, bHigh and H, in ascending order.

theorem Ratpoints.Fast.mem_denominators {c : List ℤ} {d H : ℕ} {bLow bHigh : ℤ} {b : ℕ} (h : b ∈ denominators c d H bLow bHigh) : 1 ≤ b ∧ b ≤ H ∧ bLow ≤ ↑b ∧ (bHigh < 1 ∨ ↑b ≤ bHigh)

theorem Ratpoints.Fast.mem_denominators_of_isCandidate {c : List ℤ} {H : ℕ} {bLow bHigh a : ℤ} {b : ℕ} (h1 : 1 ≤ b) (h2 : b ≤ H) (h3 : bLow ≤ ↑b) (h4 : bHigh < 1 ∨ ↑b ≤ bHigh) (hc : IsCandidate c a b) : b ∈ denominators c (BruteForce.degree c) H bLow bHigh

theorem Ratpoints.Fast.nodup_denominators (c : List ℤ) (d H : ℕ) (bLow bHigh : ℤ) : (denominators c d H bLow bHigh).Nodup

The parameters

theorem Ratpoints.Fast.mem_of_mem_groupModuli {Mmax : ℕ} {l g : List (ℕ × Array (Array Bool))} (hg : g ∈ groupModuli Mmax l) {t : ℕ × Array (Array Bool)} (ht : t ∈ g) : t ∈ l

theorem Ratpoints.Fast.choose_G_pos (tu : Tuning) (c : List ℤ) (d H B : ℕ) : 0 < (choose tu c d H B).G

theorem Ratpoints.Fast.choose_L_pos (tu : Tuning) (c : List ℤ) (d H B : ℕ) : 0 < (choose tu c d H B).L

theorem Ratpoints.Fast.eq_admitTable_of_mem_takeModuli {c : List ℤ} {d κ : ℕ} {ms : List ℕ} {E : ℕ} {t : ℕ × Array (Array Bool)} (ht : t ∈ takeModuli c d κ ms E) : t.2 = admitTable c d t.1

theorem Ratpoints.Fast.eq_admitTable_of_mem_moduliTables {tu : Tuning} {c : List ℤ} {d H B : ℕ} {t : ℕ × Array (Array Bool)} (ht : t ∈ moduliTables tu c d H B) : t.2 = admitTable c d t.1

theorem Ratpoints.Fast.eq_admitTable_of_mem_sortedGroups {tu : Tuning} {c : List ℤ} {d H B : ℕ} {g : List (ℕ × Array (Array Bool))} (hg : g ∈ sortedGroups tu c d H B) {t : ℕ × Array (Array Bool)} (ht : t ∈ g) : t.2 = admitTable c d t.1

theorem Ratpoints.Fast.isSound_of_mem_choose {tu : Tuning} {c : List ℤ} {H B : ℕ} {F : Family} (hF : F ∈ (choose tu c (BruteForce.degree c) H B).fams) : Family.IsSound c (choose tu c (BruteForce.degree c) H B).G (choose tu c (BruteForce.degree c) H B).L F

The points

theorem Ratpoints.Fast.isPoint_and_inRegion_of_mem_sievePoints {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Tuning} {p : ℤ × ℤ × ℤ} (h : p ∈ sievePoints c H bLow bHigh tu) : IsPoint c H p ∧ InRegion [] bLow bHigh p

theorem Ratpoints.Fast.mem_sievePoints_of_isPoint (hS : SturmTheorem) {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Tuning} {p : ℤ × ℤ × ℤ} (hp : IsPoint c H p) (hr : InRegion [] bLow bHigh p) : p ∈ sievePoints c H bLow bHigh tu

The search without the reversal lists every point of the region, assuming Sturm's theorem, on which the region of the numerators rests (Ratpoints.Fast.exists_bounds_region).

theorem Ratpoints.Fast.nodup_sievePoints (c : List ℤ) (H : ℕ) (bLow bHigh : ℤ) (tu : Tuning) : (sievePoints c H bLow bHigh tu).Nodup

theorem Ratpoints.Fast.isFullBox_and_binaryForm_eq_of_reversed_eq {c c' : List ℤ} {H : ℕ} {bLow bHigh : ℤ} (h : reversed c H bLow bHigh = (c', true)) : IsFullBox [] bLow bHigh H ∧ ∀ (x z : ℤ), binaryForm c' x z = binaryForm c z x

Ratpoints.Fast.reversed reverses only for the whole box, and then the binary form of the reversed list is that of c with x and z exchanged (Ratpoints.Setup.binaryForm_eq_of_reversal_eq_ok).

theorem Ratpoints.Fast.isPoint_and_inRegion_of_mem_fastPoints {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Tuning} {p : ℤ × ℤ × ℤ} (h : p ∈ fastPoints c H bLow bHigh tu) : IsPoint c H p ∧ InRegion [] bLow bHigh p

The fast search lists only points of height at most H with their denominator in the range of bLow and bHigh, for every coefficient list, every height bound, every range and every setting of the parameters: when the coefficients are reversed, the search of the reversed list lists only points, which Ratpoints.Sieve.swapPoint maps to points (Ratpoints.Sieve.isPoint_swapPoint), of the whole box.

theorem Ratpoints.Fast.mem_fastPoints_of_isPoint (hS : SturmTheorem) {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Tuning} {p : ℤ × ℤ × ℤ} (hp : IsPoint c H p) (hr : InRegion [] bLow bHigh p) : p ∈ fastPoints c H bLow bHigh tu

The fast search lists every point of height at most H with its denominator in the range of bLow and bHigh, assuming Sturm's theorem, on which the region of the search rests (Ratpoints.Fast.exists_bounds_region): when the coefficients are reversed, the point mapped by Ratpoints.Sieve.swapPoint is a point of the reversed list, of the whole box.

theorem Ratpoints.Fast.mem_fastPoints_iff {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Tuning} {p : ℤ × ℤ × ℤ} (hS : SturmTheorem) : p ∈ fastPoints c H bLow bHigh tu ↔ IsPoint c H p ∧ InRegion [] bLow bHigh p

The fast search lists exactly the points of height at most H with their denominator in the range of bLow and bHigh, for every coefficient list, every height bound, every range and every setting of the parameters, assuming Sturm's theorem.

theorem Ratpoints.Fast.nodup_fastPoints (c : List ℤ) (H : ℕ) (bLow bHigh : ℤ) (tu : Tuning) : (fastPoints c H bLow bHigh tu).Nodup

The fast search lists each point once: when the coefficients are reversed, Ratpoints.Sieve.swapPoint is injective on the points of the reversed list (Ratpoints.Sieve.swapPoint_inj).