The fast search on byte-array masks finds exactly the points

Ratpoints.FastMask.fastPoints lists the same points as Ratpoints.Fast.fastPoints, in another order (Ratpoints.FastMask.fastPoints_perm), so it lists only points of the region (Ratpoints.FastMask.isPoint_and_inRegion_of_mem_fastPoints), each once (Ratpoints.FastMask.nodup_fastPoints), and, assuming Sturm's theorem, all of them (Ratpoints.FastMask.mem_fastPoints_iff).

A mask is read as the natural number Ratpoints.Mask.toNat, whose bit j is bit j of the mask (Ratpoints.Mask.testBit_toNat). The reference definitions of the three primitives then do what the search on natural numbers does: Ratpoints.Mask.andShr is the AND with a row shifted to the right (Ratpoints.Mask.toNat_andShr), Ratpoints.Mask.andRows the AND with all the shifted rows of a denominator (Ratpoints.Mask.toNat_andRowsFrom), which on the mask of a chunk is the sieve of the search on natural numbers (Ratpoints.Mask.toNat_andRows_of_toNat_eq), and Ratpoints.Mask.setBits, on Ratpoints.Mask.nextSet, lists the set bits in ascending order where Ratpoints.Fast.setBits lists them in descending order (Ratpoints.Mask.setBits_perm). The periodic rows of Ratpoints.FastMask.baseRow and Ratpoints.Fast.baseRow agree on the bits that a family keeps (Ratpoints.FastMask.testBit_toNat_baseRow, Ratpoints.Fast.testBit_baseRow_of_lt), so the families of the two searches agree once their rows are read as numbers (Ratpoints.FastMask.map_toFast_mkFamily), and so do the parameters, the zero tests of the rows of a denominator (Ratpoints.Mask.any_isZero) and the candidates that the sieve leaves in a chunk or in a part of it, whose mask is cut from that of the chunk (Ratpoints.Mask.toNat_extract_ones, Ratpoints.FastMask.partPoints_perm); the exact check with the data made once per denominator is that of the brute force (Ratpoints.FastMask.pointsOfDenWith_eq_pointsOfDen), so the two searches agree denominator by denominator (Ratpoints.FastMask.denPoints_perm) and on the whole (Ratpoints.FastMask.search_perm, Ratpoints.FastMask.sievePoints_perm), also when the coefficients are reversed, which both decide alike (Ratpoints.Fast.reversed).

Main statements

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

Bytes and bits

theorem Nat.testBit_of_le_one {x : ℕ} (hx : x ≤ 1) (n : ℕ) : x.testBit n = (decide (n = 0) && decide (x = 1))

theorem Array.getElem!_map_list_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → List β) (φ : β → γ) (xs : Array α) (n : ℕ) : (map (fun (a : α) => List.map φ (f a)) xs)[n]! = List.map φ (map f xs)[n]!

Masks as numbers

def Ratpoints.Mask.toNat (a : ByteArray) : ℕ

The mask a as a natural number, byte i of a standing for its value times 256 ^ i: bit j of it is Ratpoints.Mask.bit a j (Ratpoints.Mask.testBit_toNat).

Equations

• Ratpoints.Mask.toNat a = List.foldr (fun (x : UInt8) (n : ℕ) => x.toNat + 256 * n) 0 a.data.toList

theorem Ratpoints.Mask.testBit_foldr (l : List UInt8) (j : ℕ) : (List.foldr (fun (x : UInt8) (n : ℕ) => x.toNat + 256 * n) 0 l).testBit j = (l.getD (j / 8) 0).toNat.testBit (j % 8)

theorem Ratpoints.Mask.byte_eq_toNat_getD (a : ByteArray) (i : ℕ) : byte a i = (a.data.toList.getD i 0).toNat

theorem Ratpoints.Mask.testBit_toNat (a : ByteArray) (j : ℕ) : (toNat a).testBit j = bit a j

theorem Ratpoints.Mask.byte_of_lt {a : ByteArray} {i : ℕ} (h : i < a.size) : byte a i = a[i].toNat

theorem Ratpoints.Mask.byte_of_le {a : ByteArray} {i : ℕ} (h : a.size ≤ i) : byte a i = 0

theorem Ratpoints.Mask.byte_lt (a : ByteArray) (i : ℕ) : byte a i < 2 ^ 8

theorem Ratpoints.Mask.bit_of_le {a : ByteArray} {j : ℕ} (h : 8 * a.size ≤ j) : bit a j = false

theorem Ratpoints.Mask.toNat_of_size_eq_zero {a : ByteArray} (h : a.size = 0) : toNat a = 0

@[simp]

theorem Ratpoints.Mask.toNat_empty : toNat ByteArray.empty = 0

theorem Ratpoints.Mask.toNat_eq_zero_iff (a : ByteArray) : toNat a = 0 ↔ ∀ j < 8 * a.size, bit a j = false

The AND with a shifted row

theorem Ratpoints.Mask.testBit_shrByte (row : ByteArray) (s i : ℕ) {t : ℕ} (ht : t < 8) : (shrByte row s i).toNat.testBit t = bit row (8 * i + t + s)

theorem Ratpoints.Mask.bit_mapIdx_and_shrByte (acc row : ByteArray) (s j : ℕ) : bit { data := Array.mapIdx (fun (i : ℕ) (x : UInt8) => x &&& shrByte row s i) acc.data } j = (bit acc j && bit row (j + s))

theorem Ratpoints.Mask.bit_of_all {a : ByteArray} (h : (a.data.all fun (x : UInt8) => x == 0) = true) (j : ℕ) : bit a j = false

theorem Ratpoints.Mask.bit_andShrSpec (acc row : ByteArray) (s j : ℕ) : bit (andShrSpec acc row s) j = (bit acc j && bit row (j + s))

theorem Ratpoints.Mask.toNat_andShr (acc row : ByteArray) (s : ℕ) : toNat (andShr acc row s) = toNat acc &&& toNat row >>> s

The primitive Ratpoints.Mask.andShr (by its reference definition) is the AND with the row shifted to the right; no mask is needed, the bits of acc past its end being 0.

theorem Ratpoints.Mask.bit_ones (len j : ℕ) : bit (ones len) j = decide (j < len)

theorem Ratpoints.Mask.toNat_ones (len : ℕ) : toNat (ones len) = 2 ^ len - 1

The set bits

theorem Ratpoints.Mask.nextSetSpec_zero_eq_iff (a : ByteArray) : nextSetSpec a 0 = 8 * a.size ↔ ∀ j < 8 * a.size, bit a j = false

theorem Ratpoints.Mask.isZero_eq_beq (a : ByteArray) : isZero a = (toNat a == 0)

theorem Ratpoints.Mask.any_isZero (rs : Array ByteArray) : rs.any isZero = (Array.map toNat rs).any fun (x : ℕ) => x == 0

theorem Ratpoints.Mask.le_nextSetSpec (a : ByteArray) {j : ℕ} (h : nextSetSpec a j < 8 * a.size) : j ≤ nextSetSpec a j

theorem Ratpoints.Mask.bit_nextSetSpec (a : ByteArray) {j : ℕ} (h : nextSetSpec a j < 8 * a.size) : bit a (nextSetSpec a j) = true

theorem Ratpoints.Mask.bit_of_lt_nextSetSpec (a : ByteArray) {i j : ℕ} (hj : j ≤ i) (hi : i < nextSetSpec a j) : bit a i = false

theorem Ratpoints.Mask.mem_setBitsFrom (a : ByteArray) {fuel j : ℕ} (h : 8 * a.size ≤ j + fuel) {t : ℕ} : t ∈ setBitsFrom a fuel j ↔ j ≤ t ∧ bit a t = true

With enough fuel, Ratpoints.Mask.setBitsFrom a fuel j lists the set bits of a from j on.

theorem Ratpoints.Mask.mem_setBits (a : ByteArray) {t : ℕ} : t ∈ setBits a ↔ (toNat a).testBit t = true

theorem Ratpoints.Mask.le_of_mem_setBitsFrom (a : ByteArray) {fuel j t : ℕ} (h : t ∈ setBitsFrom a fuel j) : j ≤ t

theorem Ratpoints.Mask.nodup_setBitsFrom (a : ByteArray) (fuel j : ℕ) : (setBitsFrom a fuel j).Nodup

theorem Ratpoints.Mask.nodup_setBits (a : ByteArray) : (setBits a).Nodup

theorem Ratpoints.Mask.setBits_perm (a : ByteArray) : (setBits a).Perm (Fast.setBits (toNat a))

Ratpoints.Mask.setBits lists the set bits in ascending order, Ratpoints.Fast.setBits in descending order.

Appending and extracting

theorem Ratpoints.Mask.byte_append (a b : ByteArray) (i : ℕ) : byte (a ++ b) i = if i < a.size then byte a i else byte b (i - a.size)

theorem Ratpoints.Mask.byte_extract (a : ByteArray) (s e i : ℕ) : byte (a.extract s e) i = if s + i < e then byte a (s + i) else 0

theorem Ratpoints.Mask.bit_extract (a : ByteArray) (s e j : ℕ) : bit (a.extract s e) j = (decide (s + j / 8 < e) && bit a (8 * s + j))

theorem Ratpoints.Mask.toNat_extract_ones {len t₁ len₁ : ℕ} (h8 : 8 ∣ t₁) (hle : t₁ + len₁ ≤ len) (hend : t₁ + len₁ = len ∨ 64 ∣ t₁ + len₁) : toNat ((ones len).extract (t₁ / 8) (8 * ((t₁ + len₁ + 63) / 64))) = 2 ^ len₁ - 1

The bits t₁, …, t₁ + len₁ - 1 of the mask of len bits, all set, from the byte of t₁ to the end of the 64-bit word of the last of them, are all set, and no other bit is when they end at the end of the mask or of a word.

The rows of the search on natural numbers

theorem Ratpoints.Fast.pattern_lt_two_pow (m : ℕ) (f : ℕ → Bool) : pattern m f < 2 ^ m

theorem Ratpoints.Fast.testBit_repeatPattern_of_lt_two_pow {P m : ℕ} (hP : P < 2 ^ m) (k j : ℕ) : (repeatPattern P m k).testBit j = (decide (j < m * 2 ^ k) && P.testBit (j % m))

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

The bits below N of the row of a modulus, both ways (Ratpoints.Fast.testBit_baseRow has one direction).

theorem Ratpoints.Fast.testBit_foldl_and_eq {α : Type u_1} (g : α → ℕ) (l : List α) (init j : ℕ) : (List.foldl (fun (acc : ℕ) (x : α) => acc &&& g x) init l).testBit j = (init.testBit j && l.all fun (x : α) => (g x).testBit j)

theorem Ratpoints.Fast.foldl_and_zero {α : Type u_1} (g : α → ℕ) (l : List α) : List.foldl (fun (n : ℕ) (x : α) => n &&& g x) 0 l = 0

theorem Ratpoints.Fast.setBits_zero : setBits 0 = []

theorem Ratpoints.Fast.sieve_map_toNat (rs : Array ByteArray) (sh : Array ℕ) (o mask : ℕ) : sieve (Array.map Mask.toNat rs) sh o mask = List.foldl (fun (n i : ℕ) => n &&& Mask.toNat rs[i]! >>> (sh[i]! + o)) mask (List.range rs.size)

The sieve on rows read as numbers (Ratpoints.Mask.toNat), without its zero tests: an AND with 0 stays 0.

The AND with several rows

theorem Ratpoints.Mask.toNat_andRowsFrom (rs : Array ByteArray) (sh : Array ℕ) (o : ℕ) (acc : ByteArray) (i : ℕ) : toNat (andRowsFrom rs sh o acc i) = List.foldl (fun (n j : ℕ) => n &&& toNat rs[j]! >>> (sh[j]! + o)) (toNat acc) (List.drop i (List.range rs.size))

The reference definition of Ratpoints.Mask.andRows, from position i on, is the AND with the shifted rows from i on; its zero tests drop nothing, an AND with 0 staying 0.

theorem Ratpoints.Mask.toNat_andRows_of_toNat_eq (rs : Array ByteArray) (sh : Array ℕ) (o : ℕ) {mask : ByteArray} {len : ℕ} (h : toNat mask = 2 ^ len - 1) : toNat (andRows mask rs sh o) = Fast.sieve (Array.map toNat rs) sh o (2 ^ len - 1)

The primitive Ratpoints.Mask.andRows (by its reference definition) on a mask with exactly its len lowest bits set is the sieve of the search on natural numbers.

The rows

theorem Ratpoints.FastMask.size_repeatBytes (a : ByteArray) (k : ℕ) : (repeatBytes a k).size = a.size * 2 ^ k

theorem Ratpoints.FastMask.byte_repeatBytes (a : ByteArray) (k i : ℕ) : Mask.byte (repeatBytes a k) i = if i < a.size * 2 ^ k then Mask.byte a (i % a.size) else 0

theorem Ratpoints.FastMask.byte_extract_repeatBytes {a : ByteArray} {k n i : ℕ} (hn : n ≤ a.size * 2 ^ k) (hi : i < n) : Mask.byte ((repeatBytes a k).extract 0 n) i = Mask.byte a (i % a.size)

theorem Ratpoints.FastMask.testBit_windowByte {q : ByteArray} (hq : ∀ (i : ℕ), q[i]!.toNat ≤ 1) (o : ℕ) {t : ℕ} (ht : t < 8) : (windowByte q o).toNat.testBit t = decide (q[o + t]!.toNat = 1)

Bit t of Ratpoints.FastMask.windowByte q o is the byte q[o + t], when each byte of q is 0 or 1.

theorem Ratpoints.FastMask.size_patternBits (T' : Array Bool) (m g k i : ℕ) (acc : ByteArray) : (patternBits T' m g k i acc).size = acc.size + (m + 8 - k)

theorem Ratpoints.FastMask.getElem!_patternBits_of_lt (T' : Array Bool) (m g k i : ℕ) (acc : ByteArray) {i' : ℕ} (hi' : i' < acc.size) : (patternBits T' m g k i acc)[i']! = acc[i']!

theorem Ratpoints.FastMask.getElem!_patternBits (T' : Array Bool) {m g : ℕ} (hg : g < m) (k i : ℕ) (acc : ByteArray) (hi : i = k * g % m) {j : ℕ} (hk : k ≤ j) (hj : j < m + 8) : (patternBits T' m g k i acc)[acc.size + (j - k)]! = T'[j * g % m]!.toUInt8

The bytes that Ratpoints.FastMask.patternBits pushes, for the index i = k g modulo m stepped by g < m.

theorem Ratpoints.FastMask.size_periodBytes (q : ByteArray) (m i o : ℕ) (acc : ByteArray) : (periodBytes q m i o acc).size = acc.size + (m - i)

theorem Ratpoints.FastMask.getElem!_periodBytes_of_lt (q : ByteArray) (m i o : ℕ) (acc : ByteArray) {i' : ℕ} (hi' : i' < acc.size) : (periodBytes q m i o acc)[i']! = acc[i']!

theorem Ratpoints.FastMask.ite_add_eight_eq_mul_mod {m i o : ℕ} (ho : o = 8 * i % m) : (if o + 8 < m then o + 8 else (o + 8) % m) = 8 * (i + 1) % m

theorem Ratpoints.FastMask.getElem!_periodBytes (q : ByteArray) (m i o : ℕ) (acc : ByteArray) (ho : o = 8 * i % m) {j : ℕ} (hi : i ≤ j) (hj : j < m) : (periodBytes q m i o acc)[acc.size + (j - i)]! = windowByte q (8 * j % m)

theorem Ratpoints.FastMask.getElem!_patternBits_zero (T' : Array Bool) {m g : ℕ} (hg : g < m) (c j : ℕ) : (patternBits T' m g 0 0 (ByteArray.emptyWithCapacity c))[j]! = if j < m + 8 then T'[j * g % m]!.toUInt8 else 0

theorem Ratpoints.FastMask.toNat_getElem!_patternBits_le_one (T' : Array Bool) {m g : ℕ} (hg : g < m) (c j : ℕ) : (patternBits T' m g 0 0 (ByteArray.emptyWithCapacity c))[j]!.toNat ≤ 1

theorem Ratpoints.FastMask.testBit_toNat_baseRow {T : Array (Array Bool)} {m G nb r j : ℕ} (hm : 0 < m) (hj : j < 8 * nb) : (Mask.toNat (baseRow T m G nb r)).testBit j = T[r]![G * j % m]!

The bits of the row of a modulus: the bits below 8 nb of the periodic byte pattern.

The families

theorem Ratpoints.FastMask.testBit_toNat_foldl_andShr {α : Type u_1} (g : α → ByteArray) (l : List α) (init : ByteArray) (j : ℕ) : (Mask.toNat (List.foldl (fun (acc : ByteArray) (x : α) => Mask.andShr acc (g x) 0) init l)).testBit j = ((Mask.toNat init).testBit j && l.all fun (x : α) => (Mask.toNat (g x)).testBit j)

theorem Ratpoints.FastMask.toNat_foldl_baseRow {G N : ℕ} {ts : List (ℕ × Array (Array Bool))} (hts : ∀ t ∈ ts, 0 < t.1) (r : ℕ) : Mask.toNat (List.foldl (fun (acc : ByteArray) (x : ℕ × Array ByteArray) => Mask.andShr acc x.2[r % x.1]! 0) (Mask.ones N) (List.map (fun (t : ℕ × Array (Array Bool)) => (t.1, Array.map (baseRow t.2 t.1 G (8 * ((N + 63) / 64))) (List.range t.1).toArray)) ts)) = List.foldl (fun (acc : ℕ) (x : ℕ × Array ℕ) => acc &&& x.2[r % x.1]!) (2 ^ N - 1) (List.map (fun (t : ℕ × Array (Array Bool)) => (t.1, Array.map (Fast.baseRow t.2 t.1 G N) (List.range t.1).toArray)) ts)

The row of a family for the residue r is the same in both searches: the AND of the rows of the moduli agrees on the bits below N, and the full mask clears the others.

def Ratpoints.FastMask.Family.toFast (F : Family) : Fast.Family

The family F with its rows as natural numbers (Ratpoints.Mask.toNat): the family of Ratpoints.Fast that Ratpoints.Fast.mkFamily makes where Ratpoints.FastMask.mkFamily makes F (Ratpoints.FastMask.map_toFast_mkFamily).

Equations

• F.toFast = { M := F.M, ginv := F.ginv, rows := Array.map Ratpoints.Mask.toNat F.rows }

@[simp]

theorem Ratpoints.FastMask.Family.toFast_M (F : Family) : F.toFast.M = F.M

@[simp]

theorem Ratpoints.FastMask.Family.toFast_rows (F : Family) : F.toFast.rows = Array.map Mask.toNat F.rows

@[simp]

theorem Ratpoints.FastMask.Family.shift_toFast (F : Family) (a₀ : ℤ) : F.toFast.shift a₀ = F.shift a₀

theorem Ratpoints.FastMask.map_toFast_mkFamily (G L : ℕ) (ts : List (ℕ × Array (Array Bool))) : Option.map Family.toFast (mkFamily G L ts) = Fast.mkFamily G L ts

theorem Ratpoints.FastMask.map_toFast_fams_choose (tu : Fast.Tuning) (c : List ℤ) (d H B : ℕ) : Array.map Family.toFast (choose tu c d H B).fams = (Fast.choose tu c d H B).fams

The points

theorem Ratpoints.FastMask.hornerRec_eq_horner (w : List ℤ) (x : ℤ) : hornerRec w x = BruteForce.horner w x

theorem Ratpoints.FastMask.pointsOfDenWith_eq_pointsOfDen (c : List ℤ) (d : ℕ) (z : ℤ) : pointsOfDenWith (BruteForce.scaledCoeffs c d z) (if d % 2 = 1 then z else 1) z = BruteForce.pointsOfDen c d z

theorem Ratpoints.FastMask.pointsOfDen_eq_pointsOfDen : pointsOfDen = BruteForce.pointsOfDen

theorem Ratpoints.FastMask.chunkPoints_perm {c : List ℤ} {d : ℕ} (G : ℕ) {w : Thunk (List ℤ)} {f : ℤ} {b : ℕ} (hw : w.get = BruteForce.scaledCoeffs c d ↑b) (hf : f = if d % 2 = 1 then ↑b else 1) (rs : Array ByteArray) (sh : Array ℕ) (o : ℕ) (a₀ : ℤ) {mask : ByteArray} {len : ℕ} (hmask : Mask.toNat mask = 2 ^ len - 1) : (chunkPoints G w f rs sh o a₀ mask b).Perm (Fast.chunkPoints c d G (Array.map Mask.toNat rs) sh o a₀ len b)

The two searches list the same points of a chunk, up to order, when the mask has exactly its len lowest bits set and the exact check gets the scaled coefficients of b and its factor.

theorem Ratpoints.FastMask.partPoints_perm {c : List ℤ} {d : ℕ} (G : ℕ) {w : Thunk (List ℤ)} {f : ℤ} {b : ℕ} (hw : w.get = BruteForce.scaledCoeffs c d ↑b) (hf : f = if d % 2 = 1 then ↑b else 1) (rs : Array ByteArray) (sh : Array ℕ) (lo hi a₀ : ℤ) (len : ℕ) : (partPoints G w f rs sh lo hi a₀ len (Mask.ones len) b).Perm (Fast.partPoints c d G (Array.map Mask.toNat rs) sh lo hi a₀ len b)

The two searches list the same points of the part of a chunk, up to order: the part that is the whole chunk with the mask of the chunk, another with the bytes of the mask that hold its bits (Ratpoints.Mask.toNat_extract_ones).

theorem Ratpoints.FastMask.denPoints_perm (c : List ℤ) (d H G : ℕ) (fams : Array Family) (reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))) (l : List (ℕ × ℤ × ℕ)) (b : ℕ) : (denPoints c d H G fams reg (List.map (fun (s : ℕ × ℤ × ℕ) => (s.1, s.2.1, s.2.2, Mask.ones s.2.2, Array.map (fun (x : Family) => x.shift s.2.1) fams)) l) b).Perm (Fast.denPoints c d H G (Array.map Family.toFast fams) reg (List.map (fun (s : ℕ × ℤ × ℕ) => (s.1, s.2.1, s.2.2, Array.map (fun (x : Fast.Family) => x.shift s.2.1) (Array.map Family.toFast fams))) l) b)

The two searches list the same points of the denominator b in the chunks l, up to order, each chunk with its mask of len bits, all set, and the shifts of the families to it.

theorem Ratpoints.FastMask.filter_map_toFast (fams : Array Family) : Array.filter (fun (F : Fast.Family) => F.rows.size == F.M && decide (0 < F.M)) (Array.map Family.toFast fams) = Array.map Family.toFast (Array.filter (fun (F : Family) => F.rows.size == F.M && decide (0 < F.M)) fams)

The families of the search on masks that have a row for each residue of a positive product, as families of the search on natural numbers.

theorem Ratpoints.FastMask.search_perm (c : List ℤ) (d H G L : ℕ) (fams : Array Family) (reg : Option (Array (Option (ℤ × ℕ) × Option (ℤ × ℕ)))) (dens : List ℕ) : (search c d H G L fams reg dens).Perm (Fast.search c d H G L (Array.map Family.toFast fams) reg dens)

theorem Ratpoints.FastMask.sievePoints_perm (c : List ℤ) (H : ℕ) (bLow bHigh : ℤ) (tu : Fast.Tuning) : (sievePoints c H bLow bHigh tu).Perm (Fast.sievePoints c H bLow bHigh tu)

The searches without the reversal list the same points.

theorem Ratpoints.FastMask.fastPoints_perm (c : List ℤ) (H : ℕ) (bLow bHigh : ℤ) (tu : Fast.Tuning) : (fastPoints c H bLow bHigh tu).Perm (Fast.fastPoints c H bLow bHigh tu)

The search on byte-array masks lists the same points as the search on natural numbers, Ratpoints.Fast.fastPoints, in another order, for every coefficient list, every height bound, every range and every setting of the parameters.

theorem Ratpoints.FastMask.isPoint_and_inRegion_of_mem_fastPoints {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Fast.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.

theorem Ratpoints.FastMask.mem_fastPoints_iff {c : List ℤ} {H : ℕ} {bLow bHigh : ℤ} {tu : Fast.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.FastMask.nodup_fastPoints (c : List ℤ) (H : ℕ) (bLow bHigh : ℤ) (tu : Fast.Tuning) : (fastPoints c H bLow bHigh tu).Nodup

The fast search lists each point once.