The denominators of a polynomial of odd degree

For a polynomial of odd degree the denominator of every point is a squarefree divisor of the leading coefficient c_d times a square, and a square when |c_d| = 1: a prime p ∤ c_d divides it an even number of times, since the term c_d a ^ d b of F(a, b) alone has the least valuation. The divisor set-up (Ratpoints.Setup.setupUs1) factors |c_d| over 2 and the primes of the table, the cofactor below the square of the next prime of the table being a prime since the table holds every odd prime below 1022 in increasing order (Ratpoints.Setup.factorLcf), lists the squarefree divisors of c_d up to the largest denominator by the doubling loop (Ratpoints.Setup.squarefreeDivisors), and computes the slopes of the valuation test (Ratpoints.Setup.slope), whose entries exclude no denominator of a point. The products x p that the C code computes as longs stay at most the largest denominator, and the square p * p of a prime of the table, an int, below 2 ^ 31. The factorization finds the primes in increasing order, so that the divisors come in the order of binary counting over the primes, and while a prime of the table is still to come its cofactor is the part of |c_d| at the primes from it on (Nat.IsRoughPart), so that it is complete exactly when the specification of the order says so (Ratpoints.FactorsByTrialDivision): the divisor set-up succeeds exactly when the factorization is complete and the doubling loop, which lists a prefix of all the products when it stops, finds fewer than Ratpoints.maxDivisors divisors.

Main definitions

• Ratpoints.Setup.IsFactorization: a list of primes in increasing order with their valuations that holds every prime factor of a number.
• Ratpoints.Setup.extendDivisors: one pass of the doubling loop of the squarefree divisors.
• Ratpoints.Setup.DenInfo.excludes: whether an entry of the valuation test of the divisor shape excludes a denominator.

Main statements

• Ratpoints.isSquare_of_sq_eq_binaryForm_of_odd: for odd degree and |c_d| = 1, the denominator of every point is a square.
• Ratpoints.exists_eq_mul_mul_of_sq_eq_binaryForm_of_odd: for odd degree, the denominator of every point is s k ^ 2 with s squarefree and s ∣ c_d.
• Ratpoints.even_add_of_sq_eq_binaryForm_of_odd: the valuation test of the slopes.
• Ratpoints.factorsByTrialDivision_of_isRoughPart_one, Ratpoints.factorsByTrialDivision_of_isRoughPart_of_lt, Ratpoints.eq_one_iff_factorsByTrialDivision_of_isRoughPart: whether ratpoints factors a number completely, read off its parts at the primes from a bound on.
• Ratpoints.Setup.factorLcf_spec, Ratpoints.Setup.squarefreeDivisors_spec, Ratpoints.Setup.slope_spec, Ratpoints.Setup.setupUs1_spec: the contracts of the divisor set-up; the factorization leaves the cofactor 1 exactly when ratpoints factors the number completely, and then it lists the primes in increasing order, each with its valuation; the set-up succeeds exactly when the cofactor is 1 and the doubling loop gives fewer than Ratpoints.maxDivisors divisors.
• Ratpoints.Setup.foldl_extendDivisors_eq_filter: the doubling loop lists the products of the sublists of the primes in the order of binary counting, up to the bound.
• Ratpoints.Setup.map_snd_run_setupUs1: the divisor set-up succeeds exactly when ratpoints factors |c_d| completely and finds fewer than Ratpoints.maxDivisors divisors, and its divisors are then those of Ratpoints.binaryDivisors.
• Ratpoints.mem_binaryDivisors_iff, Ratpoints.nodup_binaryDivisors: the divisors of Ratpoints.binaryDivisors are the squarefree divisors up to the bound, each once.
• Ratpoints.Setup.mem_iff_of_setupUs1_eq_some, Ratpoints.Setup.nodup_of_setupUs1_eq_some: so the divisors of the divisor set-up are the squarefree divisors of |c_d| up to the largest denominator, each once.
• Ratpoints.Setup.DenInfo.excludes_eq_false_of_sq_eq: no entry of the valuation test, a prime of c_d with its valuation and its slope, excludes the denominator of a point.
• Ratpoints.Setup.fitsLong_mul_of_le_div: the products x p of the C code are longs; Ratpoints.Setup.mul_self_lt_of_mem_primeTable, Ratpoints.Setup.fitsLong_of_lt_mul_self: the square p * p of a prime of the table is an int, and a cofactor below it a long.

Implementation notes

The contracts are proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions, in a file with Mathlib, since they speak of primes and their valuations. That the macro CEIL of the C code rounds up is a private lemma of this file, which only the slopes use: its if is that of the macro, and Mathlib has no ceiling division of integers to state it with. Ratpoints.Setup.fitsLong_mul_of_le_div discharges a range obligation that a Deviation paragraph of the model states, and no proof consumes it.

The denominators of the points

theorem Ratpoints.even_of_sq_eq_binaryForm_of_odd_of_dvd {c : List ℤ} {a y : ℤ} {b p V : ℕ} [Fact (Nat.Prime p)] (hd : degree c % 2 = 1) (hy : y ^ 2 = binaryForm c a ↑b) {u : ℤ} (hu : c.getD (degree c) 0 * a ^ degree c * ↑b = ↑p ^ V * u) (hpu : ¬↑p ∣ u) (h : ∀ i < degree c, ↑p ^ (V + 1) ∣ c.getD i 0 * a ^ i * ↑b ^ (degree c + 1 - i)) : Even V

For odd degree, a point (a, y, b) whose term c_d a ^ d b of F(a, b) is p ^ V u with p ∤ u, while p ^ (V + 1) divides every other term, has an even V (Int.even_and_exists_isSquare_add_of_sq_eq_sum).

theorem Ratpoints.even_add_of_sq_eq_binaryForm_of_odd {c : List ℤ} {a y : ℤ} {b p val : ℕ} [hp : Fact (Nat.Prime p)] (hd : degree c % 2 = 1) (hval : padicValNat p (c.getD (degree c) 0).natAbs = val) (hmin : ∀ k < degree c, c.getD k 0 ≠ 0 → val + 1 ≤ padicValNat p (c.getD k 0).natAbs + (degree c - k) * padicValNat p b) (hab : a.gcd ↑b = 1) (hm : padicValNat p b ≠ 0) (hy : y ^ 2 = binaryForm c a ↑b) : Even (val + padicValNat p b)

The valuation test of the slopes (odd degree): for a prime p with v_p(c_d) = val and a denominator b of a point with m = v_p(b) ≥ 1 and (d - k) m ≥ 1 + val - v_p(c_k) for every k < d with c_k ≠ 0, the term c_d a ^ d b of F(a, b) alone has the least valuation val + m, which is then even.

theorem Ratpoints.even_of_sq_eq_binaryForm_of_odd {c : List ℤ} {a y : ℤ} {b p : ℕ} [Fact (Nat.Prime p)] (hd : degree c % 2 = 1) (hc : ¬↑p ∣ c.getD (degree c) 0) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : Even (padicValNat p b)

For odd degree, a prime p ∤ c_d divides the denominator b of every point an even number of times: for v_p(b) ≥ 1 the term c_d a ^ d b of F(a, b) alone has the least valuation v_p(b) (Ratpoints.even_add_of_sq_eq_binaryForm_of_odd with v_p(c_d) = 0).

theorem Ratpoints.isSquare_of_sq_eq_binaryForm_of_odd {c : List ℤ} (hd : degree c % 2 = 1) (hc : IsUnit (c.getD (degree c) 0)) {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : IsSquare b

For odd degree and a leading coefficient ±1, the denominator b of every point is a square: its valuation v_p(b) at every prime p is even (Ratpoints.even_of_sq_eq_binaryForm_of_odd), since for v_p(b) ≥ 1 the term c_d a ^ d b of F(a, b) alone has the least valuation.

theorem Ratpoints.exists_eq_mul_mul_of_sq_eq_binaryForm_of_odd {c : List ℤ} (hd : degree c % 2 = 1) {a y : ℤ} {b : ℕ} (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : ∃ (s : ℕ) (k : ℕ), Squarefree s ∧ s ∣ (c.getD (degree c) 0).natAbs ∧ b = s * k * k

For odd degree, the denominator of every point is s k ^ 2 with s squarefree and dividing the leading coefficient: a prime that divides b an odd number of times divides c_d (Ratpoints.even_of_sq_eq_binaryForm_of_odd).

Factoring by trial division

theorem Ratpoints.factorsByTrialDivision_of_isRoughPart_one {q n : ℕ} (h : q.IsRoughPart n 1) (hq : q ≤ 1022) : FactorsByTrialDivision n

A number whose part at the primes from q ≤ 1022 on is 1 has no prime factor above 1021, so that ratpoints factors it completely.

theorem Ratpoints.factorsByTrialDivision_of_isRoughPart_of_lt {q n w : ℕ} (h : q.IsRoughPart n w) (hn : n ≠ 0) (hq : q ≤ 1021) (hw : w < q * q) : FactorsByTrialDivision n

A number whose part at the primes from q ≤ 1021 on is below q ^ 2 has its part at the primes from 1021 on below 1021 ^ 2, so that ratpoints factors it completely.

theorem Ratpoints.eq_one_iff_factorsByTrialDivision_of_isRoughPart {n w m : ℕ} (h : Nat.IsRoughPart 1021 n w) (hn : n ≠ 0) (hw : 1021 * 1021 ≤ w) (hm : Nat.IsRoughPart 1022 n m) : m = 1 ↔ FactorsByTrialDivision n

When the part w of n ≠ 0 at the primes from 1021 on is at least 1021 ^ 2, ratpoints factors n completely exactly when its part m at the primes from 1022 on is 1.

The squarefree divisors in the order of binary counting

theorem Ratpoints.mem_binaryDivisors_iff {n H s : ℕ} (hn : n ≠ 0) : s ∈ binaryDivisors n H ↔ Squarefree s ∧ s ∣ n ∧ s ≤ H

The products of the sublists of the distinct prime factors of n ≠ 0 are its squarefree divisors; for n = 0 there is only the empty product 1.

theorem Ratpoints.nodup_binaryDivisors (n H : ℕ) : (binaryDivisors n H).Nodup

Distinct sublists of the distinct prime factors of n have distinct products.

The factorization of the leading coefficient

def Ratpoints.Setup.IsFactorization (w : ℕ) (fac : List (ℕ × ℕ)) : Prop

The list fac of pairs (p, v) is the factorization of w: its primes p ascend, each with its valuation v = v_p(w) ≥ 1, and every prime factor of w is among them.

Equations

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

theorem Ratpoints.Setup.mul_self_lt_of_mem_primeTable {p : ℕ} (hp : p ∈ primeTable) : p * p < 2 ^ 31

The square p * p of a prime of the table, which setup_us1 computes as an int (find_points.c:800), is below 2 ^ 31.

theorem Ratpoints.Setup.fitsLong_of_lt_mul_self {w p : ℕ} (hp : p ∈ primeTable) (hw : w < p * p) : fitsLong ↑w = true

A cofactor below the square of a prime of the table is a long, so that the test of Ratpoints.Setup.factorLcf before it takes the cofactor as a prime always passes (find_points.c:808).

def Ratpoints.Setup.CofactorInvariant (w0 : ℕ) (fac : List (ℕ × ℕ)) : List ℕ → ℕ → Prop

The part of the invariant of Ratpoints.Setup.factorLcf for its cofactor w, with the factors fac found and the primes suff of the table still to come: while a prime cur is still to come, the primes found lie below it and every prime factor of w is at least cur; at the end, w = 1 exactly when ratpoints factors w0 completely.

Equations

• Ratpoints.Setup.CofactorInvariant w0 fac [] x✝ = (x✝ = 1 ↔ Ratpoints.FactorsByTrialDivision w0)
• Ratpoints.Setup.CofactorInvariant w0 fac (cur :: tail) x✝ = ((∀ x ∈ fac, x.1 < cur) ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ x✝ → cur ≤ p)

structure Ratpoints.Setup.FactorLcfInvariant (w0 : ℕ) (suff : List ℕ) (w : ℕ) (fac : Array (ℕ × ℕ)) : Prop

The invariant of the loop of Ratpoints.Setup.factorLcf over the primes of the table, for the number w0 ≥ 1 to factor, with the primes suff still to come: w0 is the cofactor w times the powers of the factors found, ascending primes p with their valuations v_p(w0) ≥ 1 that do not divide w, and the cofactor satisfies Ratpoints.Setup.CofactorInvariant: while a prime cur of the table is still to come, w is the part of w0 at the primes from cur on (Ratpoints.Setup.FactorLcfInvariant.isRoughPart).

• eq_mul_prod : w0 = w * (List.map (fun (x : ℕ × ℕ) => x.1 ^ x.2) fac.toList).prod

  w0 is the cofactor times the powers of the factors found.

• pairwise_lt : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (List.map Prod.fst fac.toList)

  The primes found ascend.

• prime_valuation (x : ℕ × ℕ) : x ∈ fac.toList → Nat.Prime x.1 ∧ x.2 = padicValNat x.1 w0 ∧ 0 < x.2 ∧ ¬x.1 ∣ w

  Each factor found is a prime with its valuation in w0, at least 1, that does not divide the cofactor.

• cofactor : CofactorInvariant w0 fac.toList suff w

  The cofactor satisfies Ratpoints.Setup.CofactorInvariant.

theorem Ratpoints.Setup.FactorLcfInvariant.ne_zero {w0 w : ℕ} {suff : List ℕ} {fac : Array (ℕ × ℕ)} (h : FactorLcfInvariant w0 suff w fac) (hw0 : 0 < w0) : w ≠ 0

theorem Ratpoints.Setup.FactorLcfInvariant.isRoughPart {w0 w cur : ℕ} {suff : List ℕ} {fac : Array (ℕ × ℕ)} (h : FactorLcfInvariant w0 (cur :: suff) w fac) : cur.IsRoughPart w0 w

While the prime cur of the table is still to come, the cofactor is the part of w0 at the primes from cur on: the product of the powers of the primes found, all below cur, is cur-smooth.

theorem Ratpoints.Setup.FactorLcfInvariant.push {w0 w m p v : ℕ} {suff suff' : List ℕ} {fac : Array (ℕ × ℕ)} (h : FactorLcfInvariant w0 suff w fac) (hp : Nat.Prime p) (hv : 0 < v) (hm : w = p ^ v * m) (hpm : ¬p ∣ m) (hlt : ∀ x ∈ fac.toList, x.1 < p) (h4 : CofactorInvariant w0 (fac.push (p, v)).toList suff' m) : FactorLcfInvariant w0 suff' m (fac.push (p, v))

A new prime factor p of the cofactor w = p ^ v m, p ∤ m, above the primes found, taken with its exponent v ≥ 1, leaves the cofactor m.

theorem Ratpoints.Setup.factorLcfInvariant_nil_push {w0 v2 r : ℕ} (hw0 : 0 < w0) (hv : (v2, r) = (valuation (↑w0) 2).run) (h : 0 < v2) : FactorLcfInvariant w0 (ForIn.toList primeTable) (w0 / 2 ^ v2) (#[].push (2, v2))

After the power 2 ^ v2 ≠ 1 of w0, found: the odd part of w0, every prime factor of which is at least 3, the first prime of the table.

theorem Ratpoints.Setup.factorLcfInvariant_nil {w0 v2 r : ℕ} (hw0 : 0 < w0) (hv : (v2, r) = (valuation (↑w0) 2).run) (h : ¬0 < v2) : FactorLcfInvariant w0 (ForIn.toList primeTable) w0 #[]

For odd w0: the cofactor w0, every prime factor of which is at least 3, the first prime of the table, and no prime found.

theorem Ratpoints.Setup.cofactorInvariant_of_isRoughPart {w0 w m cur : ℕ} {pref suff : List ℕ} {fac : List (ℕ × ℕ)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (hw0 : w0 ≠ 0) (hw : cur.IsRoughPart w0 w) (hlt : ¬w < cur * cur) (hm : (cur + 1).IsRoughPart w0 m) (hfac : ∀ x ∈ fac, x.1 ≤ cur) : CofactorInvariant w0 fac suff m

The cofactor m after the prime cur of the table, whose part w ≥ cur ^ 2 of w0 at the primes from cur on it has divided by the power of cur, with the primes found at most cur: while a prime is still to come, the primes found lie below it and m is the part of w0 at the primes from it on; after the last prime, 1021, m = 1 exactly when ratpoints factors w0 completely.

theorem Ratpoints.Setup.FactorLcfInvariant.push_cur {w0 w cur v r : ℕ} {pref suff : List ℕ} {fac : Array (ℕ × ℕ)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (h : FactorLcfInvariant w0 (cur :: suff) w fac) (hw0 : 0 < w0) (hlt : ¬w < cur * cur) (hv : (v, r) = (valuation (↑w) cur).run) (hpos : 0 < v) : FactorLcfInvariant w0 suff (w / cur ^ v) (fac.push (cur, v))

The prime cur of the table divided off w with its valuation v ≥ 1.

theorem Ratpoints.Setup.FactorLcfInvariant.skip {w0 w cur v r : ℕ} {pref suff : List ℕ} {fac : Array (ℕ × ℕ)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (h : FactorLcfInvariant w0 (cur :: suff) w fac) (hw0 : 0 < w0) (hlt : ¬w < cur * cur) (hv : (v, r) = (valuation (↑w) cur).run) (h0 : ¬0 < v) : FactorLcfInvariant w0 suff w fac

The prime cur of the table, which does not divide w, passed.

theorem Ratpoints.Setup.FactorLcfInvariant.push_self {w0 w cur : ℕ} {pref suff : List ℕ} {fac : Array (ℕ × ℕ)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (h : FactorLcfInvariant w0 (cur :: suff) w fac) (hw0 : 0 < w0) (h1 : ¬(w == 1) = true) (hlt : w < cur * cur) : FactorLcfInvariant w0 [] 1 (fac.push (w, 1))

A cofactor w ≠ 1 below cur ^ 2, with no prime factor below cur, is a prime (Nat.prime_of_lt_mul_self), taken with the valuation 1, which leaves the cofactor 1.

theorem Ratpoints.Setup.FactorLcfInvariant.of_eq_one {w0 w cur : ℕ} {pref suff : List ℕ} {fac : Array (ℕ × ℕ)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (h : FactorLcfInvariant w0 (cur :: suff) w fac) (h1 : (w == 1) = true) : FactorLcfInvariant w0 [] w fac

The cofactor 1: the loop ends, every prime factor of w0 found.

theorem Ratpoints.Setup.FactorLcfInvariant.of_not_fitsLong {w0 w cur : ℕ} {pref suff : List ℕ} {fac : Array (ℕ × ℕ)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (hlt : w < cur * cur) (hf : ¬fitsLong ↑w = true) : FactorLcfInvariant w0 [] w fac

A cofactor below cur ^ 2 is a long, so the loop never ends with it unfactored.

theorem Ratpoints.Setup.FactorLcfInvariant.iff_and_isFactorization {w0 w : ℕ} {fac : Array (ℕ × ℕ)} (h : FactorLcfInvariant w0 [] w fac) : (w = 1 ↔ FactorsByTrialDivision w0) ∧ (w = 1 → IsFactorization w0 fac.toList)

At the end of the loop, the cofactor is 1 exactly when ratpoints factors w0 completely, and then the factors found are the factorization of w0.

theorem Ratpoints.Setup.factorLcf_spec (w : ℕ) : ⦃ 0 < w ⦄ factorLcf w ⦃ fun (r : List (ℕ × ℕ) × ℕ) => (r.2 = 1 ↔ FactorsByTrialDivision w) ∧ (r.2 = 1 → IsFactorization w r.1) ⦄

The factorization of w ≥ 1 over 2 and the primes of the table leaves the cofactor 1 exactly when ratpoints factors w completely, and then it is the factorization of w, the primes in increasing order, each with its valuation.

theorem Ratpoints.Setup.snd_run_factorLcf_eq_one_iff {w : ℕ} (hw : 0 < w) : (factorLcf w).run.2 = 1 ↔ FactorsByTrialDivision w

Ratpoints.Setup.factorLcf_spec as a plain statement, for the cofactor.

theorem Ratpoints.Setup.isFactorization_of_run_factorLcf_eq {w : ℕ} (hw : 0 < w) {fac : List (ℕ × ℕ)} (h : (factorLcf w).run = (fac, 1)) : IsFactorization w fac

Ratpoints.Setup.factorLcf_spec as a plain statement, for a factorization with the cofactor 1.

The squarefree divisors

def Ratpoints.Setup.extendDivisors (bHigh : ℕ) (ds : List ℕ) (p : ℕ) : List ℕ

One pass of the doubling loop of Ratpoints.Setup.squarefreeDivisors with the prime p: the divisors ds found so far, then x p for each x of them with x ≤ ⌊bHigh / p⌋, in their order.

Equations

• Ratpoints.Setup.extendDivisors bHigh ds p = ds ++ List.map (fun (x : ℕ) => x * p) (List.filter (fun (x : ℕ) => decide (x ≤ bHigh / p)) ds)

def Ratpoints.Setup.DivisorsInvariant (bHigh : ℕ) (pref suff : List ℕ) (divs : Array ℕ) : Prop

The invariant of the loop of Ratpoints.Setup.squarefreeDivisors over the primes, after the primes pref with the primes suff still to come: the list is that of the passes over pref (Ratpoints.Setup.extendDivisors), or the loop has stopped at the end with Ratpoints.maxDivisors entries or more, a prefix of that list.

Equations

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

def Ratpoints.Setup.ExtendDivisorsInvariant (bHigh p : ℕ) (divs0 : Array ℕ) (pref suff : List ℕ) (divs : Array ℕ) : Prop

The invariant of the pass of Ratpoints.Setup.squarefreeDivisors with the prime p over the divisors divs0, after the positions pref with the positions suff still to come: the list is divs0 followed by the products x p of the entries x ≤ ⌊bHigh / p⌋ among the first |pref| ones, or the pass has stopped at the end with Ratpoints.maxDivisors entries or more, a prefix of that list.

Equations

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

theorem Ratpoints.Setup.divisorsInvariant_nil (bHigh : ℕ) (ps : List ℕ) : DivisorsInvariant bHigh [] ps #[1]

theorem Ratpoints.Setup.DivisorsInvariant.eq_of_cons {bHigh cur : ℕ} {pref suff : List ℕ} {divs : Array ℕ} (h : DivisorsInvariant bHigh pref (cur :: suff) divs) : divs.toList = List.foldl (extendDivisors bHigh) [1] pref

theorem Ratpoints.Setup.DivisorsInvariant.eq_or {bHigh : ℕ} {ps : List ℕ} {divs : Array ℕ} (h : DivisorsInvariant bHigh ps [] divs) : divs.toList = List.foldl (extendDivisors bHigh) [1] ps ∨ maxDivisors ≤ divs.toList.length ∧ divs.toList <+: List.foldl (extendDivisors bHigh) [1] ps

theorem Ratpoints.Setup.extendDivisorsInvariant_nil (bHigh p : ℕ) (divs0 : Array ℕ) (suff : List ℕ) : ExtendDivisorsInvariant bHigh p divs0 [] suff divs0

theorem Ratpoints.Setup.ExtendDivisorsInvariant.eq_or {bHigh p : ℕ} {divs0 divs : Array ℕ} (h : ExtendDivisorsInvariant bHigh p divs0 (ForIn.toList [:divs0.size]) [] divs) : divs.toList = extendDivisors bHigh divs0.toList p ∨ maxDivisors ≤ divs.size ∧ divs.toList <+: extendDivisors bHigh divs0.toList p

The pass over all positions of divs0 ends with Ratpoints.Setup.extendDivisors of divs0, or with a prefix of it with Ratpoints.maxDivisors entries or more.

theorem Ratpoints.Setup.ExtendDivisorsInvariant.divisorsInvariant_of_le {bHigh cur : ℕ} {ps pref suff : List ℕ} {divs0 divs : Array ℕ} (hps : ps = pref ++ cur :: suff) (h0 : DivisorsInvariant bHigh pref (cur :: suff) divs0) (h : ExtendDivisorsInvariant bHigh cur divs0 (ForIn.toList [:divs0.size]) [] divs) (hle : maxDivisors ≤ divs.size) : DivisorsInvariant bHigh ps [] divs

theorem Ratpoints.Setup.ExtendDivisorsInvariant.divisorsInvariant {bHigh cur : ℕ} {pref suff : List ℕ} {divs0 divs : Array ℕ} (h0 : DivisorsInvariant bHigh pref (cur :: suff) divs0) (h : ExtendDivisorsInvariant bHigh cur divs0 (ForIn.toList [:divs0.size]) [] divs) (hlt : ¬maxDivisors ≤ divs.size) : DivisorsInvariant bHigh (pref ++ [cur]) suff divs

theorem Ratpoints.Setup.ExtendDivisorsInvariant.eq_of_cons {bHigh p cur : ℕ} {divs0 divs : Array ℕ} {pref suff : List ℕ} (h : ExtendDivisorsInvariant bHigh p divs0 pref (cur :: suff) divs) : divs.toList = divs0.toList ++ List.map (fun (x : ℕ) => x * p) (List.filter (fun (x : ℕ) => decide (x ≤ bHigh / p)) (List.take pref.length divs0.toList))

theorem Ratpoints.Setup.ExtendDivisorsInvariant.push {bHigh p cur : ℕ} {divs0 divs : Array ℕ} {pref suff : List ℕ} (hl : ForIn.toList [:divs0.size] = pref ++ cur :: suff) (h : ExtendDivisorsInvariant bHigh p divs0 pref (cur :: suff) divs) (hle : divs[cur]! ≤ bHigh / p) : ExtendDivisorsInvariant bHigh p divs0 (pref ++ [cur]) suff (divs.push (divs[cur]! * p))

theorem Ratpoints.Setup.ExtendDivisorsInvariant.skip {bHigh p cur : ℕ} {divs0 divs : Array ℕ} {pref suff : List ℕ} (hl : ForIn.toList [:divs0.size] = pref ++ cur :: suff) (h : ExtendDivisorsInvariant bHigh p divs0 pref (cur :: suff) divs) (hgt : ¬divs[cur]! ≤ bHigh / p) : ExtendDivisorsInvariant bHigh p divs0 (pref ++ [cur]) suff divs

theorem Ratpoints.Setup.ExtendDivisorsInvariant.push_of_le {bHigh p cur : ℕ} {divs0 divs : Array ℕ} {pref suff : List ℕ} (hl : ForIn.toList [:divs0.size] = pref ++ cur :: suff) (h : ExtendDivisorsInvariant bHigh p divs0 pref (cur :: suff) divs) (hle : divs[cur]! ≤ bHigh / p) (hmax : maxDivisors ≤ (divs.push (divs[cur]! * p)).size) : ExtendDivisorsInvariant bHigh p divs0 (ForIn.toList [:divs0.size]) [] (divs.push (divs[cur]! * p))

theorem Ratpoints.Setup.ExtendDivisorsInvariant.skip_of_le {bHigh p cur : ℕ} {divs0 divs : Array ℕ} {pref suff : List ℕ} (hl : ForIn.toList [:divs0.size] = pref ++ cur :: suff) (h : ExtendDivisorsInvariant bHigh p divs0 pref (cur :: suff) divs) (hgt : ¬divs[cur]! ≤ bHigh / p) (hmax : maxDivisors ≤ divs.size) : ExtendDivisorsInvariant bHigh p divs0 (ForIn.toList [:divs0.size]) [] divs

theorem Ratpoints.Setup.squarefreeDivisors_spec (ps : List ℕ) (bHigh : ℕ) : ⦃ True ⦄ squarefreeDivisors ps bHigh ⦃ fun (r : List ℕ) => r = List.foldl (extendDivisors bHigh) [1] ps ∨ maxDivisors ≤ r.length ∧ r <+: List.foldl (extendDivisors bHigh) [1] ps ⦄

The doubling loop gives the list of all passes (Ratpoints.Setup.extendDivisors), or, when it stops at Ratpoints.maxDivisors entries, a prefix of it with that many entries or more.

theorem Ratpoints.Setup.run_squarefreeDivisors_eq_or (ps : List ℕ) (bHigh : ℕ) : (squarefreeDivisors ps bHigh).run = List.foldl (extendDivisors bHigh) [1] ps ∨ maxDivisors ≤ (squarefreeDivisors ps bHigh).run.length ∧ (squarefreeDivisors ps bHigh).run <+: List.foldl (extendDivisors bHigh) [1] ps

Ratpoints.Setup.squarefreeDivisors_spec as a plain statement.

The divisors in the order of binary counting

theorem Ratpoints.Setup.foldl_extendDivisors_eq_filter {bHigh : ℕ} (hb : 1 ≤ bHigh) {ps : List ℕ} (hps : ∀ p ∈ ps, 0 < p) : List.foldl (extendDivisors bHigh) [1] ps = List.filter (fun (x : ℕ) => decide (x ≤ bHigh)) (List.map List.prod ps.sublists)

The doubling loop over positive numbers ps lists the products of the sublists of ps that are at most bHigh ≥ 1, in the order of List.sublists: binary counting, the first entry of ps the lowest bit.

theorem Ratpoints.Setup.IsFactorization.map_fst_eq_dedup {n : ℕ} {fac : List (ℕ × ℕ)} (h : IsFactorization n fac) (hn : n ≠ 0) : List.map Prod.fst fac = n.primeFactorsList.dedup

The distinct primes of a factorization of n ≠ 0, in increasing order, are those of Nat.primeFactorsList n.

The slopes

def Ratpoints.Setup.SlopeInvariant (c : List ℤ) (d p val : ℕ) (pref : List ℕ) (n : ℤ) : Prop

The invariant of the loop of Ratpoints.Setup.slope after the positions pref: the slope n so far is at least 1, and for the coefficient c_k, k = d - 1 - j, of each position j done, (d - k) n ≥ 1 + val - v_p(c_k), with the valuation of Ratpoints.Setup.valuation.

Equations

• Ratpoints.Setup.SlopeInvariant c d p val pref n = (1 ≤ n ∧ ∀ j ∈ pref, 1 + ↑val - ↑(Ratpoints.Setup.valuation (c.getD (d - 1 - j) 0) p).run.1 ≤ ↑(d - (d - 1 - j)) * n)

theorem Ratpoints.Setup.slopeInvariant_nil (c : List ℤ) (d p val : ℕ) : SlopeInvariant c d p val [] 1

theorem Ratpoints.Setup.SlopeInvariant.append_of_lt {c : List ℤ} {d p val cur vk r : ℕ} {pref suff : List ℕ} {n t : ℤ} (hl : ForIn.toList [:d] = pref ++ cur :: suff) (h : SlopeInvariant c d p val pref n) (hv : (vk, r) = (valuation (c.getD (d - 1 - cur) 0) p).run) (ht : 1 + ↑val - ↑vk = t) (hlt : n < if t ≤ 0 then -(-t / ↑(d - (d - 1 - cur))) else 1 + (t - 1) / ↑(d - (d - 1 - cur))) : SlopeInvariant c d p val (pref ++ [cur]) (if t ≤ 0 then -(-t / ↑(d - (d - 1 - cur))) else 1 + (t - 1) / ↑(d - (d - 1 - cur)))

theorem Ratpoints.Setup.SlopeInvariant.append_of_not_lt {c : List ℤ} {d p val cur vk r : ℕ} {pref suff : List ℕ} {n t : ℤ} (hl : ForIn.toList [:d] = pref ++ cur :: suff) (h : SlopeInvariant c d p val pref n) (hv : (vk, r) = (valuation (c.getD (d - 1 - cur) 0) p).run) (ht : 1 + ↑val - ↑vk = t) (hlt : ¬n < if t ≤ 0 then -(-t / ↑(d - (d - 1 - cur))) else 1 + (t - 1) / ↑(d - (d - 1 - cur))) : SlopeInvariant c d p val (pref ++ [cur]) n

theorem Ratpoints.Setup.SlopeInvariant.one_le_toNat_and_le_mul {c : List ℤ} {d p val : ℕ} {n : ℤ} (h : SlopeInvariant c d p val (ForIn.toList [:d]) n) : 1 ≤ n.toNat ∧ ∀ k < d, 1 + ↑val - ↑(valuation (c.getD k 0) p).run.1 ≤ ↑(d - k) * ↑n.toNat

theorem Ratpoints.Setup.slope_spec (c : List ℤ) (d p val : ℕ) : ⦃ True ⦄ slope c d p val ⦃ fun (n : ℕ) => 1 ≤ n ∧ ∀ k < d, 1 + ↑val - ↑(valuation (c.getD k 0) p).run.1 ≤ ↑(d - k) * ↑n ⦄

The slope of the valuation test of the divisor shape is at least 1 and satisfies (d - k) n ≥ 1 + val - v_p(c_k) for every k < d, the valuation by Ratpoints.Setup.valuation (Ratpoints.veryBig for c_k = 0), since the macro CEIL rounds up.

The divisor set-up

theorem Ratpoints.Setup.setupUs1_spec (c : List ℤ) (d bHigh : ℕ) : ⦃ True ⦄ setupUs1 c d bHigh ⦃ fun (r : Option (List DenInfo × List ℕ)) => ∀ (fac : List (ℕ × ℕ)) (w : ℕ) (divs : List ℕ), (factorLcf (c.getD d 0).natAbs).run = (fac, w) → (squarefreeDivisors (List.map Prod.fst fac) bHigh).run = divs → r = if w = 1 ∧ divs.length < maxDivisors then some (List.map (fun (x : ℕ × ℕ) => { p := x.1, val := x.2, slope := (slope c d x.1 x.2).run }) fac, divs) else none ⦄

The divisor set-up succeeds exactly when the factorization of |c_d| leaves the cofactor 1 (Ratpoints.Setup.factorLcf) and the doubling loop over its primes (Ratpoints.Setup.squarefreeDivisors) gives fewer than Ratpoints.maxDivisors entries; it then gives the primes with their valuations and slopes (Ratpoints.Setup.slope) and that list.

theorem Ratpoints.Setup.run_setupUs1_eq {c : List ℤ} {d bHigh : ℕ} {fac : List (ℕ × ℕ)} {w : ℕ} {divs : List ℕ} (hf : (factorLcf (c.getD d 0).natAbs).run = (fac, w)) (hd : (squarefreeDivisors (List.map Prod.fst fac) bHigh).run = divs) : (setupUs1 c d bHigh).run = if w = 1 ∧ divs.length < maxDivisors then some (List.map (fun (x : ℕ × ℕ) => { p := x.1, val := x.2, slope := (slope c d x.1 x.2).run }) fac, divs) else none

Ratpoints.Setup.setupUs1_spec as a plain statement, which the proofs use without the program logic.

theorem Ratpoints.Setup.exists_isFactorization_of_setupUs1_eq_some {c : List ℤ} {d bHigh : ℕ} {info : List DenInfo} {divisors : List ℕ} (h : (setupUs1 c d bHigh).run = some (info, divisors)) (hc : c.getD d 0 ≠ 0) : ∃ (fac : List (ℕ × ℕ)), IsFactorization (c.getD d 0).natAbs fac ∧ info = List.map (fun (x : ℕ × ℕ) => { p := x.1, val := x.2, slope := (slope c d x.1 x.2).run }) fac

The divisor set-up, when it succeeds for c_d ≠ 0, is made of the factorization of |c_d| (Ratpoints.Setup.factorLcf, with the cofactor 1) and its primes with their valuations and slopes (Ratpoints.Setup.slope).

theorem Ratpoints.Setup.foldl_extendDivisors_eq_binaryDivisors {n bHigh : ℕ} {fac : List (ℕ × ℕ)} (hn : 0 < n) (h : (factorLcf n).run = (fac, 1)) (hb : 1 ≤ bHigh) : List.foldl (extendDivisors bHigh) [1] (List.map Prod.fst fac) = binaryDivisors n bHigh

For a factorization of n ≥ 1 with the cofactor 1, the doubling loop over its primes lists the squarefree divisors of n up to bHigh ≥ 1 in the order of Ratpoints.binaryDivisors.

theorem Ratpoints.Setup.map_snd_run_setupUs1 {c : List ℤ} {d bHigh : ℕ} (hc : c.getD d 0 ≠ 0) (hb : 1 ≤ bHigh) : Option.map Prod.snd (setupUs1 c d bHigh).run = if FactorsByTrialDivision (c.getD d 0).natAbs ∧ (binaryDivisors (c.getD d 0).natAbs bHigh).length < maxDivisors then some (binaryDivisors (c.getD d 0).natAbs bHigh) else none

The divisor set-up of c_d ≠ 0 succeeds exactly when ratpoints factors |c_d| completely and |c_d| has fewer than Ratpoints.maxDivisors squarefree divisors up to bHigh ≥ 1; its divisors are then those of Ratpoints.binaryDivisors, in that order.

theorem Ratpoints.Setup.eq_binaryDivisors_of_setupUs1_eq_some {c : List ℤ} {d bHigh : ℕ} {info : List DenInfo} {divisors : List ℕ} (h : (setupUs1 c d bHigh).run = some (info, divisors)) (hc : c.getD d 0 ≠ 0) (hb : 1 ≤ bHigh) : divisors = binaryDivisors (c.getD d 0).natAbs bHigh

When the divisor set-up of c_d ≠ 0 succeeds, its divisors are those of Ratpoints.binaryDivisors up to bHigh ≥ 1.

theorem Ratpoints.Setup.mem_iff_of_setupUs1_eq_some {c : List ℤ} {d bHigh : ℕ} {info : List DenInfo} {divisors : List ℕ} (h : (setupUs1 c d bHigh).run = some (info, divisors)) (hc : c.getD d 0 ≠ 0) (hbHigh : 1 ≤ bHigh) {s : ℕ} : s ∈ divisors ↔ Squarefree s ∧ s ∣ (c.getD d 0).natAbs ∧ s ≤ bHigh

When the divisor set-up succeeds, its divisors are exactly the squarefree divisors of |c_d| up to the largest denominator bHigh ≥ 1.

theorem Ratpoints.Setup.nodup_of_setupUs1_eq_some {c : List ℤ} {d bHigh : ℕ} {info : List DenInfo} {divisors : List ℕ} (h : (setupUs1 c d bHigh).run = some (info, divisors)) (hc : c.getD d 0 ≠ 0) (hb : 1 ≤ bHigh) : divisors.Nodup

theorem Ratpoints.Setup.fitsLong_mul_of_le_div {x p bHigh : ℕ} (h : x ≤ bHigh / p) (hH : bHigh < 2 ^ 63) : fitsLong ↑(x * p) = true

The products x p that the doubling loop of the C code computes, only for x ≤ ⌊bHigh / p⌋ (find_points.c:876), are at most bHigh, and so longs for a long bHigh.

def Ratpoints.Setup.DenInfo.excludes (e : DenInfo) (b : ℕ) : Bool

Whether the entry e of the valuation test of the divisor shape (Ratpoints.Sieve.denInfoTest) excludes the denominator b: v_p(b) ≥ e.slope with v_p(b) + e.val odd, for the valuation v_p(b) of Ratpoints.Setup.valuation.

Equations

• e.excludes b = (decide (e.slope ≤ (Ratpoints.Setup.valuation (↑b) e.p).run.1) && ((Ratpoints.Setup.valuation (↑b) e.p).run.1 + e.val) % 2 == 1)

theorem Ratpoints.Setup.DenInfo.excludes_eq_false_iff {e : DenInfo} {b : ℕ} : e.excludes b = false ↔ ¬(decide (e.slope ≤ (valuation (↑b) e.p).run.1) && ((valuation (↑b) e.p).run.1 + e.val) % 2 == 1) = true

theorem Ratpoints.Setup.DenInfo.excludes_eq_false_of_sq_eq {c : List ℤ} (hd : degree c % 2 = 1) {p val : ℕ} (hp : Nat.Prime p) (hval : val = padicValNat p (c.getD (degree c) 0).natAbs) {a y : ℤ} {b : ℕ} (hb : b ≠ 0) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : { p := p, val := val, slope := (Setup.slope c (degree c) p val).run }.excludes b = false

An entry of the valuation test, a prime p with the valuation val = v_p(c_d) and its slope (Ratpoints.Setup.slope_spec), does not exclude the denominator b ≥ 1 of a point: for v_p(b) ≥ slope, v_p(b) + val is even (Ratpoints.even_add_of_sq_eq_binaryForm_of_odd).