The cost model of the choice of the moduli

ratpoints chooses the moduli of its sieve and the cut points of its stages from the curve, by a model of what each modulus costs and what it says (sieving_info, Ratpoints.sievingInfo): the candidates are ranked by their keys, what a modulus costs per word swept divided by what it says, -log r for its density r; the first stage takes them while the survivors per word that the next one removes are worth its cost; the second adds an offset that grows with the length of the run; and the third stage takes further primes while the survivors they remove are worth the denominators they are carried through. This module holds the arithmetic of that model, in doubles, expression by expression as the C code computes them: the record of a candidate and its two orders, the costs and keys, the cost of the exact check, the rule that ends the first stage, the offset of the second, and the estimate of the run (the denominators, the words and the calls of the sieve) with the mean number of bits per word of the bit arrays. The composite moduli and the stages of the choice call them (Ratpoints.addModuli, Ratpoints.takeEntries, Ratpoints.rankSecond), and so do the choice (Ratpoints.sievingInfo) and the search (Ratpoints.searchPoints).

The doubles are Lean's Float, IEEE 754 binary64 with the arithmetic of the platform: +, -, *, / and sqrt correctly rounded, as the C code compiled without fused multiply-adds and without -ffast-math computes them; ceil and floor, which are exact, computed by the C library of the platform, where ratpoints computes them inline (gcc's roundsd under -mavx2); and log and pow the functions of the C library of the platform that the Lean runtime binds, on glibc an older symbol version of the routines that ratpoints binds (log@GLIBC_2.2.5 and pow@GLIBC_2.2.5, where ratpoints binds log@GLIBC_2.29 and pow@GLIBC_2.29), which give the same values on every argument that occurs here (x ≥ 0 for log, and for pow a base in [0, 1] and a positive exponent, pow(+0, y) = +0 for y > 0 in both) and differ only in errno and in the sign of the NaN of the logarithm of a negative number. glibc's log and pow are not correctly rounded and choose between variants by the processor, so that the choice of ratpoints and that of the model depend on the machine, and agree on one machine. Every expression keeps the order of the operations of the C code, and every comparison is the C code's; no fact about the values is needed by the theorems, which hold for every choice.

Main definitions

• Ratpoints.ModulusCandidate, Ratpoints.ModulusCandidate.keyLe, Ratpoints.ModulusCandidate.rLe, Ratpoints.sortFrom: a candidate modulus of the ranking, its two orders and the stable sort of the tail of the pool.
• Ratpoints.checkCost, Ratpoints.primeCost, Ratpoints.primeKey, Ratpoints.phase1Key: the cost of one exact check, the cost and the key of a modulus, and the key of the first stage.
• Ratpoints.downstreamFactor, Ratpoints.phase1Wants, Ratpoints.primesForPhase1, Ratpoints.phase2Offset: the rule that ends the first stage and the offset of the second.
• Ratpoints.ShapeArgs, Ratpoints.RunEstimate, Ratpoints.runShape: the estimate of the run.
• Ratpoints.meanBitsPerWord: the mean number of bits per word of the bit arrays of the run.

The candidates

structure Ratpoints.ModulusCandidate : Type

A candidate modulus of the ranking of sieving_info, the record entry of the C code: its density r, its key, the cost the key was made from, the modulus p, the mask of the indices of the primes it involves (a prime from the 65th of the table on is in no mask), its sieve entry, made for a prime by its examination and for a composite modulus when the ranking takes it, the count of its factors nf (0 for a prime, -1 for a prime that says only that numerator and denominator are coprime, the number of factors of a composite modulus) and the codes of its factors: the index pn of the prime prime[pn], or Ratpoints.numPrimes plus the index of an examined prime power.

C: find_points.c:147-149

Deviation: a natural number for the long modulus, a UInt64 for the unsigned long mask, an integer for the short count, the codes a list of natural numbers, for the array of RP_MAX_FACTORS shorts, and the sieve entry an option, none for the null pointer.

• r : Float

  The density.

• key : Float

  The key of the ranking.

• cost : Float

  The cost the key was made from.

• p : Nat

  The modulus.

• mask : UInt64

  The mask of the indices of the primes involved.

• ssp : Option Sieve.SieveEntry

  The sieve entry, if made.

• nf : Int

  The count of the factors.

• fac : List Nat

  The codes of the factors.

@[instance_reducible]

instance Ratpoints.instInhabitedModulusCandidate : Inhabited ModulusCandidate

Equations

• Ratpoints.instInhabitedModulusCandidate = { default := Ratpoints.instInhabitedModulusCandidate.default }

def Ratpoints.ModulusCandidate.keyLe (a b : ModulusCandidate) : Bool

The order of the ranking by keys, compare_entries: a before b unless a.key - b.key > 0, the test of the merge sort of qsort that the comparison is at most 0. On keys that are finite or +∞, never a NaN, it is a total preorder, ∞ - ∞ a NaN that compares as a tie.

C: find_points.c:1194-1198

Deviation: the test of the merge sort, whether the comparison is at most 0, for the comparison of the C code, which returns 1, -1 or 0.

Equations

• a.keyLe b = !decide (a.key - b.key > 0.0)

def Ratpoints.ModulusCandidate.rLe (a b : ModulusCandidate) : Bool

The order by density, compare_by_r: a before b unless a.r - b.r > 0.

C: find_points.c:1202-1206

Deviation: the test of the merge sort, whether the comparison is at most 0, for the comparison of the C code, which returns 1, -1 or 0.

Equations

• a.rLe b = !decide (a.r - b.r > 0.0)

def Ratpoints.sortFrom (pool : Array ModulusCandidate) (s : Nat) (le : ModulusCandidate → ModulusCandidate → Bool) : Array ModulusCandidate

The pool pool with its entries from the position s on sorted by the order le, stably, as qsort(&prec[s], pnp - s, sizeof(entry), cmp) sorts them.

It models no C code of its own: it is the call of qsort at the four places where sieving_info sorts. Lean's List.mergeSort is a stable merge sort, as glibc's qsort is on the records of the ranking when it can allocate its buffer, which it always can in the model, where no allocation fails (glibc falls back to a sort that is not stable when malloc fails), and the orders are total preorders on the keys and densities that occur, so that every stable sort gives the same order, also on ties (-C 0, -C inf).

Equations

• Ratpoints.sortFrom pool s le = pool.extract 0 s ++ ((pool.extract s).toList.mergeSort le).toArray

Costs and keys

def Ratpoints.checkCost (c : List Int) (d H : Nat) (field : Float) : Id Float

What one exact check costs on the curve of degree d with the coefficient list c, for the height bound H, in the units of Ratpoints.checkReference: the value field of -W when it is positive; else, with hbits = log(H + 1) / log 2 and cbits the largest bit length of a nonzero coefficient, at least 1, the bits fbits = cbits + d hbits of F(a, b), its limbs limbs = fbits / 64, the mean limbs mid = 0.5 (cbits + fbits) / 64 over Horner's rule, the limbs root = max(1, ⌈0.5 limbs⌉) of the square root, and the cost d (CHECK_STEP + CHECK_LIMB mid) + CHECK_CALL + CHECK_ROOT (root - 1), with CHECK_STEP + CHECK_LIMB limbs more for odd d.

C: find_points.c:1285-1318

Deviation: the coefficients, the degree and the height bound as arguments, for the fields of the arguments that check_cost reads; log the function of the C library of the platform that the Lean runtime binds (Float.log), on glibc an older symbol version of the routine that ratpoints binds, which gives the same values on every argument that occurs here, and which glibc does not round correctly and chooses by the processor, so that the value is that of the C program on the same machine; log 2 computed at run time, where gcc folds log(2.0) into the same double; ceil the function of the C library of the platform (Float.ceil), which is exact, where gcc compiles an instruction; the bit length of |c_k| (Nat.log2 + 1) for mpz_sizeinbase(c_k, 2), which it is for c_k ≠ 0; 64 for LONG_LENGTH.

Equations

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

def Ratpoints.primeCost (p : Nat) (perWord : Float) (tabled : Bool) (ct U D : Float) : Float

What one more modulus p costs the sieve per word swept, in units of an and of the first stage, for the run of U words and D denominators: perWord, the part paid for every word, plus COST_BP D / U for its entry of bp_list, and for a modulus of the first two stages (tabled) COST_SETUP D / U for its sieve spec and, for a positive cost ct of a row of a table, ct p min(D, p) / U for its table.

C: find_points.c:1220-1235

Equations

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

def Ratpoints.primeKey (r : Float) (p : Nat) (perWord : Float) (tabled : Bool) (ct U D : Float) : Float

The key of a modulus p of density r: its cost (Ratpoints.primeCost) divided by what it says, info = -log r, and 10 ^ 300 when info ≤ 0.

C: find_points.c:1241-1247

Deviation: log the function of the C library of the platform that the Lean runtime binds (Float.log), on glibc an older symbol version of the routine that ratpoints binds, which gives the same values on every argument that occurs here, and which glibc does not round correctly and chooses by the processor, so that the value is that of the C program on the same machine.

Equations

• Ratpoints.primeKey r p perWord tabled ct U D = if -r.log ≤ 0.0 then 10e299 else Ratpoints.primeCost p perWord tabled ct U D / -r.log

def Ratpoints.phase1Key (ct U D cc : Float) (e : ModulusCandidate) : ModulusCandidate

The candidate e with its key for the first stage and the cost it was made from, for the cost ct of a row of a table, the run of U words and D denominators and the cost cc of the calls of the sieve per word: the cost of a modulus of the first stage (Ratpoints.primeCost with the cost 1 per word) plus cc plus COST_LINE walk (32 / 64) D / U for the part of its row that a denominator walks, walk = min(p, U / (4 D)) bit arrays of 32 bytes; the key that cost divided by -log r, or 10 ^ 300 when that is not positive.

C: find_points.c:1256-1270

Deviation: log the function of the C library of the platform that the Lean runtime binds (Float.log), on glibc an older symbol version of the routine that ratpoints binds, which gives the same values on every argument that occurs here, and which glibc does not round correctly and chooses by the processor, so that the value is that of the C program on the same machine; the candidate returned with its key and cost, for the fields of the record that phase_1_key sets; Ratpoints.rbaPack for RBA_PACK and 8 Ratpoints.rbaPack for the size of a bit array in bytes.

Equations

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

The first two stages

def Ratpoints.downstreamFactor (pool : Array ModulusCandidate) (n pnp extra : Nat) : Id Float

What a word that survives the first stage costs from the candidate n of the pool on, relative to what it costs in a long run: the next extra candidates (as far as the pool goes) and the survivor that is left, COST_PHASE2 for each and per surviving word and COST_SURVIVOR per survivor, cost (1 - ρ) / COST_PHASE2 with ρ the geometric mean of the densities of the next Ratpoints.sp2Extra candidates (the density of n when there are none), at least 1.

C: find_points.c:1539-1561

Deviation: pow the function of the C library of the platform that the Lean runtime binds (Float.pow), on glibc an older symbol version of the routine that ratpoints binds, which gives the same values on every argument that occurs here, and which glibc does not round correctly and chooses by the processor, so that the value is that of the C program on the same machine; natural numbers for the long positions, the comparisons with the candidates left after n made on integers.

Equations

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

def Ratpoints.phase1Wants (pool : Array ModulusCandidate) (n pnp taken : Nat) (bpw rate target : Float) (extra : Nat) : Id Bool

The rule that ends the first stage: the candidate n of the pool of pnp candidates is taken when it is the first (taken = 0), or when the survivors per word it removes, bpw rate (1 - r), weighted by what they cost downstream (Ratpoints.downstreamFactor), exceed the target times its cost.

C: find_points.c:1583-1589

Equations

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

def Ratpoints.primesForPhase1 (pool : Array ModulusCandidate) (bpw target : Float) (extra : Nat) : Id Nat

How many candidates of the pool, sorted by keys, the first stage would take by its rule (Ratpoints.phase1Wants, with the product of the densities so far): the first that it refuses, or all of them, at least 1.

C: find_points.c:1598-1609

Equations

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

def Ratpoints.phase2Offset (extra : Nat) (u0 U : Float) : Nat

How many moduli the second stage adds to the first, for the offset extra of a long run, the scale u0 and the run of U words: for u0 ≤ 0 or U ≤ 0 the offset itself, capped at most = Ratpoints.numPrimes + Ratpoints.maxModuli; else e = extra / (1 + u0 / U) rounded to the nearest integer when below most, and most otherwise.

C: find_points.c:1619-1626

Deviation: natural numbers for the longs, which are not negative here; the conversion of e + 0.5 to a long, which truncates, by Float.toUInt64, which truncates e + 0.5 < most as well.

Equations

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

The estimate of the run

def Ratpoints.numeratorsFor (domain : List (Double × Double)) (b H : Float) : Id (Float × Float × Float × Float)

The numerators that the denominator b considers, for the height bound H, as doubles: over the search intervals domain, the interval [b l, b u] clipped to [-H, H], its width added when it is not empty, with the number of such intervals and of their ends that the height bound cut, below and above.

C: find_points.c:1836-1854

Deviation: the search intervals as an argument, for the fields domain and num_inter of the arguments, their ends doubles by their bits (Ratpoints.Double.toFloat); the sum and the three counts returned, the counts as doubles, as the C code hands them back through its pointers.

Equations

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

def Ratpoints.clippedPadding (cl : Sieve.NumClass) (H : Nat) (padLo padHi : Float) : Float × Float

The sums padLo and padHi with what the rounding of an interval to whole bit arrays adds at an end that the height bound H cut, for the class cl of the stride 2 ^ k and the residue a₀: the first bit lo = -(⌊(H - 2 ^ k + a₀) / 2 ^ k⌋ + 1) and minus the one past the last, hi = -⌊(H - a₀) / 2 ^ k⌋ - 1, each modulo Ratpoints.rbaLength.

C: find_points.c:1863-1876

Deviation: the two sums passed and returned, for the pointers; integers for the longs, the arithmetic shifts as divisions that round down and the masks by RBA_LENGTH - 1 as Euclidean remainders.

Equations

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

def Ratpoints.forbiddenFraction (p mask : Nat) : Id Float

The fraction of the integers b whose valuation at p is in the set that mask describes, bit m for v_p(b) = m: the sum of (1 / p ^ m) (1 - 1 / p) over the bits m ≥ 1 of the mask, while m < 64 and bits are left.

C: find_points.c:1926-1937

Deviation: natural numbers for the long and the unsigned long mask; 64 for LONG_LENGTH.

Equations

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

structure Ratpoints.ShapeArgs : Type

What the estimate of the run reads of the search: the shape of the denominators (the squares, the divisors of the leading coefficient times squares, or every denominator), whether the Jacobi test runs, the height bound, the range of the denominators, the search intervals, the word of the classes of the denominators modulo 64 that admit a numerator, the classes, and the array size.

It models no C code of its own: a structure for the fields of the arguments and the arguments of run_shape and mean_bits_per_word that describe the run (find_points.c:1939-1943, find_points.c:2134-2136), the bits RATPOINTS_USE_SQUARES, RATPOINTS_USE_SQUARES1 (with args->divisors) and RATPOINTS_USE_JACOBI of the flags as Booleans and an option, natural numbers for the longs, and the array size normalized for the height bound (Ratpoints.arraySizeAt).

• useSquares : Bool

  Whether the denominators are the squares.

• divisors : Option (List Nat)

  The divisors of the leading coefficient, when the denominators are those times squares.

• useJacobi : Bool

  Whether the Jacobi test runs.

• H : Nat

  The height bound.

• bLow : Nat

  The least denominator.

• bHigh : Nat

  The largest denominator.

• domain : List (Double × Double)

  The search intervals.

• db : UInt64

  The word den_bits of the classes that admit a numerator.

• cls : Vector Sieve.NumClass 64

  The classes of the denominators modulo 64.

• arraySize : Nat

  The array size, normalized for the height bound.

structure Ratpoints.ShapeAcc : Type

The local variables of run_shape: the fraction keep of the candidates that reach the sieve, the candidate denominators, the numerators they sweep, their nonempty intervals and the ends of those that the height bound cut, the classes kept, the sum of their shares 2 ^ -k and the sums of what a cut end pads.

C: find_points.c:1945-1957

Deviation: a structure for the local variables, with their initial values.

• keep : Float

  The fraction of the candidates that reach the sieve.

• count : Float

  The candidate denominators.

• nums : Float

  The numerators they sweep.

• inters : Float

  Their nonempty intervals.

• clo : Float

  The ends that the height bound cut below.

• chi : Float

  The ends that the height bound cut above.

• good : Nat

  The classes kept.

• packed : Float

  The sum of the shares of their numerators.

• padLo : Float

  The sum of what a cut end pads below.

• padHi : Float

  The sum of what a cut end pads above.

structure Ratpoints.RunEstimate : Type

The estimate of the run: the denominators it sifts, the words it sweeps, padding included, of which padding, and the calls of the sieve.

It models no C code of its own: a structure for the four results that run_shape hands back through its pointers (find_points.c:1942-1943).

• denoms : Float

  The denominators sifted, run_denoms.

• words : Float

  The words swept, run_words.

• pad : Float

  Of these, the padding to whole bit arrays, u_pad.

• calls : Float

  The calls of the sieve, n_calls.

def Ratpoints.sampleSteps (domain : List (Double × Double)) (H lo hi : Float) (square : Bool) (acc : ShapeAcc) : Id ShapeAcc

The accumulators acc with the denominators lo, …, hi of the steps k (the squares k ^ 2 for square, the denominators themselves otherwise): count = hi - lo + 1 when hi ≥ lo, and the numerators, intervals and cut ends of the 64 midpoint samples k = lo + (hi - lo)(i + 0.5) / 64 (Ratpoints.numeratorsFor), each sum scaled by count / 64.

C: find_points.c:1964-1973, find_points.c:2028-2037

Deviation: one function for the samples of the squares and of every denominator, which the C code writes out twice.

Equations

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

def Ratpoints.addClass (cl : Sieve.NumClass) (H : Nat) (acc : ShapeAcc) : ShapeAcc

The accumulators acc with the class cl kept: one class more, its share 2 ^ -k of the numerators, and what its cut ends pad (Ratpoints.clippedPadding).

C: find_points.c:1980-1981, find_points.c:2017-2018, find_points.c:2045-2046

Deviation: one function for the three places of the C code.

Equations

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

def Ratpoints.shapeSquares (a : ShapeArgs) : Id ShapeAcc

The accumulators of the squares in the range of the denominators: the steps ⌈√bLow⌉, …, ⌊√bHigh⌋ (Ratpoints.sampleSteps), and the classes k ^ 2 mod 64 for k < 32, those with a pattern kept, with keep the share of those kept.

C: find_points.c:1960-1962, find_points.c:1976-1979, find_points.c:1982-1985

Deviation: ceil and floor the functions of the C library of the platform (Float.ceil, Float.floor), which are exact, where gcc compiles instructions.

Equations

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

def Ratpoints.sampleDivisor (domain : List (Double × Double)) (H : Float) (bLow bHigh d : Nat) (acc : ShapeAcc) : Id ShapeAcc

The accumulators acc with the denominators d k ^ 2 of the divisor d, for k = max(1, ⌈√(bLow / d)⌉), …, ⌊√(bHigh / d)⌋: their count c and the numerators, intervals and cut ends of the 64 midpoint samples, each times c / 64.

C: find_points.c:1993-2009

Deviation: ceil and floor the functions of the C library of the platform (Float.ceil, Float.floor), which are exact, where gcc compiles instructions.

Equations

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

def Ratpoints.shapeSquares1 (a : ShapeArgs) (ds : List Nat) : Id ShapeAcc

The accumulators of the divisors ds of the leading coefficient times squares: for each divisor d its denominators (Ratpoints.sampleDivisor) and the classes d k ^ 2 mod 64 for k < 32, those with a pattern kept; keep the share of the classes kept among those tried, when any were.

C: find_points.c:1987-1992, find_points.c:2010-2016, find_points.c:2019-2023

Deviation: the divisors as a list, for the zero-terminated array args->divisors.

Equations

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

def Ratpoints.keepChecked (keep : Float) (checkDenom useJacobi : Bool) (forb : List Sieve.ForbiddenEntry) (forbVal : List Sieve.ForbiddenVal) : Id Float

The share of the denominators that reach the sieve in the shape of every denominator, from the share keep of the classes kept: for the checked loop (checkDenom), times 1 - 1 / p for each forbidden divisor p tested with words, times 1 - f for each tested by its valuations with the fraction f of its excluded valuations (Ratpoints.forbiddenFraction), and times 0.53 when the Jacobi test runs.

C: find_points.c:2051-2065

Deviation: the forbidden divisors as lists, for the arrays of the arguments with their counts fba and fdc.

Equations

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

def Ratpoints.shapeAll (a : ShapeArgs) (checkDenom : Bool) (forb : List Sieve.ForbiddenEntry) (forbVal : List Sieve.ForbiddenVal) : Id ShapeAcc

The accumulators of every denominator in the range: the denominators bLow, …, bHigh (Ratpoints.sampleSteps), the classes of the set bits of den_bits in increasing order, all kept, keep their share of the 64 classes, and that for the checked loop (Ratpoints.keepChecked).

C: find_points.c:2025-2027, find_points.c:2038-2044, find_points.c:2047-2050, find_points.c:2066

Deviation: the set bits of the word visited by the lowest set bit (Ratpoints.Sieve.ctz), as the C code visits them with RP_CTZL.

Equations

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

def Ratpoints.shapeEstimate (asz : Nat) (acc : ShapeAcc) : RunEstimate

The estimate of the run from the accumulators acc and the array size asz: the numerators times the mean share of the classes kept; the padding, what a cut end pads by its class and half a bit array for an end inside the bound; the bit arrays per interval and the calls of the sieve, one per interval and denominator and as many as asz bit arrays take; the denominators keep count, the words keep (nums + pad) / 64, the padding keep pad / 64 and the calls keep inters ⌈per / asz⌉; each at least 1, the padding 0 when the words are floored.

C: find_points.c:2074-2105

Deviation: the estimate returned as a structure, for the four pointers of run_shape; ceil the function of the C library of the platform (Float.ceil), which is exact, where gcc compiles an instruction; 64 for LONG_LENGTH.

Equations

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

def Ratpoints.runShape (a : ShapeArgs) (checkDenom : Bool) (forb : List Sieve.ForbiddenEntry) (forbVal : List Sieve.ForbiddenVal) : Id RunEstimate

How big the run is, as run_shape estimates it before any sieving, for the switch checkDenom of the checked loop and the forbidden divisors forb and forbVal known so far: by the shape (Ratpoints.shapeSquares, Ratpoints.shapeSquares1, Ratpoints.shapeAll), then the estimate (Ratpoints.shapeEstimate).

C: find_points.c:1939-1944, find_points.c:1959, find_points.c:1986, find_points.c:2024, find_points.c:2106

Deviation: the switch checkDenom for the bit RATPOINTS_CHECK_DENOM of the flags, and the forbidden divisors as lists, for the arrays with their counts fba and fdc.

Equations

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

The bits per word

def Ratpoints.popcount (w : UInt64) : Id Nat

The number of the set bits of the word w, __builtin_popcountl.

It models no C code of its own: the builtin of gcc at find_points.c:2129, in the range of Ratpoints.bpwAdd, as a loop over the 64 bits.

Equations

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

def Ratpoints.bpwAdd (cl : Sieve.NumClass) (tot wsum : Float) : Id (Float × Float)

The sums tot and wsum with the class cl, when its pattern has a set bit: its bits per word times its share 2 ^ -k of the numerators, and that share.

C: find_points.c:2128-2132

Deviation: the two sums passed and returned, for the pointers; the number of the set bits of the word a loop over its bits (Ratpoints.popcount), for gcc's builtin __builtin_popcountl.

Equations

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

def Ratpoints.bpwSquares1 (cls : Vector Sieve.NumClass 64) (ds : List Nat) : Id (Float × Float)

The sums of Ratpoints.bpwAdd over the classes that the divisors ds of the leading coefficient times squares visit: the classes d k ^ 2 mod 64 for each divisor d and k < 32.

C: find_points.c:2143-2151

Equations

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

def Ratpoints.meanBitsPerWord (a : ShapeArgs) : Id Float

The mean number of bits set per word of a bit array on entry to the sieve, over the classes of the denominators that the run visits, weighted by the words they sweep: the classes k ^ 2 mod 64 for k < 32 for the squares, those of the divisors for the divisors times squares (Ratpoints.bpwSquares1), and those of the set bits of den_bits otherwise (Ratpoints.bpwAdd); 0 when no class has a pattern.

C: find_points.c:2134-2142, find_points.c:2152-2159

Deviation: the set bits of the word visited by the lowest set bit (Ratpoints.Sieve.ctz), as the C code visits them with RP_CTZL.

Equations

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

Examples