The search delivers the points of a sound sieve

The search of the polynomial that the set-up hands on delivers to the callback, for every value of the options of the sieve, the points at infinity followed, for the denominators from bLow to bHigh that the loop of its shape visits in its order (Ratpoints.searchDens), by the points of the check with the flags of the search of the numerators a with a / b in the search intervals over the values of their ends (Ratpoints.InIntervals) that a test of the sieve lets through (Ratpoints.searchList), none when the Sturm step has left no interval, and it returns when the callback stops the search; the test, the sieve with the moduli of the block of each denominator, depends neither on the callback nor on the flags of the output, but on the search intervals, which the estimate of the run reads, and with it the choice of the moduli and the decisions of the correction, and it lets the numerator of every point through (Ratpoints.IsSoundTest), also when the search takes one of its exits, where the curve has no points (Ratpoints.exists_isSoundTest_run_searchPoints), for well-formed search intervals. So the search with a callback delivers the list that the search with the appending callback returns (Ratpoints.run_searchPoints_eq_deliver), and without RATPOINTS_NO_CHECK that list is the brute-force reference over the candidate (1, 0) and the denominators of the search with the numerators in the search intervals, mapped by Ratpoints.Sieve.swapPoint when the flag of the reversal is set, without the points with y < 0 under RATPOINTS_NO_Y (Ratpoints.searchList_of_noCheck_eq_false): the points of the reference with the denominators from bLow to bHigh in another order, except where the shape visits the denominators in increasing order, every shape but that of the divisors of the leading coefficient times squares (Ratpoints.perm_filter_bruteForce_append_flatMap_searchDens), filtered by the search intervals; without the flag of the reversal they lie in the search region (Ratpoints.mem_region_of_mem_searchList). What Ratpoints.findPoints and Ratpoints.findPointsWith return, and their refusals, are in Ratpoints.Proof.Output.

Main definitions

• Ratpoints.searchList, Ratpoints.IsSoundTest: the points that the search delivers for a test of the numerators, and a test that lets the numerator of every point through.
• Ratpoints.Sieve.IsSoundRun: what the run of the search needs of its arguments.

Main statements

• Ratpoints.searchList_of_noCheck_eq_false: without RATPOINTS_NO_CHECK, the points that the search delivers for a sound test are those of the brute-force reference with the numerators in the search intervals, mapped after a reversal, without those with y < 0 under RATPOINTS_NO_Y.
• Ratpoints.exists_eq_of_mem_searchList_of_noCheck, Ratpoints.nodup_searchList_of_noCheck: under RATPOINTS_NO_CHECK, the search delivers distinct triples (x, 0, z) of normalized pairs (x, z) of height at most H (Ratpoints.IsNormalizedPair), whatever the test; Ratpoints.map_searchList_sublist: the points that it delivers without RATPOINTS_NO_CHECK and with RATPOINTS_NO_Y, with y replaced by 0, are a sublist of them, for the same test.
• Ratpoints.mem_region_of_mem_searchList, Ratpoints.searchList_nil: without the flag of the reversal, the points that the search delivers lie in the search region; for no search interval they are the points at infinity.
• Ratpoints.exists_isSoundTest_run_sieveRun: the run of the shape that the search chooses, with sound arguments, a well-formed first decision and the bounds of well-formed search intervals, delivers the points of the numerators in the search intervals that a sound test lets through.
• Ratpoints.exists_isSoundTest_run_searchPoints: for 1 ≤ H < 2 ^ 63 and the degree of the polynomial, there is a sound test for which the search, with any callback, flags and delivery whose flag of the stop is clear and the print channel that prints nothing, gives the data and the count of the delivery of the points of Ratpoints.searchList for the denominators from bLow ≥ 1 to bHigh ≤ H and the values of well-formed search intervals, none when the Sturm step has left no interval.
• Ratpoints.run_searchPoints_eq_deliver: the search with a callback gives the data and the count of the delivery of the list of the search with the appending callback; Ratpoints.exists_isSoundTest_run_searchPoints_appendPoint: the search with the appending callback gives the list of Ratpoints.searchList, for every choice of the flags.

Proof

The run delivers, over the denominators of the listing of its shape that pass its tests, the points of the numerators that pass the class word and survive the entries of the first three stages of the decision of the block of the denominator (Ratpoints.Sieve.exists_run_sieveRun_eq_deliver), the numerators of each denominator lying in the ranges that the bounds of well-formed search intervals give for it (Ratpoints.Sieve.rangesFor_run_exactBounds), which are those with a / b in the intervals (Ratpoints.Sieve.inRanges_numeratorRanges). This test is sound: every numerator of a point passes the word of the class of its denominator and survives the sieve entries, when they are sound (Ratpoints.Sieve.classBit_and_survives_of_ne_nil), and every denominator of a point passes the filter and the tests of the shape that Ratpoints.Sieve.runSetup chooses: the squares for odd degree and |c_d| = 1 (Ratpoints.isSquare_of_sq_eq_binaryForm_of_odd, Ratpoints.Sieve.squaresDens_eq_filter), the divisors with their valuation test (Ratpoints.Sieve.run_denInfoTest_of_sq_eq), the words with the forbidden divisors and the Jacobi test (Ratpoints.Sieve.toList_run_wordsDens, Ratpoints.Sieve.getLsbD_denBits_and_all_of_sq_eq, Ratpoints.Sieve.run_wordsTest_of_sq_eq), and every denominator, by the class test (Ratpoints.Sieve.getElem!_twoAdic_ne_zero). The result of the choice of the moduli is what the run needs (Ratpoints.sievingInfo_spec), and when the choice exits, the curve has no points; when the search takes the 2-adic exit, no class of the denominators admits a numerator, so that the curve has no points either (Ratpoints.Sieve.not_isPoint_of_denBits_eq_zero).

Implementation notes

The search is proved by cases on the values of its components, the classes and the word of the 2-adic information, the 2-adic exit and the result of the choice of the moduli, which do not depend on the callback or the flags, so that the test of the sieve is chosen after them; the data and the count of the search along its paths, for these values, are proved with vcgen, which reads the components through private specifications ⦃True⦄ x ⦃fun r ↦ r = Id.run x⦄, so that its verification conditions speak of their values.

The points at infinity and the points of a denominator

theorem Ratpoints.BruteForce.horner_scaledCoeffs_one_zero (c : List ℤ) (d : ℕ) : horner (scaledCoeffs c d 0) 1 = c.getD d 0

theorem Ratpoints.BruteForce.pointsOfDen_zero_singleton_one (c : List ℤ) (d : ℕ) : pointsOfDen c d 0 [1] = pointsAbove 1 0 (c.getD d 0 * if d % 2 = 1 then 0 else 1)

The points at infinity of the brute-force reference, those of the candidate (1, 0), are those of the value F(1, 0): c_d for even d and 0 for odd d.

theorem Ratpoints.Sieve.survives_of_mem_pointsOfDen {c : List ℤ} {entries : List SieveEntry} (hent : ∀ e ∈ entries, SieveEntry.IsSound c e) {b : ℕ} {xs : List ℤ} {q : ℤ × ℤ × ℤ} (hq : q ∈ BruteForce.pointsOfDen c (BruteForce.degree c) (↑b) xs) : survives entries b q.1 = true

theorem Ratpoints.Sieve.pointsAtInfinityList_eq_filter_map_pointsOfDen {fl : CheckFlags} (hc : fl.noCheck = false) {c : List ℤ} {d : ℕ} (h : d % 2 = 1 ∨ c.getD d 0 ≠ 0) : pointsAtInfinityList c d fl = List.filter (fun (p : ℤ × ℤ × ℤ) => !fl.noY || decide (0 ≤ p.2.1)) (List.map (if fl.reversed = true then swapPoint else id) (BruteForce.pointsOfDen c d 0 [1]))

Without RATPOINTS_NO_CHECK, for odd d or c_d ≠ 0, the points at infinity that the search delivers are those of the candidate (1, 0) of the brute-force reference, mapped by Ratpoints.Sieve.swapPoint after a reversal, without the point with y < 0 under RATPOINTS_NO_Y (Ratpoints.Sieve.pointsAtInfinityList_of_noCheck_eq_false).

theorem Ratpoints.Sieve.pointsAtInfinityList_eq_nil_of_pointsOfDen_eq_nil {c : List ℤ} {d : ℕ} (h : BruteForce.pointsOfDen c d 0 [1] = []) (fl : CheckFlags) : pointsAtInfinityList c d fl = []

When the brute-force reference has no point at infinity, for even d and c_d not a square, the search delivers none, whatever the flags.

theorem Ratpoints.Sieve.classBit_and_survives_of_ne_nil {c : List ℤ} {entries : List SieveEntry} (hent : ∀ e ∈ entries, SieveEntry.IsSound c e) {b : ℕ} {a : ℤ} (h : BruteForce.pointsOfDen c (degree c) ↑b [a] ≠ []) : classBit (twoAdic c (degree c)).run[b % 64]! a = true ∧ survives entries b a = true

The class word of the denominator b and sound sieve entries let the numerator of every point over b through (Ratpoints.Sieve.classBit_twoAdic_of_sq_eq, Ratpoints.Sieve.survives_of_mem_pointsOfDen).

The points that the search delivers

def Ratpoints.searchList (c : List ℤ) (H bLow bHigh : ℕ) (D : List (WithBotTop ℚ × WithBotTop ℚ)) (S : ℕ → ℤ → Bool) (fl : CheckFlags) : List (ℤ × ℤ × ℤ)

The points that the search of the polynomial with the coefficient list c, of its degree, delivers for the height H, the denominators from bLow to bHigh, the search intervals D over the values of their ends and the flags fl of the check, for the test S b a of the numerators a over the denominators b of the search: the points at infinity (Ratpoints.Sieve.pointsAtInfinityList), then, for the denominators b of the search in the order of its loop (Ratpoints.searchDens), the points of the check with the flags (Ratpoints.Sieve.checkNumWith) of the numerators -H, …, H with a / b in one of the intervals (Ratpoints.InIntervals) that pass S b. For every value of the options of the sieve the test of the sieve is one that lets the numerator of every point through (Ratpoints.IsSoundTest, Ratpoints.exists_isSoundTest_run_searchPoints).

Equations

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

def Ratpoints.IsSoundTest (c : List ℤ) (H bLow bHigh : ℕ) (S : ℕ → ℤ → Bool) : Prop

A test S b a of the numerators a of -H, …, H over the denominators b from bLow to bHigh of the search (Ratpoints.searchDens) that lets the numerator of every point of the curve y ^ 2 = F(x, z) with the coefficient list c through.

Equations

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

theorem Ratpoints.searchList_of_noCheck_eq_false {c : List ℤ} {H bLow bHigh : ℕ} {S : ℕ → ℤ → Bool} (hS : IsSoundTest c H bLow bHigh S) (hc : 0 < degree c) (D : List (WithBotTop ℚ × WithBotTop ℚ)) {fl : CheckFlags} (hn : fl.noCheck = false) : searchList c H bLow bHigh D S fl = List.filter (fun (p : ℤ × ℤ × ℤ) => !fl.noY || decide (0 ≤ p.2.1)) (List.map (if fl.reversed = 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) bLow bHigh)))

Without RATPOINTS_NO_CHECK, for a sound test and c of positive degree, the points that the search delivers are those of the brute-force reference over the candidate (1, 0) and the denominators of the search with the numerators a of -H, …, H with a / b in one of the search intervals, in this order, mapped by Ratpoints.Sieve.swapPoint after a reversal, without those with y < 0 under RATPOINTS_NO_Y: a sound test leaves out only numerators without points (Ratpoints.BruteForce.pointsOfDen_filter_of_ne).

theorem Ratpoints.searchList_false {c : List ℤ} (H bLow bHigh : ℕ) (D : List (WithBotTop ℚ × WithBotTop ℚ)) {fl : CheckFlags} (h : Sieve.pointsAtInfinityList c (degree c) fl = []) : searchList c H bLow bHigh D (fun (x : ℕ) (x_1 : ℤ) => false) fl = []

With the test that lets no numerator through, and no point at infinity, the search delivers nothing.

theorem Ratpoints.searchList_eq_map (c : List ℤ) (H bLow bHigh : ℕ) (D : List (WithBotTop ℚ × WithBotTop ℚ)) (S : ℕ → ℤ → Bool) (fl : CheckFlags) : searchList c H bLow bHigh D S fl = List.map (if fl.reversed = true then Sieve.swapPoint else id) (searchList c H bLow bHigh D S { noCheck := fl.noCheck, noY := fl.noY })

The points that the search delivers are those of the search without the flag of the reversal, mapped by Ratpoints.Sieve.swapPoint when it is set.

theorem Ratpoints.exists_eq_of_mem_searchList_of_noCheck {c : List ℤ} {H bLow bHigh : ℕ} {D : List (WithBotTop ℚ × WithBotTop ℚ)} {S : ℕ → ℤ → Bool} {fl : CheckFlags} (hc : fl.noCheck = true) (hH : 1 ≤ H) (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) {q : ℤ × ℤ × ℤ} (hq : q ∈ searchList c H bLow bHigh D S fl) : ∃ (x : ℤ) (z : ℤ), q = (x, 0, z) ∧ IsNormalizedPair H x z

Under RATPOINTS_NO_CHECK, the search with the denominators from bLow ≥ 1 to bHigh ≤ H delivers triples (x, 0, z) of pairs (x, z) of normalized points of height at most H (Ratpoints.IsNormalizedPair): the survivors (a, 0, b) of the numerators a prime to the denominators b of the search and the point (1, 0, 0) at infinity, mapped after a reversal (Ratpoints.IsNormalizedPair.swapPoint).

theorem Ratpoints.mem_region_of_mem_searchList {c : List ℤ} {H bLow bHigh : ℕ} {D : List (WithBotTop ℚ × WithBotTop ℚ)} {S : ℕ → ℤ → Bool} {fl : CheckFlags} (hr : fl.reversed = false) (hbLow : 1 ≤ bLow) {q : ℤ × ℤ × ℤ} (hq : q ∈ searchList c H bLow bHigh D S fl) : q.2.2 = 0 ∨ ↑bLow ≤ q.2.2 ∧ q.2.2 ≤ ↑bHigh ∧ InIntervals D (↑q.1 / ↑q.2.2)

Without the flag of the reversal, a point that the search delivers is at infinity, or its denominator lies from bLow ≥ 1 to bHigh and its x / z in one of the search intervals.

theorem Ratpoints.searchList_nil (c : List ℤ) (H bLow bHigh : ℕ) (S : ℕ → ℤ → Bool) (fl : CheckFlags) : searchList c H bLow bHigh [] S fl = Sieve.pointsAtInfinityList c (degree c) fl

Without search intervals, the search delivers its points at infinity only.

theorem Ratpoints.nodup_searchList_of_noCheck {c : List ℤ} {H bLow bHigh : ℕ} (hH : 1 ≤ H) (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) (D : List (WithBotTop ℚ × WithBotTop ℚ)) (S : ℕ → ℤ → Bool) {fl : CheckFlags} (hc : fl.noCheck = true) : (searchList c H bLow bHigh D S fl).Nodup

Under RATPOINTS_NO_CHECK, the points that the search delivers are distinct: the survivors (a, 0, b) are distinct pairs over distinct denominators b ≥ 1 (Ratpoints.nodup_searchDens), the point at infinity apart, and the map of the reversal is injective on the normalized pairs (Ratpoints.Sieve.swapPoint_inj).

theorem Ratpoints.map_searchList_sublist (c : List ℤ) (H bLow bHigh : ℕ) (D : List (WithBotTop ℚ × WithBotTop ℚ)) (S : ℕ → ℤ → Bool) (rev noY : Bool) : (List.map (fun (q : ℤ × ℤ × ℤ) => (q.1, 0, q.2.2)) (searchList c H bLow bHigh D S { reversed := rev, noY := true })).Sublist (searchList c H bLow bHigh D S { reversed := rev, noCheck := true, noY := noY })

Without RATPOINTS_NO_CHECK and with RATPOINTS_NO_Y, the points that the search delivers, with y replaced by 0, are a sublist of those that it delivers under RATPOINTS_NO_CHECK with the same test: each numerator gives at most its point with y ≥ 0 in the one case and its survivor in the other (Ratpoints.Sieve.map_checkNumWith_sublist).

theorem Ratpoints.isSoundTest_false_of_forall_not_isPoint {c : List ℤ} {H bLow bHigh : ℕ} (hH : 1 ≤ H) (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) (h : ∀ (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) : IsSoundTest c H bLow bHigh fun (x : ℕ) (x_1 : ℤ) => false

On a curve without points of height at most H, the test that lets no numerator through is sound, for the denominators from bLow ≥ 1 to bHigh ≤ H.

theorem Ratpoints.pointsAtInfinityList_eq_nil_of_forall_not_isPoint {c : List ℤ} {H : ℕ} (hH : 1 ≤ H) (h : ∀ (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) (fl : CheckFlags) : Sieve.pointsAtInfinityList c (degree c) fl = []

On a curve without points of height at most H, the search delivers no point at infinity, whatever the flags.

The run in each shape

structure Ratpoints.Sieve.IsSoundRun (c : List ℤ) (entries : List SieveEntry) (magics : Array ℕ) (cls : Vector NumClass 64) (offsets : Array ℕ) (db : UInt64) (store : RowStore) extends Ratpoints.Sieve.EntriesWF c entries magics store : Prop

What the run of the search needs of its arguments for the curve y ^ 2 = F(x, z) with the coefficient list c: sieve entries fit for the run, with the reciprocals of their moduli in their order and a store of the tables of rows that fits them all (Ratpoints.Sieve.EntriesWF), with the row offsets of the packings of the classes cls for all of them (Ratpoints.Sieve.OffsetsFor), since a correction may move the cut points, classes that pack the words of the 2-adic information (Ratpoints.Sieve.twoAdic), and the word db of the classes that admit a numerator (Ratpoints.Sieve.denBits).

• isSound (e : SieveEntry) : e ∈ entries → SieveEntry.IsSound c e
• isPrimeEntry_of_nf (e : SieveEntry) : e ∈ entries → e.nf = 0 → e.IsPrimeEntry
• magics_eq : magics.toList = List.map (fun (e : SieveEntry) => magic e.p) entries
• hasInverses (e : SieveEntry) : e ∈ entries → e.HasInverses
• fits : store.Fits entries
• offsetsFor : OffsetsFor cls entries offsets

  The classes with a pattern have their row offsets for all the entries.

• packs (b : ℕ) : b < 64 → cls[b]!.Packs (twoAdic c (degree c)).run[b]!

  The classes pack the words of the 2-adic information.

• db_eq : db = denBits (twoAdic c (degree c)).run

  The word of the classes that admit a numerator.

theorem Ratpoints.Sieve.IsSoundRun.getLsbD_db {c : List ℤ} {entries : List SieveEntry} {magics : Array ℕ} {cls : Vector NumClass 64} {offsets : Array ℕ} {db : UInt64} {store : RowStore} (h : IsSoundRun c entries magics cls offsets db store) {j : ℕ} (hj : j < 64) : db.toBitVec.getLsbD j = (cls[j]!.bits != 0)

The bits of the word db of a sound run are those of its classes with a pattern.

The search

theorem Ratpoints.exists_isSoundTest_run_sieveRun {c : List ℤ} {H A bLow bHigh : ℕ} {s : SieveOptions} {P : Params} {entries : List Sieve.SieveEntry} {magics : Array ℕ} {cls : Vector Sieve.NumClass 64} {offsets : Array ℕ} {db : UInt64} {store : Sieve.RowStore} (hrun : Sieve.IsSoundRun c entries magics cls offsets db store) (hdec : Sieve.DecisionWF entries P.sp1 { block := 0, sp2 := P.sp2, sp3 := P.sp3 }) (hH63 : H < 2 ^ 63) (hA : 1 ≤ A) (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) {us1 : Option (List Setup.DenInfo × List ℕ)} (hus1 : (if (degree c % 2 == 1 && (c.getD (degree c) 0).natAbs != 1) = true then (Setup.setupUs1 c (degree c) bHigh).run else none) = us1) {checkDenom useJacobi : Bool} {forb : List Sieve.ForbiddenEntry} {forbVal : List Sieve.ForbiddenVal} (hforb : ∀ e ∈ forb, Sieve.IsForbiddenEntry c (degree c) bHigh e) (hval : ∀ e ∈ forbVal, Sieve.IsForbiddenVal c (degree c) bHigh e) (hcd : checkDenom = true → degree c % 2 = 0) {dom : List (Double × Double)} (hdom : IntervalsWF (domainBits dom)) {shape : Sieve.Shape} {iv : Array Sieve.IntervalBounds} (hsetup : (Sieve.runSetup (degree c % 2 == 1 && (c.getD (degree c) 0).natAbs == 1) us1 checkDenom useJacobi forb forbVal (c.getD (degree c) 0) H bHigh dom).run = (shape, iv)) : ∃ (S : ℕ → ℤ → Bool), IsSoundTest c H bLow bHigh S ∧ ∀ {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (fl : CheckFlags) (r : Delivery σ), r.quit = false → (Sieve.sieveRun process c (degree c) H A fl s P entries magics cls offsets db shape iv bLow bHigh store r).run.1 = Delivery.deliver process r (List.flatMap (fun (b : ℕ) => List.flatMap (Sieve.checkNumWith (BruteForce.scaledCoeffs c (degree c) ↑b) (if degree c % 2 = 1 then ↑b else 1) (↑b) fl) (List.filter (fun (a : ℤ) => decide (InIntervals (domainValues dom) (↑a / ↑b)) && S b a) (BruteForce.numerators H))) (searchDens c (degree c) bLow bHigh))

The run of the shape that Ratpoints.Sieve.runSetup chooses, with sound arguments (Ratpoints.Sieve.IsSoundRun), a well-formed first decision (Ratpoints.Sieve.DecisionWF), pieces of at least one bit array, the height below 2 ^ 63, the denominators from bLow ≥ 1 to bHigh ≤ H and well-formed search intervals dom, delivers, with any callback, flags of the check and delivery whose flag is clear, the points of the check with the flags of the numerators in the search intervals that pass a test of the sieve over the denominators of the search (Ratpoints.Sieve.exists_run_sieveRun_eq_deliver, Ratpoints.Sieve.rangesFor_run_exactBounds, Ratpoints.Sieve.inRanges_numeratorRanges); the test, which depends neither on the callback nor on the flags, but on the search intervals, which the decisions of the blocks read (Ratpoints.Sieve.blockDecision), is sound (Ratpoints.IsSoundTest): the shape lets every denominator of a point through, and the class words and the sound entries of every block every numerator of a point (Ratpoints.Sieve.classBit_and_survives_of_ne_nil).

theorem Ratpoints.exists_isSoundTest_run_searchPoints {c : List ℤ} {H : ℕ} (s : SieveOptions) (mayExtend : Bool) (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {bLow bHigh : ℕ} (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) {dom : List (Double × Double)} (hdom : IntervalsWF (domainBits dom)) (sturmEmpty : Bool) : ∃ (S : ℕ → ℤ → Bool), IsSoundTest c H bLow bHigh S ∧ ∀ {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (fl : CheckFlags) (r : Delivery σ), r.quit = false → ((searchPoints process c (degree c) H s.normalize mayExtend fl bLow bHigh dom sturmEmpty (fun (x : String) (s : σ) => s) r).run.info, (searchPoints process c (degree c) H s.normalize mayExtend fl bLow bHigh dom sturmEmpty (fun (x : String) (s : σ) => s) r).run.total) = ((Delivery.deliver process r (searchList c H bLow bHigh (if sturmEmpty = true then [] else domainValues dom) S fl)).info, (Delivery.deliver process r (searchList c H bLow bHigh (if sturmEmpty = true then [] else domainValues dom) S fl)).total)

For options of the sieve as the search normalizes them, 1 ≤ H < 2 ^ 63, the denominators from bLow ≥ 1 to the largest denominator bHigh ≤ H and well-formed search intervals dom, there is a sound test of the numerators (Ratpoints.IsSoundTest) for which the search of the polynomial with the coefficient list c, of its degree, with any callback, flags of the check and delivery whose flag is clear and the print channel that prints nothing, gives the data and the count of the delivery of the points of Ratpoints.searchList for the values of dom, or for no interval when the Sturm step has left none (sturmEmpty): the test is that of the sieve with the moduli that the choice gives each block (Ratpoints.sievingInfo_spec, Ratpoints.exists_isSoundTest_run_sieveRun), which depends neither on the callback nor on the flags, but on the search intervals, which the estimate of the run reads, and with it the choice and the decisions of the correction, the points at infinity come first (Ratpoints.Sieve.pointsAtInfinity_eq_deliver), and the search returns after them when the callback has stopped it or the Sturm step has left no interval (Ratpoints.searchList_nil); when the search takes the 2-adic exit or an exit of the choice of the moduli, the curve has no points (Ratpoints.Sieve.not_isPoint_of_denBits_eq_zero, Ratpoints.sievingInfo_spec), so that the test that lets no numerator through is sound and there is no point at infinity.

The protocol of the search

theorem Ratpoints.run_searchPoints_eq_deliver {c : List ℤ} {H : ℕ} (s : SieveOptions) (mayExtend : Bool) (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {bLow bHigh : ℕ} (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) {dom : List (Double × Double)} (hdom : IntervalsWF (domainBits dom)) (sturmEmpty : Bool) {σ : Type} (process : ℤ → ℤ → ℤ → σ → Answer σ) (fl : CheckFlags) {r : Delivery σ} (hr : r.quit = false) : ((searchPoints process c (degree c) H s.normalize mayExtend fl bLow bHigh dom sturmEmpty (fun (x : String) (s : σ) => s) r).run.info, (searchPoints process c (degree c) H s.normalize mayExtend fl bLow bHigh dom sturmEmpty (fun (x : String) (s : σ) => s) r).run.total) = have r' := Delivery.deliver process r (searchPoints appendPoint c (degree c) H s.normalize mayExtend fl bLow bHigh dom sturmEmpty (fun (x : String) (s : Array (ℤ × ℤ × ℤ)) => s) { info := #[], total := 0, quit := false }).run.info.toList; (r'.info, r'.total)

For options of the sieve as the search normalizes them, 1 ≤ H < 2 ^ 63, the denominators from bLow ≥ 1 to bHigh ≤ H and well-formed search intervals, the search of the polynomial with the coefficient list c, of its degree, with a callback, flags of the check, the print channel that prints nothing and a delivery whose flag is clear, gives the data and the count of the delivery (Ratpoints.Delivery.deliver) of the list of the points that the search with the appending callback (Ratpoints.appendPoint) gives for the same flags from the empty array: both deliver the points of Ratpoints.searchList for the test of the sieve (Ratpoints.exists_isSoundTest_run_searchPoints).

theorem Ratpoints.exists_isSoundTest_run_searchPoints_appendPoint {c : List ℤ} {H : ℕ} (s : SieveOptions) (mayExtend : Bool) (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) {bLow bHigh : ℕ} (hbLow : 1 ≤ bLow) (hbH : bHigh ≤ H) {dom : List (Double × Double)} (hdom : IntervalsWF (domainBits dom)) (sturmEmpty : Bool) : ∃ (S : ℕ → ℤ → Bool), IsSoundTest c H bLow bHigh S ∧ ∀ (fl : CheckFlags), (searchPoints appendPoint c (degree c) H s.normalize mayExtend fl bLow bHigh dom sturmEmpty (fun (x : String) (s : Array (ℤ × ℤ × ℤ)) => s) { info := #[], total := 0, quit := false }).run.info.toList = searchList c H bLow bHigh (if sturmEmpty = true then [] else domainValues dom) S fl

For options of the sieve as the search normalizes them, 1 ≤ H < 2 ^ 63, the denominators from bLow ≥ 1 to bHigh ≤ H and well-formed search intervals dom, the search with the appending callback gives the list of Ratpoints.searchList for the values of dom, or for no interval when the Sturm step has left none (sturmEmpty), and a sound test of the sieve, for every choice of the flags (Ratpoints.exists_isSoundTest_run_searchPoints).