8 The denominators
Before it sieves the numerators of a denominator \(b\) (Chapter 9), ratpoints decides which denominators it sieves at all, in which order, and which numerators modulo \(64\) each class of the denominators modulo \(64\) admits. This chapter describes these choices and proves that none of them loses a point. They are made for the polynomial searched, of degree \(d\) with the coefficients \(c_0, \dots , c_d\), that the set-up hands on (Chapter 4), with its binary form \(F(x, z) = \sum _k c_k x^k z^{D - k}\) of the even degree \(D = 2 \lceil d/2 \rceil \) (Definition 2.1). The lemmas speak of triples \((a, y, b)\) of integers \(a\), \(y\) and a natural number \(b\) with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\), as every point (Definition 2.4) is one, and the denominators range from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\), which are \(1\) and the height bound \(H\) unless the options narrow the range (Definition 2.6).
The 2-adic information says which numerators modulo \(64\) each class of \(b \bmod 64\) admits (Section 8.1). For odd \(d\) the denominator of a point is a squarefree divisor of \(c_d\) times a square (Section 8.2). For even \(d\) ratpoints looks for primes that divide no denominator of a point, or only to certain powers (Section 8.3), and tests the denominators by a Jacobi symbol (Section 8.4). The loop over the denominators takes one of four shapes that combine these tests (Section 8.5). Each test removes only candidates that carry no point; what the tests change is the order of the points, and Section 8.6 proves that the model visits the denominators in the order of the specification (Definition 2.9). The forbidden divisors of the primes examined for the sieve come out of the loop of the tables of the choice of the moduli, which also cuts the loop over the denominators into blocks (Chapter 6); the class of \(b\) gives the sieve its first pattern and the packing of its numerators (Chapter 9).
In the C code, find_points_work_1 sets the flags of the tests (find_points.c:4607-4607, find_points.c:4905-4943): for even \(d\) the checked loop and, when \(c_d\) is not a square and the caller does not forbid it (the option -j of the program), the Jacobi test; for odd \(d\) the squares when \(|c_d| = 1\) and the divisors of setup_us1 otherwise. The model keeps the order of the C code (Ratpoints.searchPoints, Ratpoints.sievingInfo, Ratpoints.Sieve.sieveRun).
8.1 The 2-adic information
Write \(f(x) = F(x, 1)\) and \(\tilde f(t) = F(1, t)\), the reversed polynomial. In a pair \((a, b)\) with \(\gcd (a, b) = 1\), \(a\) or \(b\) is odd. For odd \(b\), \(F(a, b) \equiv b^D f(a b^{-1}) \bmod 64\), where \(b^D\) is the square of a unit since \(D\) is even; for even \(b\), \(a\) is odd and \(F(a, b) \equiv a^D \tilde f(b a^{-1}) \bmod 64\). So two words of \(64\) bits decide which pairs of residues modulo \(64\) can carry a point: the residues \(k\) at which \(f(k)\) is a square modulo \(64\), and the even residues \(t\) at which \(\tilde f(t)\) is one.
The words \(\mathrm{fsq}\) and \(\mathrm{gsq}\), by Horner’s rule on \(64\)-bit words (find_points.c:1006-1014, find_points.c:1015-1021): bit \(k\) of \(\mathrm{fsq}\) is set exactly when \(k {\lt} 64\) and \(\sum _{i \le d} c_i k^i\) is a square in \(\mathbb {Z}/64\), bit \(t\) of \(\mathrm{gsq}\) exactly when \(t {\lt} 64\) is even and \(\sum _{i \le d} c_i t^{D - i}\) is a square in \(\mathbb {Z}/64\). The words \(\mathrm{nb}[b]\) for \(b {\lt} 64\), scattered from these (find_points.c:983-994, find_points.c:1023-1050): bit \(a\) of \(\mathrm{nb}[b]\) is set exactly when \(b\) is odd and \(a = k b \bmod 64\) for a set bit \(k\) of \(\mathrm{fsq}\), or \(a {\lt} 64\) is odd and \(b = t a \bmod 64\) for a set bit \(t\) of \(\mathrm{gsq}\). And \(\mathrm{den\_ bits}\), with bit \(b\) set exactly when \(\mathrm{nb}[b] \ne 0\). These descriptions are the contracts.
By the congruences above, bit \(a\) of \(\mathrm{nb}[b]\) is set exactly when \(a\) or \(b\) is odd and \(F(a, b)\) is a square modulo \(64\).
Let \(a\) and \(y\) be integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). Then bit \(a \bmod 64\) of \(\mathrm{nb}[b \bmod 64]\) is set. So the word of the class of a denominator over which the brute-force reference finds a point is not \(0\); and if \(\mathrm{den\_ bits} = 0\), the curve has no point of any height, the points at infinity included.
For odd \(b\), \(f(k)\) is a square modulo \(64\) at \(k = a b^{-1} \bmod 64\), and the scatter sets bit \(k b \equiv a\) of \(\mathrm{nb}[b \bmod 64]\); for even \(b\), \(\tilde f(t)\) is a square at the even \(t = b a^{-1} \bmod 64\), and the scatter sets bit \(a \bmod 64\) in the word of \(t a \equiv b\) (Ratpoints.isSquare_sum_mul_pow_sub_of_sq_eq_binaryForm and its companion, in any commutative ring); Horner’s rule on \(64\)-bit words is exact modulo \(64\). A point at infinity is a triple \((1, y, 0)\) and also sets a bit of \(\mathrm{den\_ bits}\).
So the 2-adic exit, which ends the search when \(\mathrm{den\_ bits} = 0\) and there is no point at infinity, loses nothing, and its condition on the points at infinity always holds. Since bit \(0\) of \(\mathrm{fsq}\) says that \(c_0\) is a square modulo \(64\) and bit \(0\) of \(\mathrm{gsq}\) that \(c_D\) is one, the exit is taken only for even \(d\) with \(c_0\) and \(c_d\) non-squares modulo \(64\).
The classes of the numerators (Ratpoints.Sieve.numClasses, Definition 9.5) have the pattern \(0\) exactly when their word is \(0\). So the class test of the loop over the denominators, that the pattern of the class of \(b \bmod 64\) is not \(0\), removes no denominator of a point, and the pattern, with which the sieve of \(b\) starts, removes no numerator of a point.
8.2 Odd degree: squares and divisors
For odd \(d\), \(F(a, b) = b\, G(a, b)\) with \(G(a, b) = c_d a^d + b \sum _{k {\lt} d} c_k a^k b^{d-1-k}\). Let \((a, y, b)\) be a triple as above and \(p\) a prime with \(p \nmid c_d\) and \(v_p(b) = m \ge 1\). Then \(p \nmid a\), the term \(c_d a^d b\) of \(F(a, b)\) has the valuation \(m\) at \(p\), and every other term has at least \(2m\). When in a sum \(y^2 = \sum _i f_i\) of integers one term \(p^v u\) with \(p \nmid u\) has a lower valuation than all others, \(v\) is even and \(u\) is a square modulo \(p\) (Int.even_and_exists_isSquare_add_of_sq_eq_sum); so \(m\) is even. Hence \(b = s k^2\) with \(s\) squarefree and \(s \mid c_d\), and \(b\) is a square when \(|c_d| = 1\). For a prime \(p \mid c_d\) there is a second test: when \(v_p(b)\) is large enough, the term \(c_d a^d\) alone has the least valuation in \(G(a, b)\), so that \(v_p(b) + v_p(c_d) = v_p(y^2)\) is even.
The valuation \(v\) of an integer \(n \ne 0\) at \(p\) with the unit part \((|n| / p^v) \bmod p\), by repeated division with remainder, and \((\mathrm{veryBig}, 0)\) for \(n = 0\), with \(\mathrm{veryBig} = 1000\) (find_points.c:422-422): one function for valuation on GMP integers and valuation1 on longs (find_points.c:424-454). The contract: for \(p {\gt} 1\) the loop ends, and for \(n \ne 0\), \(v\) is the \(p\)-adic valuation of \(|n|\) and the unit part is not \(0\).
For odd \(d\) and \(|c_d| \ne 1\), as setup_us1 computes them: the factorization of \(|c_d|\) by trial division over the primes of the table, a cofactor below the square of the next prime taken as a prime (find_points.c:777-860); the squarefree divisors at most \(b_{\mathrm{high}}\) by a doubling loop, at most \(\mathrm{maxDivisors} = 512\) of them (find_points.c:864-880); and for each prime \(p\) of \(c_d\) a record of \(p\), \(v_p(c_d)\) and the slope, the least \(n \ge 1\) with \((d - k)\, n {\gt} v_p(c_d) - v_p(c_k)\) for all \(k {\lt} d\) (find_points.c:894-912). The records and the divisors are returned exactly when the factorization ends with the cofactor \(1\) and there are fewer than \(\mathrm{maxDivisors}\) divisors (find_points.c:914-935). The contracts say so, and: for \(c_d \ne 0\) the factorization ends with the cofactor \(1\) exactly when ratpoints factors \(|c_d|\) completely in the sense of the specification (\(\mathrm{FactorsByTrialDivision}\), Definition 2.9), and then lists the primes of \(|c_d|\) in increasing order with their valuations; the slope satisfies \(n \ge 1\) and \(1 + v_p(c_d) - v_p(c_k) \le (d - k)\, n\) for all \(k {\lt} d\), where \(v_p(0) = \mathrm{veryBig}\); for \(c_d \ne 0\) and \(b_{\mathrm{high}} \ge 1\) the set-up returns divisors exactly when \(|c_d|\) is factored completely and has fewer than \(\mathrm{maxDivisors}\) squarefree divisors at most \(b_{\mathrm{high}}\), and these are then \(\mathrm{binaryDivisors}(|c_d|, b_{\mathrm{high}})\), in its order.
The contract of the factorization rests on the invariant Ratpoints.Setup.FactorLcfInvariant of its loop. By Ratpoints.Setup.foldl_extendDivisors_eq_filter, the doubling loop lists the products at most \(b_{\mathrm{high}}\) of the sublists of the primes, in the order of binary counting, the first prime the lowest bit, or a prefix of them.
Let \(d\) be odd, \(a\) and \(y\) integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\).
- (1)
If \(|c_d| = 1\), then \(b\) is a square.
- (2)
\(b = s k^2\) for a squarefree \(s\) that divides \(c_d\).
- (3)
If \(p\) is a prime with \(v_p(b) \ge 1\) and \(v_p(c_d) + 1 \le v_p(c_k) + (d - k)\, v_p(b)\) for every \(k {\lt} d\) with \(c_k \ne 0\), then \(v_p(c_d) + v_p(b)\) is even. So for \(b \ge 1\) the record of any prime \(p\) with its slope does not exclude \(b\), where a record excludes \(b\) when \(v_p(b)\) is at least the slope and \(v_p(b) + v_p(c_d)\) is odd.
When the set-up returns divisors, for \(c_d \ne 0\) and \(b_{\mathrm{high}} \ge 1\), they are the squarefree divisors of \(c_d\) at most \(b_{\mathrm{high}}\), each once.
Parts (1) and (2) are the argument at the beginning of this section. For (3), \(p \nmid a\), and in \(G(a, b)\) the term \(c_d a^d\) has the valuation \(v_p(c_d)\), every other nonzero term a larger one, so that \(v_p(b) + v_p(c_d) = v_p(y^2)\) is even; when \(v_p(b)\) is at least the slope, the contract of the slope gives the hypothesis. The divisors are \(\mathrm{binaryDivisors}(|c_d|, b_{\mathrm{high}})\), each once (Ratpoints.mem_binaryDivisors_iff, Ratpoints.nodup_binaryDivisors).
8.3 Even degree: the forbidden divisors
For even \(d\), a prime \(p\) and a triple \((a, y, b)\) as above with \(v_p(b) = m \ge 1\), \(p \nmid a\), and the term \(j\) of \(F(a, b) = \sum _{j \le d} c_{d-j}\, a^{d-j} b^j\) has the valuation \(w_j + j m\), where \(w_j = v_p(c_{d-j})\). If one term \(j_0\) alone has the least valuation, that valuation is even, and for even \(j_0\) the unit part \(r_{j_0}\) of \(c_{d-j_0}\) is a square modulo \(p\): the argument of the Newton polygon. A valuation \(m\) at which this fails is one that no denominator of a point has at \(p\). For \(p \nmid c_d\) and \(p \mid b\), further, \(y^2 \equiv c_d a^d \bmod p\) with \(a^d\) the square of a unit; so when \(c_d\) is not a square modulo \(p\), \(p\) divides no denominator of a point. Such primes are the forbidden divisors, of two kinds: primes tested on words of \(64\) denominators at once (Ratpoints.Sieve.ForbiddenEntry), and primes with a mask of excluded valuations (Ratpoints.Sieve.ForbiddenVal).
Let \(d\) be even. The test of a valuation \(m\) at a prime \(p\) is true when, for the valuations \(w_j\) and the unit parts \(r_j\) modulo \(p\), signs included, of the nonzero \(c_{d-j}\), the least \(w_j + j m\) is taken at one \(j_0\) only and is odd, or \(j_0\) is even and \(r_{j_0}\) is not a square modulo \(p\) (find_points.c:2218-2228); the mask of the forbidden valuations at \(p\), a natural number, has bit \(m\) set for the \(m \ge 1\) with \(p^m \le b_{\mathrm{high}}\) that the test excludes (find_points.c:2229-2234). The forbidden divisor of an examined prime \(p\) (find_points.c:2642-2676): for \(p \mid c_d\) and a nonzero mask, \(p\) with its words when the mask holds every \(m \ge 1\) with \(p^m \le b_{\mathrm{high}}\), and \(p\) with its mask otherwise; for \(p \nmid c_d\), \(p\) with its words when \(c_d\) is not a square modulo \(p\), as the entry at infinity of its table says. Then, unless \(c_d\) is a square, the further primes \(p\) of the table, from the first one not examined, with \(p^2 \le b_{\mathrm{high}}\) and \(c_d\) not a square modulo \(p\), with their words, while fewer than \(\mathrm{maxForbidden}\) forbidden divisors are found (find_points.c:2709-2772). The contracts: a true test means that one term of least valuation excludes \(m\), and the mask is as described. A forbidden divisor is admissible when it is the forbidden divisor of a prime of the table, made from the residues of the coefficients and the entry at infinity of its table, or, with words, a prime of the table with its words and its reciprocal at which \(c_d\) is not a square; from admissible entries the further primes add only admissible ones, whatever the cap.
The words of a prime \(p\) are those of Ratpoints.Sieve.forbiddenRow, \(p\) words with bit \(j\) of word \(r\) clear exactly when \(p \mid 64 r + j\), read from the generated pattern sieves0 for the first \(\mathrm{numPrimes}\) primes of the table and made as sieving_info makes them for the others (Ratpoints.Sieve.extract_sieves0). For even \(d\), and while fewer than \(\mathrm{maxForbidden}\) forbidden divisors have been found, the loop of the tables records the forbidden divisor of each examined prime (find_points.c:2624-2626); these are admissible (Ratpoints.Sieve.isForbiddenEntry_of_run_examinePrime?_eq_some and its companion), so that the choice of the moduli hands on admissible forbidden divisors only (Ratpoints.IsSievingInfo, Chapter 6).
Let \(d\) be even, \(a\) and \(y\) integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). For every prime \(p\) and every \(b_{\mathrm{high}}\), bit \(v_p(b)\) of the mask of the forbidden valuations at \(p\) is clear. An admissible forbidden divisor with words has the words of Ratpoints.Sieve.forbiddenRow, and for \(1 \le b \le b_{\mathrm{high}}\) its prime does not divide \(b\); and for \(b \ge 1\) no admissible forbidden divisor with a mask excludes \(b\).
The first statement is the Newton polygon at \(p\) (Ratpoints.even_and_isSquare_of_sq_eq_binaryForm_of_even), from the statement on a sum with one term of least valuation; bit \(0\) is never set. A prime with words from a mask has every valuation up to \(b_{\mathrm{high}}\) excluded; one with \(p \nmid c_d\) divides no denominator of a point by the congruence above, the entry at infinity of its table saying, for even \(d\), whether \(c_d\) is a square modulo \(p\).
8.4 The Jacobi test
For even \(d\), an odd prime \(q \mid b\) with \(q \nmid c_d\) makes \(c_d\) a square modulo \(q\), by the congruence of Section 8.3. So for the largest divisor \(b^*\) of \(b\) prime to \(2 c_d\), the Jacobi symbol \(J(c_d \mid b^*)\) is \(1\): the test rejects every denominator with an odd number of prime factors, counted with multiplicity, at which \(c_d\) is not a square. The C code computes the symbol by a binary algorithm or, when the leading coefficient allows it, by tables of the non-squares modulo its odd primes and quadratic reciprocity.
The binary algorithm (find_points.c:498-566, find_points.c:568-641) for \(b \ge 1\) and an integer \(\ell \): subtraction and halving on \(\ell \bmod b\) and \(b\), with the signs of \(J(2 \mid m)\) and of the reciprocity, the gcd divided out of \(b\) when it is not \(1\). Its contract: the result is \(J(\ell \mid b^*)\), where \(b^*\) is the largest divisor of \(b\) prime to \(2\ell \). The tables (find_points.c:683-708), for \(\ell = \pm 2^v \prod _i q_i^{e_i}\) and \(b_{\mathrm{high}} \le \mathrm{mulModLimit} = 2^{32} - 1\): the odd primes \(q_i\), at most \(\mathrm{jacobiPrimes} = 16\), each with its reciprocal and, for odd \(e_i\), the table of the non-squares modulo \(q_i\), at most \(\mathrm{jacobiTable} = 8192\) entries in all; and the sign for each \(b^* \bmod 8\), the product of \(J(-1 \mid b^*)\) for negative \(\ell \), \(J(2 \mid b^*)^v\) and the signs of the reciprocity of the \(q_i \equiv 3 \bmod 4\) with odd \(e_i\); none when a prime of \(\ell \) lies beyond the table or a bound is passed. The test of \(b\) (find_points.c:734-759) divides \(2\) and the \(q_i\) out of \(b\) with the reciprocals and passes when the sign of the result times its entries modulo the \(q_i\) of odd exponent is \(1\). The contracts: tables exist only for \(b_{\mathrm{high}} \le \mathrm{mulModLimit}\) and \(\ell \ne 0\), and then describe \(\ell \) as above, with primes of the table and their reciprocals; for such tables and \(1 \le b {\lt} 2^{64}\) with \(b q {\lt} 2^{64}\) for every prime \(q\) of the tables, the test is the negated exclusive or of the sign and the entries at the part of \(b\) free of \(2\) and of these primes.
The contract of the binary algorithm rests on invariants of its loops; \(b^*\) is Nat.coprimePart, and the symbol is Mathlib’s jacobiSym.
When the tables of \(\ell \) for \(b_{\mathrm{high}}\) exist, the test by tables passes \(1 \le b \le b_{\mathrm{high}}\) exactly when \(J(\ell \mid b^*) = 1\). Let \(d\) be even, \(a\) and \(y\) integers and \(b\) a natural number with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). Then \(J(c_d \mid b^*) = 1\) for the largest divisor \(b^*\) of \(b\) prime to \(2 c_d\); so for \(b \ge 1\) the binary algorithm gives \(1\) on \(b\) and \(c_d\), and the test by tables of \(c_d\) for \(b_{\mathrm{high}} \ge b\), when they exist, passes \(b\).
The denominators are below \(2^{32}\) and the primes of the table below \(2^{10}\), so the quotients by the reciprocals are exact (Ratpoints.Sieve.mulDiv_magic) and leave \(b^*\); by reciprocity each \(J(q_i \mid b^*)\) of odd exponent is the Legendre symbol of \(b^* \bmod q_i\), which the table gives, times a sign by \(b^* \bmod 4\). For a triple of even degree, \(c_d\) is a square modulo every prime of \(b\) prime to it (Ratpoints.Sieve.isSquare_getD_degree_of_sq_eq_binaryForm).
8.5 The shapes of the loop
The four shapes with their data (find_points.c:3725-3728, find_points.c:3736-3749), which run_setup chooses from the flags and returns with the bounds of the search intervals (find_points.c:3778-3806), and their denominators from \(b_{\mathrm{low}}\) to \(b_{\mathrm{high}}\) in the order of the loop, each with its test of a single denominator:
- (1)
under the flag of the squares, the squares \(k^2\) for \(\lceil \sqrt{b_{\mathrm{low}}}\, \rceil \le k \le \lfloor \sqrt{b_{\mathrm{high}}}\, \rfloor \), with the class test;
- (2)
otherwise, when the set-up has returned the records and the divisors of Definition 8.4, the divisors times squares: for each divisor \(s\) in turn, the \(s k^2\) of the range in increasing order of \(k\), with the class test and the valuation test, which \(b\) fails when the record of a prime excludes it (find_points.c:3944-3953);
- (3)
otherwise, under the flag of the checked loop, the words, with the forbidden divisors, the switch of the Jacobi test, its tables when the test is on and they exist, and \(c_d\): word by word, the \(64 w + j\) of the range for the set bits \(j\), lowest first, of \(\mathrm{den\_ bits}\) and-ed with word \(w \bmod p\) of each forbidden divisor \(p\) with words, tested by the tables, then by the forbidden divisors with masks, and, with the Jacobi test on and no tables, by the binary algorithm (find_points.c:4013-4041);
- (4)
otherwise every denominator, \(b_{\mathrm{low}}, \dots , b_{\mathrm{high}}\), with the class test.
The class test is that the pattern of the class of \(b \bmod 64\) is not \(0\). The lists of the denominators of the shapes (Ratpoints.Sieve.Shape.dens) and the choice of the test of a single denominator (Ratpoints.Sieve.Shape.keep) are definitions of the proofs, the reference of the loops over the blocks, which test and sift each denominator as they reach it, as run_block does; the tests themselves model the C code. The denominators of the search (Ratpoints.searchDens) are those of the divisors times squares when \(d\) is odd, \(|c_d| \ne 1\) and the set-up for \(b_{\mathrm{high}}\) returns divisors, and \(b_{\mathrm{low}}, \dots , b_{\mathrm{high}}\) otherwise.
The loops over the blocks (Ratpoints.Sieve.Shape.blockLoop, Chapter 6) visit the denominators of the list of the shape in its order (Ratpoints.Sieve.Shape.flatMap_blockDens). In the shape of the words they reduce the number of the first word of a block modulo each forbidden divisor, with its reciprocal while that number is at most \(\mathrm{mulModLimit}\) and by division otherwise, and step on from there (find_points.c:3981-4006).
Let \(1 \le b_{\mathrm{low}}\). The denominators of every shape lie in the range: the squares are its squares in increasing order; for positive divisors, the divisors times squares are its \(s k^2\) with \(s\) a divisor, without duplicates for distinct squarefree divisors; for forbidden divisors with positive primes and the words of Ratpoints.Sieve.forbiddenRow, the words give, in increasing order, the denominators of the range with their bit in \(\mathrm{den\_ bits}\) set that none of these primes divides. Let \(a\) and \(y\) be integers and \(1 \le b \le H\) with \(\gcd (a, b) = 1\) and \(y^2 = F(a, b)\). For odd \(d\), \(b\) passes the valuation test with the records of Definition 8.4; for even \(d\) and admissible forbidden divisors for \(b_{\mathrm{high}} = H\), the bit of \(b \bmod 64\) in \(\mathrm{den\_ bits}\) is set, no forbidden divisor with words divides \(b\), and \(b\) passes the tests of the words, with the tables for \(H\) when the Jacobi test is on. When bit \(j\) of \(\mathrm{den\_ bits}\) says whether the pattern of class \(j\) is not \(0\), a denominator of a shape that passes its test has a nonzero pattern.
The squares come from the integer square roots, \(\lceil \sqrt{n}\, \rceil \le k\) exactly when \(n \le k^2\); \(s k^2\) determines the squarefree \(s\) and \(k\) (Nat.eq_of_mul_sq_eq_mul_sq); and bit \(t\) of word \(w \bmod p\) of a forbidden divisor is clear exactly when \(p \mid 64 w + t\) (Ratpoints.Sieve.getLsbD_getElem!_forbiddenRow). The tests pass \(b\) by Lemmas 8.2, 8.5, 8.7 and 8.9.
8.6 The order of the denominators
The shapes visit their denominators in increasing order, except the divisors times squares, which go divisor by divisor. The denominators that the other shapes and the tests leave out carry no point (Lemma 8.11), so among those that carry points only the divisor shape changes the order. For \(y^2 = 1 + 2x\) and \(H = 20\), with the divisors \(1\) and \(2\), the loop visits \(1, 4, 9, 16\) and then \(2, 8, 18\) (\(4\) and \(16\) fail the valuation test of the prime \(2\)), so that ratpoints prints \((-4 : 3 : 9)\) before \((-1 : 0 : 2)\).
For \(b_{\mathrm{high}} \ge 1\) the denominators of the search of \(c\) of its degree from \(1\) to \(b_{\mathrm{high}}\) are \(\mathrm{searchDenominators}(\mathrm{maxDivisors}, c, b_{\mathrm{high}})\) (Definition 2.9), and those from \(b_{\mathrm{low}} \ge 1\) are those from \(1\) that are at least \(b_{\mathrm{low}}\). For \(1 \le b_{\mathrm{low}}\) and \(1 \le b_{\mathrm{high}} \le H\), the points that the brute-force reference finds over \((1, 0)\), the points at infinity, followed by those over the denominators of the search with the numerators \(-H, \dots , H\), are a permutation of the points of \(\mathrm{bruteForce}(c, H)\) with \(z = 0\) or \(b_{\mathrm{low}} \le z \le b_{\mathrm{high}}\).
The specification takes the divisors times squares under the same condition, with the divisors \(\mathrm{binaryDivisors}\) (Definition 8.4); from \(1\) the divisor shape lists the \(s k^2 \le b_{\mathrm{high}}\) divisor by divisor (Ratpoints.Sieve.squares1Dens_one_eq_filter). The divisor shape holds every denominator of a point in the range once (Lemmas 8.5 and 8.11), so its points are a permutation of those of the whole range (Ratpoints.perm_flatMap_squares1Dens).
With the block lemma (Theorem 3.13), these lemmas give the list that a search delivers (Chapter 3), on which the order theorem (Theorem 3.5) and the membership theorem (Theorem 3.3) rest.
8.7 Where the model differs from the C code
One function serves for valuation and valuation1, one for jacobi and jacobi1; the square shapes take exact integer square roots, which agree with the C code’s corrected square roots in double on the arguments it passes; and the symbol \(J(c_d \mid p) = -1\) of the further primes is read off the table of the squares modulo \(p\). The masks of the forbidden valuations have no bound \(m {\lt} 63\), which never binds for a long \(b_{\mathrm{high}}\) (Ratpoints.Sieve.lt_forty_of_pow_le), so that the model is sound for every height. The other deviations, natural numbers for the C integer types and no failure for lack of memory, are those of the whole model (Chapter 11).