The output of the search and the refusals

Ratpoints.findPointsWith searches the polynomial that the reversal check of the normalized options hands on, on the search intervals that the Sturm step leaves of those of Ratpoints.searchIntervals, unless it refuses the input or the Sturm step returns before the search (Ratpoints.findPointsWith_eq_ok_iff); its refusals do not depend on the callback, and for every value of the options of the sieve it gives the data and the count of the delivery (Ratpoints.Delivery.deliver) of the list that Ratpoints.findPoints, its instance with the appending callback, returns: the protocol of the delivery (Ratpoints.map_findPointsWith_eq_map_findPoints). That list is the list of the points that the search of the polynomial searched delivers on its search region after the Sturm step (Ratpoints.searchRegion) for a sound test of the sieve, which does not depend on the options of the output (Ratpoints.exists_searchList_of_findPoints_eq_ok); without RATPOINTS_NO_CHECK it is the brute-force reference of the polynomial searched, over the candidate (1, 0) and the denominators of the search with the numerators in that region, mapped back after a reversal, without the points with y < 0 under RATPOINTS_NO_Y (Ratpoints.exists_eq_of_findPoints_eq_ok). Assuming Sturm's theorem (Ratpoints.SturmTheorem) when the Sturm step is on, the region holds the x / z of every point in the search region of the options, and lies inside it: the list is that of the points of the specification in the search region (Ratpoints.InRegion) in the order of Ratpoints.orderedPoints, so that it holds exactly these points, those with y ≥ 0 under RATPOINTS_NO_Y, each once. Under RATPOINTS_NO_CHECK it holds triples (x, 0, z) of normalized pairs (x, z) of height at most H in the search region, each once, among them those of all the points in it, and the list of the search with RATPOINTS_NO_CHECK cleared and RATPOINTS_NO_Y set, with y replaced by 0, is a sublist of it. Ratpoints.findPoints refuses exactly the inputs that the program refuses: with the Sturm step on, those with fewer than two or more than Ratpoints.maxDegree + 1 coefficients, the height bound 0 or one of 2 ^ 63 or more, which is not a long, the binary forms Φ_c that are not squarefree and search intervals that are not well formed (Ratpoints.IntervalsWF); without it, instead of the forms that are not squarefree, those that the test of the leading zeros and, for the whole box (Ratpoints.IsFullBox), the reversal check refuse. Comparator certifies the protocol, the membership, the order, the absence of duplicates, the three statements under RATPOINTS_NO_CHECK and both refusal theorems (comparator/Challenge.lean).

Main definitions

• Ratpoints.IsSearchedPoly: what a successful search guarantees after the refusals, the polynomial that the reversal check hands on, of a degree from 1 to Ratpoints.maxDegree, a height bound that is a positive long, well-formed search intervals of the caller and a Sturm step that does not refuse.

Main statements

• Ratpoints.findPointsWith_eq: the search with a callback and the print channel that prints nothing, as the refusals in the order of the program followed by the search.
• Ratpoints.findPointsWith_eq_ok_iff, Ratpoints.findPointsWith_eq_error_iff, Ratpoints.exists_findPoints_eq_error_iff: what Ratpoints.findPointsWith returns, and its refusals, which do not depend on the callback.
• Ratpoints.map_findPointsWith_eq_map_findPoints: for every value of the options of the sieve, the data and the count of Ratpoints.findPointsWith are those of the delivery of the list of Ratpoints.findPoints.
• Ratpoints.info_total_eq_of_findPointsWith_eq_ok: for every value of the options of the sieve, the data and the count of a successful search with a callback are those of the delivery of the list of Ratpoints.findPoints; Ratpoints.exists_findPointsWith_eq_ok_of_findPoints_eq_ok: the search with a callback succeeds when Ratpoints.findPoints does.
• Ratpoints.exists_searchList_of_findPoints_eq_ok: the list of Ratpoints.findPoints is that of the search on its search region with a sound test of the sieve, the same for every choice of the options of the output.
• Ratpoints.exists_eq_of_findPoints_eq_ok: without RATPOINTS_NO_CHECK, it is the reference of the polynomial searched on its search region, mapped back after a reversal, filtered under RATPOINTS_NO_Y.
• Ratpoints.exists_eq_filter_inRegion_of_findPoints_eq_ok: assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, the list is that of the reference of the polynomial searched over the denominators of its search up to the largest, mapped back after a reversal, filtered by the search region of the options and under RATPOINTS_NO_Y.
• Ratpoints.eq_orderedPoints_of_findPoints_eq_ok: assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, the list is Ratpoints.orderedPoints, filtered under RATPOINTS_NO_Y and by the search region.
• Ratpoints.perm_filter_bruteForce_of_findPoints_eq_ok: assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, the list is a permutation of the reference in the search region, filtered under RATPOINTS_NO_Y.
• Ratpoints.mem_iff_isPoint_of_findPoints_eq_ok: assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, a triple lies in the list exactly when it is a normalized point of height at most H in the search region, with y ≥ 0 under RATPOINTS_NO_Y.
• Ratpoints.toFinset_eq_filter_points_of_findPoints_eq_ok: assuming Sturm's theorem when the Sturm step is on, without the options of the output, its set of elements is that of the points in the search region.
• Ratpoints.findPoints_sturm_neg_eq_ok: assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, the Sturm step changes only the speed.
• Ratpoints.nodup_of_findPoints_eq_ok: for every option, the list has no duplicates.
• Ratpoints.isNormalizedPair_of_mem_of_findPoints_eq_ok_of_noCheck, Ratpoints.mem_of_isPoint_of_findPoints_eq_ok_of_noCheck, Ratpoints.map_sublist_of_findPoints_eq_ok_of_noCheck: under RATPOINTS_NO_CHECK, the list holds triples (x, 0, z) of normalized pairs of height at most H in the search region, among them, assuming Sturm's theorem when the Sturm step is on, (x, 0, z) for every point (x, y, z) in it, and the list of the search with RATPOINTS_NO_CHECK cleared and RATPOINTS_NO_Y set, with y replaced by 0, is a sublist of it.
• Ratpoints.exists_findPoints_eq_error_iff_of_sturm_nonneg: with the Sturm step on, Ratpoints.findPoints refuses exactly the inputs with fewer than two or more than Ratpoints.maxDegree + 1 coefficients, the height bound 0 or one of 2 ^ 63 or more, the forms that are not squarefree and search intervals that are not well formed.
• Ratpoints.exists_findPoints_eq_error_iff_of_sturm_neg: without it, those with fewer than two or more than Ratpoints.maxDegree + 1 coefficients, the height bound 0 or one of 2 ^ 63 or more, a degree d with d + 2 ≤ 2 ⌈n / 2⌉, when the reversal is allowed and the search region is the whole box an even degree with c₀ = c₁ = 0, and search intervals that are not well formed.

Proof

Ratpoints.findPoints and Ratpoints.findPointsWith run the search on the polynomial that the reversal check hands on, with its degree (Ratpoints.Setup.degree_eq_of_reversal_eq_ok), which is positive after the refusals (Ratpoints.Setup.one_le_of_reversal_eq_ok), and its flag of the reversal, with the options of the output as the flags of the check, the normalized range of the denominators (Ratpoints.Options.normalize) and the search intervals of the Sturm step, which are well formed (Ratpoints.intervalsWF_run_searchIntervals, Ratpoints.run_sturmRegion_subset; Ratpoints.exists_isSoundTest_run_searchPoints, Ratpoints.run_searchPoints_eq_deliver, Ratpoints.searchList_of_noCheck_eq_false); the binary form of a reversed polynomial is that of c with x and z exchanged (Ratpoints.Setup.binaryForm_eq_of_reversal_eq_ok), so that its reference, mapped back, is a permutation of that of c (Ratpoints.Sieve.perm_map_swapPoint_bruteForce), and a reversal comes only for the whole box (Ratpoints.isFullBox_of_reversal_normalize_eq_ok). In the terms of the specification of the order, the reversal check hands on the polynomial of Ratpoints.searchedPoly (Ratpoints.searchedPoly_eq_of_reversal_eq_ok), the denominators of the search are those of Ratpoints.searchDenominators up to the largest denominator (Ratpoints.searchDens_one_eq_searchDenominators, Ratpoints.searchDens_eq_filter), and the reference finds over a denominator, and over the candidate (1, 0), the points of Ratpoints.pointsWithDen (Ratpoints.pointsOfDen_eq_pointsWithDen, Ratpoints.pointsOfDen_zero_eq_pointsWithDen). Under RATPOINTS_NO_CHECK the search delivers, for the same sound test of the sieve, the survivors of the numerators prime to the denominators of the search in its search region (Ratpoints.exists_eq_of_mem_searchList_of_noCheck, Ratpoints.mem_region_of_mem_searchList, Ratpoints.searchRegion_subset, distinct by Ratpoints.nodup_searchList_of_noCheck), of which the points with y ≥ 0 that the search delivers without it are a sublist (Ratpoints.map_searchList_sublist). Of the refusals, the heights that are not longs are those of 2 ^ 63 or more (Ratpoints.fitsLong_natCast), and the test of the leading zeros and that of the reversal check stand for Z ^ 2 ∣ Φ_c and X ^ 2 ∣ Φ_c (Ratpoints.not_squarefree_binaryFormPoly_of_lt, Ratpoints.Setup.not_squarefree_binaryFormPoly_of_reversal_eq_error), the refusal of the search intervals is the negation of Ratpoints.IntervalsWF (Ratpoints.run_searchIntervals_eq_none_iff), and after them the Sturm step refuses exactly when the remainder chain of the polynomial searched is none (Ratpoints.run_sturmRegion_eq_error_iff), that is when Φ_c is not squarefree (Ratpoints.Sturm.run_chain_eq_none_iff_of_reversal_eq_ok). Assuming Sturm's theorem when the Sturm step is on, the search region after it holds, of the numerators of the points of a denominator, exactly those in the caller's search intervals (Ratpoints.searchRegion_covers, Ratpoints.searchRegion_subset, Ratpoints.elim_searchRegion_pointsOfDen_filter), and when it returns before the search the polynomial searched has no points at infinity (Ratpoints.elim_searchRegion_pointsOfDen_zero); the filter by the caller's intervals and the denominators from the normalized bLow on is the filter by the search region of the options (Ratpoints.inRegion_ite_swapPoint_iff, Ratpoints.map_append_flatMap_filter_eq_filter_inRegion), which holds the points at infinity and those of the denominators up to the largest of the search (Ratpoints.eq_zero_or_le_toNat_bHigh_normalize_of_inRegion, Ratpoints.perm_map_append_flatMap_searchDens). The search without the Sturm step refuses no other inputs, so that it returns the same list (Ratpoints.findPoints_sturm_neg_eq_ok).

The search with a callback

theorem Ratpoints.findPointsWith_eq (c : List ℤ) (H : ℕ) (s : SieveOptions) (o : Options) {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (info : σ) : findPointsWith c H s o process info = if maxDegree + 1 < c.length then Except.error Refusal.tooManyCoefficients else if c.length < 2 then Except.error Refusal.tooFewCoefficients else if H = 0 ∨ 2 ^ 63 ≤ H then Except.error Refusal.incorrectHeight else if (degree c + 1) / 2 < c.length / 2 then Except.error Refusal.notSquarefree else match Setup.reversal (o.normalize H).reverse c (degree c) with | Except.error e => Except.error e | Except.ok (c', d', rev) => match (searchIntervals H o.domain).run with | none => Except.error Refusal.badArgs | some dom => match (sturmRegion c' d' (o.normalize H).sturm dom).run with | Except.error e => Except.error e | Except.ok none => Except.ok { info := info, total := 0, reversed := rev, useSquares := false, useSquares1 := false, domain := [] } | Except.ok (some (dom', empty)) => Except.ok (searchPoints process c' d' H s.normalize (decide (s.numPrimes < 0)) { reversed := rev, noCheck := o.noCheck, noY := o.noY } (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat dom' empty (fun (x : String) (s : σ) => s) { info := info, total := 0, quit := false }).run

Ratpoints.findPointsWith with the print channel that prints nothing, as the refusals in the order of the program followed by the search: the report of the library prints nothing, and a refusal gives back its error alone.

theorem Ratpoints.findPointsWith_eq_ok_iff {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {σ : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {info : σ} {out : Outcome σ} : findPointsWith c H s o process info = Except.ok out ↔ ∃ (c' : List ℤ) (d' : ℕ) (rev : Bool) (dom : List (Double × Double)) (r : Option (List (Double × Double) × Bool)), c.length ≤ maxDegree + 1 ∧ 2 ≤ c.length ∧ 1 ≤ H ∧ H < 2 ^ 63 ∧ c.length / 2 ≤ (degree c + 1) / 2 ∧ Setup.reversal (o.normalize H).reverse c (degree c) = Except.ok (c', d', rev) ∧ (searchIntervals H o.domain).run = some dom ∧ (sturmRegion c' d' (o.normalize H).sturm dom).run = Except.ok r ∧ out = r.elim { info := info, total := 0, reversed := rev, useSquares := false, useSquares1 := false, domain := [] } fun (x : List (Double × Double) × Bool) => (searchPoints process c' d' H s.normalize (decide (s.numPrimes < 0)) { reversed := rev, noCheck := o.noCheck, noY := o.noY } (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat x.1 x.2 (fun (x : String) (s : σ) => s) { info := info, total := 0, quit := false }).run

Ratpoints.findPointsWith returns the outcome out exactly when it refuses none of its inputs, in the order of the program, and out is, for the result r of the Sturm step, either, when the step returns before the search (find_points.c:4889), the data info with the count 0, the flag of the reversal and no search intervals, or the outcome of the search of the polynomial c' of degree d' that the reversal check of the normalized options hands on, with the flag of the reversal and the options of the output, the normalized range of the denominators and the search intervals that the Sturm step leaves of those of Ratpoints.searchIntervals, from the data info, the count 0 and the flag of the stop clear.

theorem Ratpoints.findPointsWith_eq_error_iff {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {σ σ' : Type} {process : ℤ → ℤ → ℤ → σ → Answer σ} {info : σ} {process' : ℤ → ℤ → ℤ → σ' → Answer σ'} {info' : σ'} {e : Refusal} : findPointsWith c H s o process info = Except.error e ↔ findPointsWith c H s o process' info' = Except.error e

The refusals of Ratpoints.findPointsWith do not depend on the callback or its data.

theorem Ratpoints.exists_findPoints_eq_error_iff {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} : (∃ (e : Refusal), findPoints c H s o = Except.error e) ↔ ∃ (e : Refusal), findPointsWith c H s o appendPoint #[] = Except.error e

theorem Ratpoints.map_findPointsWith_eq_map_findPoints (c : List ℤ) (H : ℕ) (s : SieveOptions) (o : Options) {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (info : σ) : Except.map (fun (out : Outcome σ) => (out.info, out.total)) (findPointsWith c H s o process info) = Except.map (fun (L : List (ℤ × ℤ × ℤ)) => have r := Delivery.deliver process { info := info, total := 0, quit := false } L; (r.info, r.total)) (findPoints c H s o)

For every option, Ratpoints.findPointsWith with a callback and its data gives, besides the bits of the flags and the search intervals written back, the data and the count of the delivery (Ratpoints.Delivery.deliver) of the list that Ratpoints.findPoints returns, from the data, the count 0 and the flag of the stop clear, and it refuses the same inputs with the same errors: the calls of the callback are those of the points of that list, in its order, up to and including the first that stops the search (Ratpoints.run_searchPoints_eq_deliver); when the Sturm step returns before the search, there are no calls and no points; comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.info_total_eq_of_findPointsWith_eq_ok {σ : Type} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {process : ℤ → ℤ → ℤ → σ → Answer σ} {info : σ} {r : Outcome σ} {L : List (ℤ × ℤ × ℤ)} (hr : findPointsWith c H s o process info = Except.ok r) (hL : findPoints c H s o = Except.ok L) : r.info = (Delivery.deliver process { info := info, total := 0, quit := false } L).info ∧ r.total = (Delivery.deliver process { info := info, total := 0, quit := false } L).total

For every value of the options of the sieve, the data and the count of a successful search with a callback are those of the delivery of the points of Ratpoints.findPoints to it, by the protocol of the delivery (Ratpoints.map_findPointsWith_eq_map_findPoints).

theorem Ratpoints.exists_findPointsWith_eq_ok_of_findPoints_eq_ok {σ : Type} {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} (process : ℤ → ℤ → ℤ → σ → Answer σ) (info : σ) {L : List (ℤ × ℤ × ℤ)} (hL : findPoints c H s o = Except.ok L) : ∃ (r : Outcome σ), findPointsWith c H s o process info = Except.ok r

The search with a callback succeeds when Ratpoints.findPoints does: the refusals of Ratpoints.findPointsWith do not depend on the callback (Ratpoints.findPointsWith_eq_error_iff).

The output of Ratpoints.findPoints

structure Ratpoints.IsSearchedPoly (c : List ℤ) (H : ℕ) (o : Options) (c' : List ℤ) (rev : Bool) : Prop

What a successful search of c up to the height H with the options o guarantees after the refusals: the reversal check of the normalized options hands on c' with its degree and the flag rev, the degree of c' lies from 1 to Ratpoints.maxDegree, the height bound is a positive long, the caller's search intervals are well formed, and the Sturm step, when it is on, does not refuse.

• reversal_eq : Setup.reversal (o.normalize H).reverse c (degree c) = Except.ok (c', degree c', rev)

  The reversal check of the normalized options hands on c' with the flag rev.

• degree_pos : 0 < degree c'

  The degree of c' is positive.

• degree_le : degree c' ≤ maxDegree

  The degree of c' is at most Ratpoints.maxDegree.

• one_le : 1 ≤ H

  The height bound is positive.

• lt_two_pow : H < 2 ^ 63

  The height bound is a long.

• intervalsWF : IntervalsWF (domainBits o.domain)

  The caller's search intervals are well formed.

• chain_ne_none : 0 ≤ o.sturm → (Sturm.chain c' (degree c')).run ≠ none

  With the Sturm step on, the remainder chain of c' is not none.

theorem Ratpoints.exists_searchList_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (h : findPoints c H s o = Except.ok L) : ∃ (c' : List ℤ) (rev : Bool) (S : ℕ → ℤ → Bool), IsSearchedPoly c H o c' rev ∧ IsSoundTest c' H (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat S ∧ (L = (searchRegion c' (degree c') H o).elim [] fun (D : List (WithBotTop ℚ × WithBotTop ℚ)) => searchList c' H (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat D S { reversed := rev, noCheck := o.noCheck, noY := o.noY }) ∧ ∀ (noCheck noY : Bool), findPoints c H s { reverse := o.reverse, sturm := o.sturm, noCheck := noCheck, noY := noY, domain := o.domain, bLow := o.bLow, bHigh := o.bHigh } = Except.ok ((searchRegion c' (degree c') H o).elim [] fun (D : List (WithBotTop ℚ × WithBotTop ℚ)) => searchList c' H (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat D S { reversed := rev, noCheck := noCheck, noY := noY })

For every value of the options of the sieve, the list that Ratpoints.findPoints returns is that of the points that the search of the polynomial c' that the reversal check of the normalized options hands on delivers (Ratpoints.searchList), with its flag of the reversal and the options of the output, the normalized range of the denominators and the search region after the Sturm step (Ratpoints.searchRegion), none at all when the Sturm step returns before the search, for a sound test of the sieve (Ratpoints.IsSoundTest) that does not depend on the options of the output: with the other options unchanged, Ratpoints.findPoints returns the list of the search with this test for every choice of them (Ratpoints.exists_isSoundTest_run_searchPoints). The refusals leave a polynomial searched of a degree from 1 to Ratpoints.maxDegree (Ratpoints.Setup.one_le_of_reversal_eq_ok, Ratpoints.Setup.degree_le_of_reversal_eq_ok), well formed search intervals of the caller and a Sturm step that does not refuse (Ratpoints.IsSearchedPoly).

theorem Ratpoints.exists_eq_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) : ∃ (c' : List ℤ) (rev : Bool), IsSearchedPoly c H o c' rev ∧ L = (searchRegion c' (degree c') H o).elim [] fun (D : List (WithBotTop ℚ × WithBotTop ℚ)) => List.filter (fun (p : ℤ × ℤ × ℤ) => !o.noY || decide (0 ≤ p.2.1)) (List.map (if rev = true then Sieve.swapPoint else id) (BruteForce.pointsOfDen c' (degree c') 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c' (degree c') (↑b) (List.filter (fun (a : ℤ) => decide (InIntervals D (↑a / ↑b))) (BruteForce.numerators H))) (searchDens c' (degree c') (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat)))

Without RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list that Ratpoints.findPoints returns is that of the brute-force reference of the polynomial c' that the reversal check of the normalized options hands on, over the candidate (1, 0) and the denominators of its search (Ratpoints.searchDens) with the numerators a with a / b in the search region after the Sturm step (Ratpoints.searchRegion), in this order, mapped back by Ratpoints.Sieve.swapPoint after a reversal, without the points with y < 0 under RATPOINTS_NO_Y (Ratpoints.searchList_of_noCheck_eq_false); none when the Sturm step returns before the search.

The search region of the options

theorem Ratpoints.isFullBox_of_reversal_normalize_eq_ok {o : Options} {H : ℕ} {c c' : List ℤ} {d d' : ℕ} (h : Setup.reversal (o.normalize H).reverse c d = Except.ok (c', d', true)) : IsFullBox o.domain o.bLow o.bHigh H

The search region of the options is the whole box when the reversal check of the normalized options reverses the polynomial.

theorem Ratpoints.inRegion_ite_swapPoint_of_mem_pointsOfDen_zero {o : Options} {H : ℕ} {rev : Bool} (hb : rev = true → IsFullBox o.domain o.bLow o.bHigh H) (hH : 1 ≤ H) {c : List ℤ} {d : ℕ} {p : ℤ × ℤ × ℤ} (hp : p ∈ BruteForce.pointsOfDen c d 0 [1]) : InRegion (domainValues o.domain) o.bLow o.bHigh ((if rev = true then Sieve.swapPoint else id) p)

A point of the candidate (1, 0) of the brute-force reference, mapped back by Ratpoints.Sieve.swapPoint after a reversal, which comes only for the whole box, lies in the search region of the options: it stays at infinity without a reversal, and becomes (0, y, 1) after one.

theorem Ratpoints.inRegion_ite_swapPoint_iff {o : Options} {H : ℕ} {rev : Bool} (hb : rev = true → IsFullBox o.domain o.bLow o.bHigh H) {b : ℕ} (hb1 : 1 ≤ b) (hbB : b ≤ (o.normalize H).bHigh.toNat) {p : ℤ × ℤ × ℤ} (hz : p.2.2 = ↑b) (hx : |p.1| ≤ ↑H) : InRegion (domainValues o.domain) o.bLow o.bHigh ((if rev = true then Sieve.swapPoint else id) p) ↔ (o.normalize H).bLow.toNat ≤ b ∧ (o.domain = [] ∨ InIntervals (domainValues o.domain) (↑p.1 / ↑b))

A triple (a, y, b) with 1 ≤ b ≤ bHigh for the normalized bHigh and |a| ≤ H, mapped back by Ratpoints.Sieve.swapPoint after a reversal, which comes only for the whole box, lies in the search region of the options exactly when b is at least the normalized bLow and a / b lies in the caller's search intervals, when there are some.

theorem Ratpoints.map_append_flatMap_filter_eq_filter_inRegion {o : Options} {H : ℕ} {rev : Bool} (hb : rev = true → IsFullBox o.domain o.bLow o.bHigh H) (hH : 1 ≤ H) {c : List ℤ} {d : ℕ} {l : List ℕ} (hl : ∀ b ∈ l, 1 ≤ b ∧ b ≤ (o.normalize H).bHigh.toNat) : List.map (if rev = true then Sieve.swapPoint else id) (BruteForce.pointsOfDen c d 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c d (↑b) (List.filter (fun (a : ℤ) => decide (o.domain = [] ∨ InIntervals (domainValues o.domain) (↑a / ↑b))) (BruteForce.numerators H))) (List.filter (fun (x : ℕ) => decide ((o.normalize H).bLow.toNat ≤ x)) l)) = List.filter (fun (b : ℤ × ℤ × ℤ) => decide (InRegion (domainValues o.domain) o.bLow o.bHigh b)) (List.map (if rev = true then Sieve.swapPoint else id) (BruteForce.pointsOfDen c d 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c d (↑b) (BruteForce.numerators H)) l))

The points at infinity and the points of the denominators b of l, within 1, …, bHigh for the normalized bHigh, from the normalized bLow on and with the numerators a with a / b in the caller's search intervals, when there are some, mapped back after a reversal, are those of all the denominators of l in the search region of the options (Ratpoints.inRegion_ite_swapPoint_iff), the whole box after a reversal.

theorem Ratpoints.perm_map_append_flatMap_searchDens {o : Options} {H : ℕ} {c c' : List ℤ} {rev : Bool} (hr : Setup.reversal (o.normalize H).reverse c (degree c) = Except.ok (c', degree c', rev)) (hH : 1 ≤ H) : (List.map (if rev = true then Sieve.swapPoint else id) (BruteForce.pointsOfDen c' (degree c') 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c' (degree c') (↑b) (BruteForce.numerators H)) (searchDens c' (degree c') 1 (o.normalize H).bHigh.toNat))).Perm (List.filter (fun (p : ℤ × ℤ × ℤ) => decide (p.2.2 = 0 ∨ 1 ≤ p.2.2 ∧ p.2.2 ≤ ↑(o.normalize H).bHigh.toNat)) (bruteForce c H))

The points at infinity and the points of the denominators of the search from 1 to the normalized bHigh of the polynomial c' that the reversal check of the normalized options hands on, mapped back after a reversal, are a permutation of the brute-force reference of c restricted to the points at infinity and the denominators up to the normalized bHigh (Ratpoints.perm_filter_bruteForce_append_flatMap_searchDens, Ratpoints.Sieve.perm_map_swapPoint_bruteForce), which is H after a reversal.

theorem Ratpoints.eq_zero_or_le_toNat_bHigh_normalize_of_inRegion {o : Options} {D : List (WithBotTop ℚ × WithBotTop ℚ)} {H : ℕ} {p : ℤ × ℤ × ℤ} (hz : 0 ≤ p.2.2) (hzH : p.2.2 ≤ ↑H) (h : InRegion D o.bLow o.bHigh p) : p.2.2 = 0 ∨ 1 ≤ p.2.2 ∧ p.2.2 ≤ ↑(o.normalize H).bHigh.toNat

A triple with a denominator from 0 to H in the search region of the options is at infinity or has a denominator from 1 to the normalized largest denominator.

theorem Ratpoints.filter_filter_bruteForce_eq {o : Options} (D : List (WithBotTop ℚ × WithBotTop ℚ)) (c : List ℤ) (H : ℕ) (t : ℤ × ℤ × ℤ → Bool) : List.filter (fun (p : ℤ × ℤ × ℤ) => t p && decide (InRegion D o.bLow o.bHigh p)) (List.filter (fun (p : ℤ × ℤ × ℤ) => decide (p.2.2 = 0 ∨ 1 ≤ p.2.2 ∧ p.2.2 ≤ ↑(o.normalize H).bHigh.toNat)) (bruteForce c H)) = List.filter (fun (p : ℤ × ℤ × ℤ) => t p && decide (InRegion D o.bLow o.bHigh p)) (bruteForce c H)

The points of the brute-force reference at infinity or with a denominator up to the normalized largest denominator that pass a test t and lie in the search region of the options are those of the reference that do: the region holds no others (Ratpoints.eq_zero_or_le_toNat_bHigh_normalize_of_inRegion).

Assuming Sturm's theorem

theorem Ratpoints.elim_searchRegion_pointsOfDen_zero {c : List ℤ} {d H : ℕ} {o : Options} (hdom : IntervalsWF (domainBits o.domain)) (hc : 0 ≤ o.sturm → (Sturm.chain c d).run ≠ none) : ((searchRegion c d H o).elim [] fun (x : List (WithBotTop ℚ × WithBotTop ℚ)) => BruteForce.pointsOfDen c d 0 [1]) = BruteForce.pointsOfDen c d 0 [1]

When the Sturm step returns before the search, the polynomial searched has no points at infinity: it does so only for even degree and a leading coefficient that is not a square (Ratpoints.searchRegion_eq_none).

theorem Ratpoints.elim_searchRegion_pointsOfDen_filter {c : List ℤ} {d H : ℕ} {o : Options} (hS : 0 ≤ o.sturm → SturmTheorem) (hdom : IntervalsWF (domainBits o.domain)) (hd : d = degree c) (hd0 : 0 < d) (hd57 : d < 2 ^ 57) (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) (hc : 0 ≤ o.sturm → (Sturm.chain c d).run ≠ none) {b : ℕ} (hb : 0 < b) : ((searchRegion c d H o).elim [] fun (D : List (WithBotTop ℚ × WithBotTop ℚ)) => BruteForce.pointsOfDen c d (↑b) (List.filter (fun (a : ℤ) => decide (InIntervals D (↑a / ↑b))) (BruteForce.numerators H))) = BruteForce.pointsOfDen c d (↑b) (List.filter (fun (a : ℤ) => decide (o.domain = [] ∨ InIntervals (domainValues o.domain) (↑a / ↑b))) (BruteForce.numerators H))

Assuming Sturm's theorem when the step is on, the points of the denominator b ≥ 1 of the polynomial c of degree 0 < d < 2 ^ 57 with the numerators a with a / b in the search region after the Sturm step, none when it returns before the search, are those with a / b in the caller's search intervals, when there are some (Ratpoints.searchRegion_covers, Ratpoints.searchRegion_subset): on a point, F(a, b) = y ^ 2 ≥ 0.

theorem Ratpoints.exists_eq_filter_inIntervals_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) : ∃ (c' : List ℤ) (rev : Bool), Setup.reversal (o.normalize H).reverse c (degree c) = Except.ok (c', degree c', rev) ∧ 1 ≤ H ∧ L = List.filter (fun (p : ℤ × ℤ × ℤ) => !o.noY || decide (0 ≤ p.2.1)) (List.map (if rev = true then Sieve.swapPoint else id) (BruteForce.pointsOfDen c' (degree c') 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c' (degree c') (↑b) (List.filter (fun (a : ℤ) => decide (o.domain = [] ∨ InIntervals (domainValues o.domain) (↑a / ↑b))) (BruteForce.numerators H))) (searchDens c' (degree c') (o.normalize H).bLow.toNat (o.normalize H).bHigh.toNat)))

Assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list that Ratpoints.findPoints returns is the brute-force reference of the polynomial c' that the reversal check of the normalized options hands on, over the candidate (1, 0) and the denominators of its search with the numerators a with a / b in the caller's search intervals, when there are some, in this order, mapped back after a reversal, without the points with y < 0 under RATPOINTS_NO_Y: the search region after the Sturm step holds exactly these numerators of the points (Ratpoints.exists_eq_of_findPoints_eq_ok, Ratpoints.elim_searchRegion_pointsOfDen_zero, Ratpoints.elim_searchRegion_pointsOfDen_filter).

theorem Ratpoints.exists_eq_filter_inRegion_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) : ∃ (c' : List ℤ) (rev : Bool), Setup.reversal (o.normalize H).reverse c (degree c) = Except.ok (c', degree c', rev) ∧ 1 ≤ H ∧ L = List.filter (fun (p : ℤ × ℤ × ℤ) => (!o.noY || decide (0 ≤ p.2.1)) && decide (InRegion (domainValues o.domain) o.bLow o.bHigh p)) (List.map (if rev = true then Sieve.swapPoint else id) (BruteForce.pointsOfDen c' (degree c') 0 [1] ++ List.flatMap (fun (b : ℕ) => BruteForce.pointsOfDen c' (degree c') (↑b) (BruteForce.numerators H)) (searchDens c' (degree c') 1 (o.normalize H).bHigh.toNat)))

Assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list that Ratpoints.findPoints returns is the brute-force reference of the polynomial c' that the reversal check of the normalized options hands on, over the candidate (1, 0) and the denominators of its search from 1 to the normalized largest denominator, in this order, mapped back after a reversal, filtered by the search region of the options (Ratpoints.InRegion) and under RATPOINTS_NO_Y by y ≥ 0 (Ratpoints.map_append_flatMap_filter_eq_filter_inRegion).

theorem Ratpoints.perm_filter_bruteForce_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) : L.Perm (List.filter (fun (p : ℤ × ℤ × ℤ) => (!o.noY || decide (0 ≤ p.2.1)) && decide (InRegion (domainValues o.domain) o.bLow o.bHigh p)) (bruteForce c H))

Assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list that Ratpoints.findPoints returns is a permutation of the brute-force reference in the search region of the options (Ratpoints.InRegion), without the points with y < 0 under RATPOINTS_NO_Y: the search region holds the points at infinity and those with a denominator up to the largest of the search (Ratpoints.eq_zero_or_le_toNat_bHigh_normalize_of_inRegion), whose points the search gives (Ratpoints.perm_map_append_flatMap_searchDens).

theorem Ratpoints.eq_orderedPoints_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) : L = List.filter (fun (p : ℤ × ℤ × ℤ) => (!o.noY || decide (0 ≤ p.2.1)) && decide (InRegion (domainValues o.domain) o.bLow o.bHigh p)) (orderedPoints maxDivisors (o.reverse && decide (IsFullBox o.domain o.bLow o.bHigh H)) c H (denominatorBound o.bHigh H))

Assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list that Ratpoints.findPoints returns is Ratpoints.orderedPoints for the switch of the reversal of the normalized options and the largest denominator of the search (Ratpoints.denominatorBound), the points in the order of the specification, those in the search region of the options (Ratpoints.InRegion), without those with y < 0 under RATPOINTS_NO_Y; comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.nodup_map_bruteForce_of_reversal_eq_ok {allow rev : Bool} {c c' : List ℤ} {d' : ℕ} (hr : Setup.reversal allow c (degree c) = Except.ok (c', d', rev)) (H : ℕ) : (List.map (if rev = true then Sieve.swapPoint else id) (bruteForce c' H)).Nodup

The brute-force reference of the polynomial that the reversal check hands on, mapped back after a reversal, has no duplicates: it is a permutation of the reference of c after a reversal (Ratpoints.Sieve.perm_map_swapPoint_bruteForce).

The main theorems

theorem Ratpoints.mem_iff_isPoint_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) {p : ℤ × ℤ × ℤ} : p ∈ L ↔ IsPoint c H p ∧ (o.noY = true → 0 ≤ p.2.1) ∧ InRegion (domainValues o.domain) o.bLow o.bHigh p

Assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, for every value of the options of the sieve and the other options, a triple lies in the list that Ratpoints.findPoints returns exactly when it is a normalized point of height at most H in the search region of the options (Ratpoints.InRegion), with y ≥ 0 under RATPOINTS_NO_Y; comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.nodup_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (h : findPoints c H s o = Except.ok L) : L.Nodup

For every option, the list that Ratpoints.findPoints returns has no duplicates: without RATPOINTS_NO_CHECK it is a sublist of a permutation of the brute-force reference, filtered under RATPOINTS_NO_Y and by the search region, and under RATPOINTS_NO_CHECK the survivors are distinct (Ratpoints.nodup_searchList_of_noCheck); comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.toFinset_eq_filter_points_of_findPoints_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = false) (hy : o.noY = false) : L.toFinset = Finset.filter (InRegion (domainValues o.domain) o.bLow o.bHigh) (points c H)

Assuming Sturm's theorem when the Sturm step is on, without the options of the output, the set of the elements of the list that Ratpoints.findPoints returns is the set of the points in the search region of the options.

RATPOINTS_NO_CHECK

theorem Ratpoints.isNormalizedPair_of_mem_of_findPoints_eq_ok_of_noCheck {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = true) {q : ℤ × ℤ × ℤ} (hq : q ∈ L) : q.2.1 = 0 ∧ IsNormalizedPair H q.1 q.2.2 ∧ InRegion (domainValues o.domain) o.bLow o.bHigh q

Under RATPOINTS_NO_CHECK, for every value of the options of the sieve, every triple (x, y, z) of the list that Ratpoints.findPoints returns, whether it is a point or not, has y = 0 and its pair (x, z) normalized and of height at most H, and lies in the search region of the options (Ratpoints.exists_eq_of_mem_searchList_of_noCheck, Ratpoints.mem_region_of_mem_searchList, Ratpoints.searchRegion_subset); comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.map_sublist_of_findPoints_eq_ok_of_noCheck {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L L' : List (ℤ × ℤ × ℤ)} (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = true) (h' : findPoints c H s { reverse := o.reverse, sturm := o.sturm, noY := true, domain := o.domain, bLow := o.bLow, bHigh := o.bHigh } = Except.ok L') : (List.map (fun (q : ℤ × ℤ × ℤ) => (q.1, 0, q.2.2)) L').Sublist L

Under RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list L' that Ratpoints.findPoints returns for the same input with RATPOINTS_NO_CHECK cleared and RATPOINTS_NO_Y set, with y replaced by 0, is a sublist of the list L that it returns: both searches run with the same test of the sieve and the same search region, so that the points come in the same order among the survivors (Ratpoints.map_searchList_sublist); comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.mem_of_isPoint_of_findPoints_eq_ok_of_noCheck {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (h : findPoints c H s o = Except.ok L) (hc : o.noCheck = true) {p : ℤ × ℤ × ℤ} (hp : IsPoint c H p) (hr : InRegion (domainValues o.domain) o.bLow o.bHigh p) : (p.1, 0, p.2.2) ∈ L

Assuming Sturm's theorem when the Sturm step is on, under RATPOINTS_NO_CHECK, for every value of the options of the sieve, the list that Ratpoints.findPoints returns has the triple (x, 0, z) of every normalized point (x, y, z) of height at most H in the search region of the options: the point (x, |y|, z) is in the list of the search with RATPOINTS_NO_CHECK cleared and RATPOINTS_NO_Y set (Ratpoints.map_sublist_of_findPoints_eq_ok_of_noCheck); comparator certifies this (comparator/Challenge.lean).

The refusals

theorem Ratpoints.exists_findPoints_eq_error_iff_of_sturm_nonneg {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} (hs : 0 ≤ o.sturm) : (∃ (e : Refusal), findPoints c H s o = Except.error e) ↔ c.length < 2 ∨ maxDegree + 1 < c.length ∨ H = 0 ∨ 2 ^ 63 ≤ H ∨ ¬Squarefree (binaryFormPoly c) ∨ ¬IntervalsWF (domainBits o.domain)

With the Sturm step on (0 ≤ o.sturm, as in a run of the program without options), Ratpoints.findPoints refuses exactly the inputs with fewer than two or more than Ratpoints.maxDegree + 1 coefficients, the height bound 0 or one of 2 ^ 63 or more, which is not a long (Ratpoints.fitsLong_natCast), the binary forms Ratpoints.binaryFormPoly c that are not squarefree, and search intervals that are not well formed (Ratpoints.IntervalsWF), for all options of the sieve, whether the reversal is allowed or not; comparator certifies this (comparator/Challenge.lean).

theorem Ratpoints.exists_reversal_normalize_eq_error_iff {o : Options} {H : ℕ} {c : List ℤ} {d : ℕ} : (∃ (e : Refusal), Setup.reversal (o.normalize H).reverse c d = Except.error e) ↔ o.reverse = true ∧ IsFullBox o.domain o.bLow o.bHigh H ∧ d % 2 = 0 ∧ c.getD 0 0 = 0 ∧ c.getD 1 0 = 0

The reversal check of the normalized options refuses exactly when the reversal is allowed, the search region is the whole box (Ratpoints.IsFullBox), the degree is even and c₀ = c₁ = 0.

theorem Ratpoints.exists_findPoints_eq_error_iff_of_sturm_neg {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} (hs : o.sturm < 0) : (∃ (e : Refusal), findPoints c H s o = Except.error e) ↔ c.length < 2 ∨ maxDegree + 1 < c.length ∨ H = 0 ∨ 2 ^ 63 ≤ H ∨ degree c + 2 ≤ 2 * (c.length / 2) ∨ o.reverse = true ∧ IsFullBox o.domain o.bLow o.bHigh H ∧ degree c % 2 = 0 ∧ c.getD 0 0 = 0 ∧ c.getD 1 0 = 0 ∨ ¬IntervalsWF (domainBits o.domain)

Without the Sturm step (o.sturm < 0, the option -s of the program), Ratpoints.findPoints refuses, besides the coefficient lists of fewer than two or more than Ratpoints.maxDegree + 1 entries and the height bound 0 or one of 2 ^ 63 or more, which is not a long (Ratpoints.fitsLong_natCast), exactly the forms whose leading zeros lower ⌈n / 2⌉, for n + 1 coefficients, that is d + 2 ≤ 2 ⌈n / 2⌉ for the degree d, and those of even degree with c₀ = c₁ = 0 when the reversal is allowed and the search region is the whole box (Ratpoints.IsFullBox), all of them forms that are not squarefree, but not all such forms; and the search intervals that are not well formed (Ratpoints.IntervalsWF); comparator certifies this (comparator/Challenge.lean), so that a Ratpoints.findPoints that refused every input under -s would not pass.

The Sturm step changes only the speed

theorem Ratpoints.findPoints_sturm_neg_eq_ok {c : List ℤ} {H : ℕ} {s : SieveOptions} {o : Options} {L : List (ℤ × ℤ × ℤ)} (hS : 0 ≤ o.sturm → SturmTheorem) (hc : o.noCheck = false) (h : findPoints c H s o = Except.ok L) : findPoints c H s { reverse := o.reverse, sturm := -1, noCheck := o.noCheck, noY := o.noY, domain := o.domain, bLow := o.bLow, bHigh := o.bHigh } = Except.ok L

Assuming Sturm's theorem when the Sturm step is on, without RATPOINTS_NO_CHECK, the Sturm step changes only the speed of the search: the search without it returns the same list.

The axioms of the main theorems