The order of the points #
The list of the points that ratpoints finds, in its order, for a coefficient list c and a height
bound H. It is the order of the polynomial that ratpoints searches, which its set-up may
reverse, exchanging x and z in the binary form: the points at infinity first, then the points of
each denominator z in turn, in the order of the loop of the search, which visits those that its
tests let through (the others carry no point), by ascending numerator x, (x, y, z) before
(x, -y, z), each point mapped back to the caller's curve after a reversal. The denominators of the
polynomial searched ascend, except when it has odd degree d with |c_d| ≠ 1 (its own degree and
leading coefficient) and ratpoints factors |c_d| completely by trial division and finds fewer
than maxDiv of its squarefree divisors up to the largest denominator B of the search: then they
are e k ^ 2, divisor e by divisor in the order of binary counting over the primes of c_d, and
k ascending. The largest denominator is the height bound H, or the bound of the range of the
denominators of a search region (Ratpoints.denominatorBound); the other parts of a search region
(the search intervals, the lower bound of the denominators) only filter the list, and a search
region other than the whole box (Ratpoints.IsFullBox) forbids the reversal. The specification uses
Mathlib and nothing of the model; the comparator challenge restates its definitions verbatim.
Main definitions #
Ratpoints.searchedPoly: the polynomial searched, and whether it is the reversed one.Ratpoints.FactorsByTrialDivision: whetherratpointsfactors a number completely.Ratpoints.binaryDivisors: the squarefree divisors up toH, in the order of binary counting.Ratpoints.searchDenominators: the denominators of the search, in its order.Ratpoints.pointsWithDen: the points of one denominator, in their order.Ratpoints.orderedPoints: the list of the points, in the order ofratpoints.
Implementation notes #
The file imports Mathlib.Data.Nat.Factors for the prime factors of a number
(Nat.primeFactorsList, in increasing order with multiplicity), and Ratpoints.Spec.Region for the
examples with a search region; the comparator challenge imports the Mathlib modules among the public
imports of the files of the specification that it restates.
The polynomial that ratpoints searches for the coefficient list c of degree d, and whether
it is reversed, when the switch reverse allows a reversal (the option -k of the program forbids
it): for even d, the list c_d, …, c₀ when c₀ = 0 (then c₁ ≠ 0, or the binary form is not
squarefree and refused) or when c_d is a square and c₀ is not; for odd d, the list
0, c_d, …, c₁ when |c_d| ≠ 1, c₀ = 0 and |c₁| = 1; otherwise c itself. The binary form
of a reversed list is that of c with x and z exchanged, except for even d with
c₀ = c₁ = 0, which ratpoints refuses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whether ratpoints factors n completely: it divides off 2 and the odd primes up to 1021
in turn and takes a cofactor below p ^ 2, for the next prime p, as a prime, which it is; so it
fails exactly when the part of n at the primes from 1021 on is at least 1021 ^ 2 and not a
power of 1021.
Equations
- Ratpoints.FactorsByTrialDivision n = ((List.filter (fun (x : ℕ) => decide (1021 ≤ x)) n.primeFactorsList).prod < 1021 ^ 2 ∨ ∀ p ∈ n.primeFactorsList, p ≤ 1021)
Instances For
Equations
- One or more equations did not get rendered due to their size.
The squarefree divisors of n at most H, in the order of binary counting over the prime
factors p₁ < p₂ < ⋯ of n: the products of the sublists of the primes,
1, p₁, p₂, p₁ p₂, p₃, p₁ p₃, …, those of them at most H, in this order (List.sublists, p₁
the lowest bit).
Equations
- Ratpoints.binaryDivisors n H = List.filter (fun (x : ℕ) => decide (x ≤ H)) (List.map List.prod n.primeFactorsList.dedup.sublists)
Instances For
The denominators of the search of the polynomial with the coefficient list c of degree d,
up to the largest denominator H of the search (the height bound, or the bound of the range of the
denominators, Ratpoints.denominatorBound): when d is odd, |c_d| ≠ 1, ratpoints factors
|c_d| completely (Ratpoints.FactorsByTrialDivision) and it has fewer than maxDiv squarefree
divisors at most H (Ratpoints.binaryDivisors), the numbers e k ^ 2 ≤ H, divisor e by
divisor in that order and k = 1, 2, … for each; otherwise 1, …, H. This is the order of the
loop of the search, which visits those of them that its tests let through (for d odd and
|c_d| = 1 only the squares); the others carry no point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The points of height at most H with the denominator z: for the numerators x = -H, …, H
in turn, with y = ⌊√F(x, z)⌋ (Int.sqrt, which is 0 when F(x, z) < 0, where the filter by
Ratpoints.IsPoint keeps nothing), the points among (x, y, z) and (x, -y, z), in this order
(one point when y = 0). The denominator 0 gives the points at infinity, whose numerator is
1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The points of height at most H on y ^ 2 = F(x, z) for the coefficient list c with
denominators at most B, in the order in which ratpoints finds them, for the switch reverse of
the reversal and the bound maxDiv of the number of divisors: for the polynomial searched
(Ratpoints.searchedPoly), its points at infinity, then the points of its denominators up to B
(Ratpoints.searchDenominators) in turn (Ratpoints.pointsWithDen); after a reversal, each point
(a, y, b) of that list becomes (b, y, a) for a ≥ 0 and (-b, y, -a) for a < 0, a point of
the caller's curve.
Equations
- One or more equations did not get rendered due to their size.