A fast search for the points

Ratpoints.Fast.fastPoints c H bLow bHigh lists the normalized points of height at most H on y ^ 2 = F(x, z) whose denominator z lies in the range of bLow and bHigh (the points at infinity always), each once, in an order of its own: only such points in any case, and all of them assuming Sturm's theorem, on which the region of the numerators rests. It is not a model of the C code: it sieves in the way that suits Lean, with bit masks held in natural numbers, which Lean represents by GMP integers, so that one &&& ANDs thousands of candidates without an allocation per word. The program ratpoints-lean runs Ratpoints.FastMask.fastPoints, the same sieve with the masks held in byte arrays, which lists the same points in another order.

• Without a range of the denominators (bLow ≤ 1, and bHigh < 1 or H ≤ bHigh) the coefficients are reversed where the reversal check of ratpoints reverses them (Ratpoints.Fast.reversed, on Ratpoints.Setup.reversal: the binary form with x and z exchanged); the search Ratpoints.Fast.sievePoints then runs on them over the whole box, and its points are mapped back by Ratpoints.Sieve.swapPoint.
• The numerators x = -H, …, H are split into the classes of x + H modulo G = 2 ^ e; a class is searched for the denominator b only when the residues of x and b modulo G allow a point (Ratpoints.Fast.admitTable).
• Each class is searched in chunks of at most L numerators a₀, a₀ + G, a₀ + 2G, …. A chunk is a bit mask with one bit per numerator, ANDed with the rows of the families of moduli (Ratpoints.Fast.Family): the row of the family of the moduli m₁, …, mₖ for b has the bit of x set when for every mᵢ the residues of x and b allow a point. The rows of a family depend on b modulo M = m₁ ⋯ mₖ only, and on x modulo M: they are made once, for the numerators 0, G, 2G, …, and shifted to the start of a chunk, by a multiple of 8 when M is odd (Ratpoints.Fast.Family.shift).
• The denominators are the outer loop: for each b, every chunk of every class that b allows is searched in turn, with the same rows, which the search on byte arrays then finds in the cache.
• The bits that survive go to the exact check of the brute force, Ratpoints.BruteForce.pointsOfDen.
• For odd degree only the denominators s k ^ 2 with s dividing the leading coefficient can carry a point, and only they are searched; for even degree no multiple of an odd p with (c_d / p) = -1 can (Ratpoints.Fast.forbiddenDens).
• The numerators of a denominator b are those a with a / b in the intervals that the Sturm step of ratpoints keeps (Ratpoints.Fast.region), outside of which F(a, b) < 0 assuming Sturm's theorem: each chunk is cut to the 64-bit words that hold the numerators from the first to the last of them (Ratpoints.Fast.bounds, Ratpoints.Fast.part).

The choice of G, L and the families affects the speed only: the proofs hold for every choice.

Main definitions

• Ratpoints.Fast.fastPoints: the points, by the sieve.
• Ratpoints.Fast.sievePoints: the search without the reversal.

Residues that allow a point

def Ratpoints.Fast.sqTable (m : Nat) : Array Bool

The squares modulo m: entry v is true when v = y * y % m for some y < m (each y * y % m marked in turn).

Equations

• Ratpoints.Fast.sqTable m = List.foldl (fun (A : Array Bool) (y : Nat) => A.set! (y * y % m) true) (Array.replicate m false) (List.range m)

def Ratpoints.Fast.hornerMod : List Int → Int → Nat → Int

Horner's rule modulo m: the value w₀ + x (w₁ + x (w₂ + ⋯)) reduced modulo m at each step.

Equations

• Ratpoints.Fast.hornerMod [] x✝¹ x✝ = 0
• Ratpoints.Fast.hornerMod (a :: w) x✝¹ x✝ = (a + x✝¹ * Ratpoints.Fast.hornerMod w x✝¹ x✝) % ↑x✝

def Ratpoints.Fast.powMod (r m : Nat) : Nat → Nat

r ^ e % m, by repeated multiplication modulo m.

Equations

• Ratpoints.Fast.powMod r m 0 = 1 % m
• Ratpoints.Fast.powMod r m e.succ = Ratpoints.Fast.powMod r m e * r % m

def Ratpoints.Fast.scaledCoeffsMod (c : List Int) (d m r : Nat) : List Int

The products cₖ r^(d - k) of Ratpoints.BruteForce.scaledCoeffs c d r, reduced modulo m.

Equations

• Ratpoints.Fast.scaledCoeffsMod c d m r = List.map (fun (k : Nat) => c.getD k 0 % ↑m * ↑(Ratpoints.Fast.powMod r m (d - k))) (List.range (d + 1))

@[irreducible]

def Ratpoints.Fast.natGcd (a b : Nat) : Nat

Nat.gcd a b by Euclid's algorithm in Lean, which on small numbers is much faster than the runtime's Nat.gcd: that one goes through GMP.

Equations

• Ratpoints.Fast.natGcd a b = if b = 0 then a else Ratpoints.Fast.natGcd b (a % b)

def Ratpoints.Fast.coprimeWith (g x : Nat) : Bool

Whether x has no prime factor in common with g, quickly when g = 1.

Equations

• Ratpoints.Fast.coprimeWith g x = (g == 1 || Ratpoints.Fast.natGcd x g == 1)

def Ratpoints.Fast.admitRow (c : List Int) (d m : Nat) (sq : Array Bool) (r : Nat) : Array Bool

The row r of Ratpoints.Fast.admitTable c d m, computed directly (sq is Ratpoints.Fast.sqTable m): entry x is true when x, r and m have no prime factor in common and F(x, r) is a square modulo m.

Equations

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

def Ratpoints.Fast.invTable (m : Nat) : Array Nat

Candidates for the inverses modulo m, entry i by inv i = -(m / i) inv (m % i): the inverses when m is prime, and checked where they are used.

Equations

• Ratpoints.Fast.invTable m = List.foldl (fun (inv : Array Nat) (i : Nat) => inv.push (if i ≤ 1 then i else (m - m / i * inv[m % i]! % m) % m)) #[] (List.range m)

def Ratpoints.Fast.permRow (one : Array Bool) (m u : Nat) : Array Bool

The row one permuted: entry x < m is one[x * u % m], the index stepped by u (for u < m), without a division.

Equations

• Ratpoints.Fast.permRow one m u = Ratpoints.Fast.permRow.go one m u 0 0 (Array.emptyWithCapacity m)

@[irreducible]

def Ratpoints.Fast.permRow.go (one : Array Bool) (m u x i : Nat) (acc : Array Bool) : Array Bool

acc with the entries one[i] pushed for x up to m - 1, the index i stepped by u modulo m.

Equations

• Ratpoints.Fast.permRow.go one m u x i acc = if x < m then Ratpoints.Fast.permRow.go one m u (x + 1) (if i + u < m then i + u else i + u - m) (acc.push one[i]!) else acc

def Ratpoints.Fast.admitTable (c : List Int) (d m : Nat) : Array (Array Bool)

The residues modulo m that allow a point (a, y, b) with gcd(a, b) = 1 of the binary form of degree d of c: entry x of row r (for r, x < m) is true when x, r and m have no prime factor in common and F(x, r) is a square modulo m. A row r with an inverse u < m modulo m (from Ratpoints.Fast.invTable) is row 1 permuted (Ratpoints.Fast.permRow): F(x, r) = r ^ D F(x u, 1) with D even; the others come from Ratpoints.Fast.admitRow.

Equations

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

@[irreducible]

def Ratpoints.Fast.admitTable.go (c : List Int) (d m : Nat) (sq one : Array Bool) (inv : Array Nat) (r : Nat) (acc : Array (Array Bool)) : Array (Array Bool)

acc with the rows r to m - 1 of Ratpoints.Fast.admitTable pushed.

Equations

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

Bit masks

def Ratpoints.Fast.pattern (m : Nat) (f : Nat → Bool) : Nat

The number with bit j set for every j < m with f j.

Equations

• Ratpoints.Fast.pattern m f = List.foldl (fun (P j : Nat) => if f j = true then P ||| 1 <<< j else P) 0 (List.range m)

def Ratpoints.Fast.repeatPattern (P m : Nat) : Nat → Nat

The pattern P of m bits repeated 2 ^ k times.

Equations

• Ratpoints.Fast.repeatPattern P m 0 = P
• Ratpoints.Fast.repeatPattern P m e.succ = Ratpoints.Fast.repeatPattern P m e ||| Ratpoints.Fast.repeatPattern P m e <<< (m * 2 ^ e)

def Ratpoints.Fast.doublings (m N : Nat) : Nat

A number k of doublings with N ≤ m * 2 ^ k for 0 < m.

Equations

• Ratpoints.Fast.doublings m N = (N / m).log2 + 1

@[irreducible]

def Ratpoints.Fast.setBitsSmall (n : Nat) : List Nat

The positions of the bits set in n, from the highest down, one Nat.log2 at a time.

Equations

• Ratpoints.Fast.setBitsSmall n = if h : n = 0 then [] else n.log2 :: Ratpoints.Fast.setBitsSmall (n - 2 ^ n.log2)

def Ratpoints.Fast.setBitsAux (o n : Nat) : Nat → List Nat

The positions, offset by o, of the bits set in n: those of n >>> h and of n % 2 ^ h for h = 64 * 2 ^ (k - 1) in turn, down to k = 0, where Ratpoints.Fast.setBitsSmall takes all the bits that are left.

Equations

• Ratpoints.Fast.setBitsAux o n 0 = List.map (fun (x : Nat) => o + x) (Ratpoints.Fast.setBitsSmall n)
• Ratpoints.Fast.setBitsAux o n e.succ = if n = 0 then [] else have h := 64 * 2 ^ e; Ratpoints.Fast.setBitsAux (o + h) (n >>> h) e ++ Ratpoints.Fast.setBitsAux o (n % 2 ^ h) e

def Ratpoints.Fast.setBits (n : Nat) : List Nat

The positions of the bits set in n, in descending order.

Equations

• Ratpoints.Fast.setBits n = Ratpoints.Fast.setBitsAux 0 n ((n.log2 / 64 + 1).log2 + 1)

Families of moduli

def Ratpoints.Fast.baseRow (T : Array (Array Bool)) (m G N r : Nat) : Nat

The row of the modulus m for the residue r of the denominator, for the numerators 0, G, 2G, … and at least N of them, from the table T = Ratpoints.Fast.admitTable c d m: bit j is set when the residues G j and r modulo m allow a point.

Equations

• Ratpoints.Fast.baseRow T m G N r = Ratpoints.Fast.repeatPattern (Ratpoints.Fast.pattern m fun (j : Nat) => T[r]![G * j % m]!) m (Ratpoints.Fast.doublings m N)

structure Ratpoints.Fast.Family : Type

A family of moduli with product M, for the step G of the numerators: an inverse ginv of G modulo M and the rows for the residues r < M of the denominator, for the numerators 0, G, 2G, …: the AND of the rows of its moduli (Ratpoints.Fast.baseRow).

• M : Nat

  The product of the moduli.

• ginv : Nat

  An inverse of the step G modulo M.

• rows : Array Nat

  The rows, for the residues 0, …, M - 1 of the denominator.

def Ratpoints.Fast.mkFamily (G L : Nat) (ts : List (Nat × Array (Array Bool))) : Option Family

The family of the moduli m of the list ts of pairs (m, T), T the table Ratpoints.Fast.admitTable c d m, for the step G and chunks of at most L numerators, if every modulus is positive and G is invertible modulo their product M: its rows have L + 8 M bits, enough for a chunk at every shift below 8 M (Ratpoints.Fast.Family.shift).

Equations

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

def Ratpoints.Fast.Family.shift (F : Family) (a₀ : Int) : Nat

The shift that aligns the rows of the family F with a chunk starting at the numerator a₀: s < 8 F.M with G s ≡ a₀ modulo F.M, the least one plus the multiple of F.M that makes it a multiple of 8 when F.M is odd (F.M ^ 2 ≡ 1 modulo 8), so that the search on byte arrays reads whole bytes of the rows.

Equations

• F.shift a₀ = (a₀ * ↑F.ginv % ↑F.M).toNat + F.M * ((8 - (a₀ * ↑F.ginv % ↑F.M).toNat % 8) * F.M % 8)

The sieve

def Ratpoints.Fast.sieve (rs sh : Array Nat) (o mask : Nat) : Nat

The candidates of a chunk: the mask ANDed with the rows rs[i] shifted by sh[i] + o, in turn; once nothing is left, the rest is skipped.

Equations

• Ratpoints.Fast.sieve rs sh o mask = List.foldl (fun (acc i : Nat) => if (acc == 0) = true then 0 else acc &&& rs[i]! >>> (sh[i]! + o)) mask (List.range rs.size)

def Ratpoints.Fast.classCount (n G ρ : Nat) : Nat

The number of the indices i < n with i % G = ρ.

Equations

• Ratpoints.Fast.classCount n G ρ = (n + G - 1 - ρ) / G

def Ratpoints.Fast.chunks (cnt L : Nat) : List (Nat × Nat)

The chunks of [0, cnt): their starts k L and lengths min L (cnt - k L).

Equations

• Ratpoints.Fast.chunks cnt L = List.map (fun (k : Nat) => (k * L, min L (cnt - k * L))) (List.range ((cnt + L - 1) / L))

def Ratpoints.Fast.slots (H G L : Nat) : List (Nat × Int × Nat)

The chunks of the search, class by class: for the numerators x with x + H ≡ ρ modulo G, each chunk as the residue of its numerators modulo G, its first numerator a₀ and its length len, for the numerators a₀, a₀ + G, …, a₀ + (len - 1) G.

Equations

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

def Ratpoints.Fast.chunkPoints (c : List Int) (d G : Nat) (rs sh : Array Nat) (o : Nat) (a₀ : Int) (len b : Nat) : List (Int × Int × Int)

The points with the denominator b in the chunk of len numerators a₀, a₀ + G, …, by the sieve with the rows rs of b and the shifts sh moved by o.

Equations

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

The region

def Ratpoints.Fast.sturmIntervals (c : List Int) (d H depth : Nat) : Option (Array (Double × Double))

The intervals of x that the Sturm step of ratpoints (Ratpoints.Sturm.computeSturm) keeps at the depth depth of the whole line, outside of which F(x, 1) < 0 assuming Sturm's theorem; none, no restriction, when the step does not apply (the degree 0 or at least 2 ^ 57, a height of at least 2 ^ 63, a depth beyond 55, or a polynomial that is not squarefree).

Equations

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

def Ratpoints.Fast.endFrac (H : Nat) (x : Double) : Option (Int × Nat)

An end of an interval of the region, for the numerators of absolute value at most H: the exact value n / q of the double in lowest terms (q a power of 2) when it is finite and of absolute value at most H, else H + 1 or -(H + 1) by its sign (an infinity too), which bound the values a / b with |a| ≤ H and b ≥ 1 as the end does, so that an interval beyond H keeps no numerator; none, read by Ratpoints.Fast.numRange as no bound, only for a NaN.

Equations

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

def Ratpoints.Fast.region (c : List Int) (d H depth : Nat) : Option (Array (Option (Int × Nat) × Option (Int × Nat)))

The region of the search, for the numerators of absolute value at most H: the intervals of Ratpoints.Fast.sturmIntervals with their ends as in Ratpoints.Fast.endFrac.

Equations

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

def Ratpoints.Fast.numRange (H b : Nat) (iv : Option (Int × Nat) × Option (Int × Nat)) : Int × Int

The numerators a with |a| ≤ H and a / b in the interval with the ends iv (as in Ratpoints.Fast.endFrac, an end none bounding nothing), from the first to the last; an end beyond H gives its bound without the product with b, which would leave the small integers.

Equations

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

def Ratpoints.Fast.bounds (H b : Nat) (reg : Option (Array (Option (Int × Nat) × Option (Int × Nat)))) : Option (Int × Int)

The numerators of the denominator b to search: from the first to the last a with |a| ≤ H and a / b in one of the intervals of reg (none when there is none), or all of -H, …, H without a region.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Fast.bounds H b none = some (-↑H, ↑H)

@[inline]

def Ratpoints.Fast.part (G : Nat) (lo hi a₀ : Int) (len : Nat) : Option (Nat × Nat)

The part of the chunk of the len numerators a₀, a₀ + G, … that holds those from lo to hi, from the 64-bit word of the first to the end of the word of the last, or the whole chunk when that part leaves out fewer than len / 4 of its numerators (none when there is none): the bits t₁, …, t₁ + len₁ - 1 of the chunk as the pair (t₁, len₁), t₁ a multiple of 64.

Equations

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

def Ratpoints.Fast.partPoints (c : List Int) (d G : Nat) (rs sh : Array Nat) (lo hi a₀ : Int) (len b : Nat) : List (Int × Int × Int)

The points with the denominator b in the part of the chunk of the len numerators a₀, a₀ + G, … that holds those from lo to hi (Ratpoints.Fast.part), by the sieve with the rows rs of b and the shifts sh of the chunk moved by the offset of the part.

Equations

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

def Ratpoints.Fast.denPoints (c : List Int) (d H G : Nat) (fams : Array Family) (reg : Option (Array (Option (Int × Nat) × Option (Int × Nat)))) (sl : List (Nat × Int × Nat × Array Nat)) (b : Nat) : List (Int × Int × Int)

The points with the denominator b in the chunks sl, each given by its residue modulo G, its first numerator a₀, its length and the shifts of the families fams to a₀, by the sieve with the rows of b and the region reg: none when the row of b of some family is 0, which clears every chunk; else the chunks whole when the numerators of b in the region (Ratpoints.Fast.bounds) are all of -H, …, H, else their parts that hold these numerators (Ratpoints.Fast.partPoints).

Equations

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

def Ratpoints.Fast.search (c : List Int) (d H G L : Nat) (fams : Array Family) (reg : Option (Array (Option (Int × Nat) × Option (Int × Nat)))) (dens : List Nat) : List (Int × Int × Int)

The points with the denominators dens (all positive), by the sieve with the step G, chunks of at most L numerators, the families fams and the region reg: for each denominator b, the chunks of the classes that the residue of b modulo G allows (Ratpoints.Fast.admitTable modulo G; these chunks are listed once for each residue), cut to the numerators of b in the region (Ratpoints.Fast.denPoints).

Equations

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

The denominators

def Ratpoints.Fast.isSquare (k : Nat) : Bool

Whether k is a square.

Equations

• Ratpoints.Fast.isSquare k = (k.sqrt * k.sqrt == k)

def Ratpoints.Fast.jacobiNatAux : Nat → Nat → Nat → Int → Int

The Jacobi symbol (a / n) times s for odd n, by Euclid's algorithm in at most fuel steps: the factors 2 of a are taken out with the sign of (2 / n), and for odd a the symbol becomes (n % a / a) with the sign of the reciprocity. The value is 0 when a and n have a common factor, and also when the steps run out, which they do not for n < 2 ^ 64 and fuel = 256; only the value -1 is used (Ratpoints.Fast.forbiddenDens).

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Fast.jacobiNatAux 0 x✝² x✝¹ x✝ = 0

def Ratpoints.Fast.jacobiNat (a n : Nat) : Int

The Jacobi symbol (a / n) for odd n (Ratpoints.Fast.jacobiNatAux), or 0.

Equations

• Ratpoints.Fast.jacobiNat a n = Ratpoints.Fast.jacobiNatAux 256 (a % n) n 1

@[irreducible]

def Ratpoints.Fast.markMultiples (a : ByteArray) (n j hi : Nat) : ByteArray

a with the bytes j, j + n, j + 2 n, … up to hi set to 1.

Equations

• Ratpoints.Fast.markMultiples a n j hi = if j ≤ hi ∧ 0 < n then Ratpoints.Fast.markMultiples (a.set! j 1) n (j + n) hi else a

@[irreducible]

def Ratpoints.Fast.forbiddenDensFrom (lc : Int) (hi : Nat) (comp forb : ByteArray) (p : Nat) : ByteArray

The loop of Ratpoints.Fast.forbiddenDens over the odd numbers from p to hi, with the odd composites marked in comp and the forbidden denominators in forb so far: an unmarked p is a prime, whose odd multiples from p ^ 2 on are marked composite, and whose multiples are marked forbidden when (lc / p) = -1.

Equations

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

def Ratpoints.Fast.forbiddenDens (lc : Int) (hi : Nat) : ByteArray

The denominators up to hi that no point of a curve of even degree with the leading coefficient lc can have, marked 1: the multiples of an odd p with (lc / p) = -1 (Ratpoints.Fast.jacobiNat), p running over the odd primes up to hi, found by the sieve of Eratosthenes along the way (which p are tried affects the speed only).

Equations

• Ratpoints.Fast.forbiddenDens lc hi = Ratpoints.Fast.forbiddenDensFrom lc hi { data := Array.replicate (hi + 1) 0 } { data := Array.replicate (hi + 1) 0 } 3

def Ratpoints.Fast.collectMarked (m : ByteArray) (v : UInt8) (lo : Nat) : Nat → List Nat → List Nat

The numbers b from max lo 1 to n with m[b] = v, in ascending order, before acc.

Equations

• Ratpoints.Fast.collectMarked m v lo 0 x✝ = x✝
• Ratpoints.Fast.collectMarked m v lo b.succ x✝ = if b + 1 < lo then x✝ else Ratpoints.Fast.collectMarked m v lo b (if (m[b + 1]! == v) = true then (b + 1) :: x✝ else x✝)

@[irreducible]

def Ratpoints.Fast.markSquares (a : ByteArray) (s k hi : Nat) : ByteArray

a with the bytes s j ^ 2 ≤ hi for j from k on (and j ≤ hi) set to 1.

Equations

• Ratpoints.Fast.markSquares a s k hi = if k ≤ hi ∧ s * k * k ≤ hi then Ratpoints.Fast.markSquares (a.set! (s * k * k) 1) s (k + 1) hi else a

def Ratpoints.Fast.squareDens (n hi : Nat) : ByteArray

The numbers s k ^ 2 ≤ hi with s dividing n and k ≥ 1, marked 1 (for n ≥ 1).

Equations

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

def Ratpoints.Fast.denominators (c : List Int) (d H : Nat) (bLow bHigh : Int) : List Nat

The denominators of the search, for the degree d, the height bound H and the range of bLow and bHigh: those b with max 1 bLow ≤ b ≤ H, and b ≤ bHigh unless bHigh < 1; for odd d only those of the form s k ^ 2 with s dividing the leading coefficient (Ratpoints.Fast.squareDens), for even d those that Ratpoints.Fast.forbiddenDens does not mark (all of them when the leading coefficient is a positive square, which Ratpoints.Fast.forbiddenDens would not mark); in ascending order.

Equations

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

The choice of the parameters

def Ratpoints.Fast.density (m : Nat) (T : Array (Array Bool)) : Nat

The fraction, in thousandths, of the pairs of residues modulo m that allow a point, from the table T = Ratpoints.Fast.admitTable c d m.

Equations

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

def Ratpoints.Fast.groupModuli (Mmax : Nat) : List (Nat × Array (Array Bool)) → List (List (Nat × Array (Array Bool)))

The pairs (m, T) grouped into families: in ascending order of m, each family taking moduli while their product stays at most Mmax.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Fast.groupModuli Mmax [] = []

structure Ratpoints.Fast.Config : Type

The parameters of the search: the step G, the chunk length L and the families, the most selective first.

• G : Nat

  The step of the numerators in a chunk, a power of 2.

• L : Nat

  The largest number of numerators in a chunk.

• fams : Array Family

  The families.

def Ratpoints.Fast.candidateModuli : List Nat

The moduli that the sieve may use.

Equations

• Ratpoints.Fast.candidateModuli = [9, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 101, 103, 107, 109, 113, 127]

def Ratpoints.Fast.furtherModuli : List Nat

The further moduli, for the searches in which many candidates are expected to survive the moduli of Ratpoints.Fast.candidateModuli (Ratpoints.Fast.takeModuli).

Equations

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

def Ratpoints.Fast.takeModuli (c : List Int) (d κ : Nat) : List Nat → Nat → List (Nat × Array (Array Bool))

The moduli m of ms with their tables Ratpoints.Fast.admitTable c d m, taken in turn while 64 m ^ 2 ≤ κ E, E the expected number of candidates that survive the moduli taken so far (each taken modulus keeps the share of them given by the density of its table): a modulus pays for its table, of cost about m ^ 2, only while many candidates are left.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Fast.takeModuli c d κ [] x✝ = []

structure Ratpoints.Fast.Tuning : Type

Settings of the choice of the parameters (for tuning): the step G, the largest chunk length, the largest product of a family, the weight of the choice of the moduli and the depth of the Sturm step; 0 for the default.

• G : Nat

  The step.

• L : Nat

  The largest chunk length.

• Mmax : Nat

  The largest product of the moduli of a family.

• further : Nat

  The weight κ of Ratpoints.Fast.takeModuli.

• sturm : Nat

  The depth of the Sturm step (Ratpoints.Fast.region).

def Ratpoints.Fast.orDefault (x dflt : Nat) : Nat

x, or dflt when x = 0.

Equations

• Ratpoints.Fast.orDefault x dflt = if x = 0 then dflt else x

def Ratpoints.Fast.moduliTables (tu : Tuning) (c : List Int) (d H B : Nat) : List (Nat × Array (Array Bool))

The moduli of the sieve with their tables, for the coefficients c of degree d, the height bound H and B denominators: those of Ratpoints.Fast.candidateModuli and then of Ratpoints.Fast.furtherModuli that the expected number of survivors pays for (Ratpoints.Fast.takeModuli, from the (2 H + 1) B candidates).

Equations

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

def Ratpoints.Fast.sortedGroups (tu : Tuning) (c : List Int) (d H B : Nat) : List (List (Nat × Array (Array Bool)))

The moduli of Ratpoints.Fast.moduliTables grouped into families (Ratpoints.Fast.groupModuli), the most selective first.

Equations

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

def Ratpoints.Fast.choose (tu : Tuning) (c : List Int) (d H B : Nat) : Config

The parameters for the coefficients c of degree d, the height bound H and B denominators. The chunk length is tu.L (by default 8192), but at most the number of numerators of a class rounded up to a multiple of 64: by default a multiple of 64, so that the rows of the families are long enough at every shift for the fast path of Ratpoints.Mask.andRows in Ratpoints.FastMask.choose, which makes the same choice.

Equations

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

The search

def Ratpoints.Fast.sievePoints (c : List Int) (H : Nat) (bLow bHigh : Int) (tu : Tuning := { }) : List (Int × Int × Int)

The normalized points of height at most H on y ^ 2 = F(x, z) whose denominator z is 0 or lies in the range of bLow and bHigh (bLow ≤ z, and z ≤ bHigh unless bHigh < 1), each once: the points at infinity, then those that the sieve finds (only such points in any case, and all of them assuming Sturm's theorem, on which the region of the numerators rests).

Equations

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

def Ratpoints.Fast.reversed (c : List Int) (H : Nat) (bLow bHigh : Int) : List Int × Bool

The coefficients to search with and whether they are reversed: the reversed coefficients when the reversal check of ratpoints (Ratpoints.Setup.reversal) reverses them and no range of the denominators restricts the search (bLow ≤ 1, and bHigh < 1 or H ≤ bHigh); otherwise, the refusal of the check included, c itself.

Equations

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

def Ratpoints.Fast.fastPoints (c : List Int) (H : Nat) (bLow bHigh : Int) (tu : Tuning := { }) : List (Int × Int × Int)

The normalized points of height at most H on y ^ 2 = F(x, z) whose denominator z is 0 or lies in the range of bLow and bHigh (bLow ≤ z, and z ≤ bHigh unless bHigh < 1), each once: those of Ratpoints.Fast.sievePoints, on the coefficients reversed as ratpoints reverses them when no range of the denominators is given (Ratpoints.Fast.reversed; the binary form with x and z exchanged), with the points mapped back by Ratpoints.Sieve.swapPoint (only such points in any case, and all of them assuming Sturm's theorem, on which the region of the numerators rests).

Equations

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