The denominators of the search

The search of the polynomial with the coefficient list c of degree d visits the denominators from bLow to the largest denominator bHigh in the order of the loop of its shape (Ratpoints.searchDens): the divisors of the leading coefficient times squares when d is odd, |c_d| ≠ 1 and the divisor set-up up to bHigh succeeds, and bLow, …, bHigh otherwise. These are the denominators of the specification of the order up to bHigh (Ratpoints.searchDenominators) from bLow on, each once, and their points, with the points at infinity, are a permutation of the brute-force reference restricted to these denominators.

Main definitions

• Ratpoints.searchDens: the denominators of the search, in the order of its loop.

Main statements

• Ratpoints.perm_filter_bruteForce_append_flatMap_searchDens: the points at infinity and those of the denominators of the search from bLow to bHigh are a permutation of the brute-force reference restricted to these denominators.
• Ratpoints.searchDens_one_eq_searchDenominators: the denominators of the search from 1 on are those of the specification of the order up to bHigh; Ratpoints.searchDens_eq_filter: from bLow on, they are those from 1 on that are at least bLow.

Proof

The divisor shape visits each denominator of a point once (Ratpoints.exists_eq_mul_mul_of_sq_eq_binaryForm_of_odd, Ratpoints.Setup.mem_iff_of_setupUs1_eq_some, Ratpoints.Sieve.mem_squares1Dens_iff, Ratpoints.Sieve.nodup_squares1Dens), so that its list gives a permutation of the reference (List.perm_flatMap_of_nodup); the divisor set-up succeeds exactly when the specification of the order takes the divisor shape, with the divisors of Ratpoints.binaryDivisors (Ratpoints.Setup.map_snd_run_setupUs1).

def Ratpoints.searchDens (c : List ℤ) (d bLow bHigh : ℕ) : List ℕ

The denominators of the search of the polynomial with the coefficient list c of degree d, from bLow to the largest denominator bHigh, in the order of its loop: the divisors of the leading coefficient times squares (Ratpoints.Sieve.squares1Dens) when d is odd, |c_d| ≠ 1 and the divisor set-up up to bHigh succeeds (Ratpoints.Setup.setupUs1), and bLow, …, bHigh otherwise, of which the other shapes visit, in this order, those that their tests let through (Ratpoints.Sieve.Shape).

Equations

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

theorem Ratpoints.le_and_le_of_mem_searchDens {c : List ℤ} {bLow bHigh b : ℕ} (hbLow : 1 ≤ bLow) (hb : b ∈ searchDens c (degree c) bLow bHigh) : bLow ≤ b ∧ b ≤ bHigh

The denominators of the search lie in bLow, …, bHigh.

theorem Ratpoints.nodup_searchDens (c : List ℤ) {bLow bHigh : ℕ} (hbLow : 1 ≤ bLow) : (searchDens c (degree c) bLow bHigh).Nodup

The denominators of the search from bLow ≥ 1 are distinct: bLow, …, bHigh, or for odd degree the products of the distinct squarefree divisors of the set-up with squares (Ratpoints.Sieve.nodup_squares1Dens), and none for bHigh = 0.

theorem Ratpoints.perm_flatMap_squares1Dens {c : List ℤ} {H bLow bHigh : ℕ} (hbLow : 1 ≤ bLow) (hb : 1 ≤ bHigh) (hd : degree c % 2 = 1) {info : List Setup.DenInfo} {divisors : List ℕ} (hs : (Setup.setupUs1 c (degree c) bHigh).run = some (info, divisors)) : (List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c (degree c) (↑b) (BruteForce.numerators H)) (Sieve.squares1Dens divisors bLow bHigh)).Perm (List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c (degree c) (↑b) (BruteForce.numerators H)) (List.range' bLow (bHigh + 1 - bLow)))

The divisor shape visits each denominator of a point once, so that it gives a permutation of the points of the denominators bLow, …, bHigh: the denominator of every point is s k ^ 2 with s squarefree and dividing c_d, so one of the divisors of the set-up, and the shape lists each such product once (List.perm_flatMap_of_nodup).

theorem Ratpoints.perm_filter_bruteForce_append_flatMap_searchDens (c : List ℤ) {H bLow bHigh : ℕ} (hbLow : 1 ≤ bLow) (hb : 1 ≤ bHigh) (hbH : bHigh ≤ H) : (BruteForce.pointsOfDen c (degree c) 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c (degree c) (↑b) (BruteForce.numerators H)) (searchDens c (degree c) bLow bHigh)).Perm (List.filter (fun (p : ℤ × ℤ × ℤ) => decide (p.2.2 = 0 ∨ ↑bLow ≤ p.2.2 ∧ p.2.2 ≤ ↑bHigh)) (bruteForce c H))

The points at infinity and those of the denominators of the search from bLow ≥ 1 to bHigh ≤ H are a permutation of the brute-force reference restricted to the points at infinity and the denominators from bLow to bHigh (Ratpoints.perm_flatMap_squares1Dens).

theorem Ratpoints.searchDens_eq_filter (c : List ℤ) (d : ℕ) {bLow : ℕ} (hbLow : 1 ≤ bLow) (bHigh : ℕ) : searchDens c d bLow bHigh = List.filter (fun (x : ℕ) => decide (bLow ≤ x)) (searchDens c d 1 bHigh)

The denominators of the search from bLow ≥ 1 on are those from 1 on that are at least bLow, for each shape by its listing (Ratpoints.Sieve.squares1Dens_eq_filter).

theorem Ratpoints.searchDens_one_eq_searchDenominators (c : List ℤ) {bHigh : ℕ} (hb : 1 ≤ bHigh) : searchDens c (degree c) 1 bHigh = searchDenominators maxDivisors c bHigh

The denominators of the search of the polynomial with the coefficient list c of its degree from 1 to bHigh ≥ 1 are those of the specification of the order (Ratpoints.searchDenominators): the divisor set-up succeeds exactly when the specification takes the divisor shape, with the divisors of Ratpoints.binaryDivisors (Ratpoints.Setup.map_snd_run_setupUs1).