The moduli of the choice

The candidates of the composite moduli that the choice offers (Ratpoints.addModuli) factor over the primes looked at into factors whose tables the choice holds, with codes that Ratpoints.makeModulus can read (Ratpoints.IsFactorCode), and the sieve entries that it makes of them are sound, each at its position (Ratpoints.IsChoiceEntry); the candidates of the primes have the sieve entries of their primes (Ratpoints.ModulusCandidate.IsPrime). After the stages, every candidate has its sieve entry (Ratpoints.ChoicePoolWF), the third stage keeping it so and exiting only at a prime modulo which the curve has no points (Ratpoints.thirdStage_spec).

Main definitions

• Ratpoints.IsExaminedPrimeSe, Ratpoints.Sieve.Power.IsExamined: the tables of the primes and the records of the prime powers as the choice examines them.
• Ratpoints.factorOfCode, Ratpoints.IsFactorCode: the factor of a code of a composite modulus.
• Ratpoints.ModulusCandidate.IsPrime, Ratpoints.ModulusCandidate.IsComposite, Ratpoints.ModulusCandidate.IsPrimeOrComposite: the candidates before the stages.
• Ratpoints.PowerTable.WF, Ratpoints.FacState.WF: the state of Ratpoints.addModuli.
• Ratpoints.IsChoiceEntry: a sieve entry that the choice makes at a position.
• Ratpoints.ChoicePoolWF, Ratpoints.ThirdState.WF: the pool after the stages.

Main statements

• Ratpoints.factorCandidate_spec, Ratpoints.offerModulus_spec, Ratpoints.addModuli_spec: the composite moduli offered.
• Ratpoints.isFactorCode_of_getD_eq_some, Ratpoints.isFactorCode_add_of_getElem?_eq_some: the codes of the primes and of the prime powers can be read.
• Ratpoints.isChoiceEntry_primeEntry, Ratpoints.makeModulus_spec: the sieve entries.
• Ratpoints.stageEntries_spec, Ratpoints.thirdStage_spec: the pool after the stages.

The codes of the factors

def Ratpoints.factorOfCode (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) (code : ℕ) : Sieve.Factor

The factor of the code code of a composite modulus, as Ratpoints.makeModulus reads it: a code below Ratpoints.numPrimes the table of the prime at that position from the loop of the tables (primeSe), another the record of the prime power of its index (pws).

Equations

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

def Ratpoints.IsExaminedPrimeSe (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) : Prop

The tables and densities of the loop of the tables (primeSe) for the curve with the coefficient list c: each table that it holds is that of Ratpoints.Sieve.examinePrime for the prime of the table at its position, one of the first Ratpoints.numPrimes.

Equations

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

def Ratpoints.Sieve.Power.IsExamined (c : List ℤ) (pw : Power) : Prop

The record of a prime power as Ratpoints.addModuli examines it: the tables of Ratpoints.Sieve.examinePower of a prime of the table, one of the first Ratpoints.numPrimes, with a positive exponent, for either path of the reduction and either value of the flag pinf.

Equations

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

structure Ratpoints.IsFactorCode (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) (code : ℕ) : Prop

A code of a factor of a composite modulus that Ratpoints.makeModulus can read: a code below Ratpoints.numPrimes of a prime whose table the loop of the tables holds, another the index of a record of the prime powers.

• prime : code < numPrimes → ∃ (r : Float), primeSe.getD code none = some (Sieve.examinePrime c (degree c) primeTable[code]!, r)

  A code of a prime has its table.

• power : numPrimes ≤ code → ∃ (pw : Sieve.Power), pws[code - numPrimes]? = some pw ∧ Sieve.Power.IsExamined c pw

  Another code has its record.

theorem Ratpoints.IsFactorCode.isSound {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {code : ℕ} (h : IsFactorCode c primeSe pws code) {m : ℕ} (hm0 : 0 < m) (hm : m < maxPrimeEven) (hd : (factorOfCode primeSe pws code).modulus ∣ m) : Sieve.Factor.IsSound c m (factorOfCode primeSe pws code)

The factor of a code that Ratpoints.makeModulus can read is sound for every modulus 0 < m < maxPrimeEven that its modulus divides.

theorem Ratpoints.IsFactorCode.extend {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws pws' : Array Sieve.Power} {code : ℕ} (h : IsFactorCode c primeSe pws code) (hx : pws.Extends pws') : IsFactorCode c primeSe pws' code

A code that Ratpoints.makeModulus can read stays so when the records of the prime powers are extended.

theorem Ratpoints.IsFactorCode.factorOfCode_extend {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws pws' : Array Sieve.Power} {code : ℕ} (h : IsFactorCode c primeSe pws code) (hx : pws.Extends pws') : factorOfCode primeSe pws' code = factorOfCode primeSe pws code

The factor of a code that Ratpoints.makeModulus can read stays the same when the records of the prime powers are extended.

The candidates

structure Ratpoints.ModulusCandidate.IsPrime (c : List ℤ) (e : ModulusCandidate) : Prop

The candidate of a prime as the loop of the tables and the third stage make it for the curve with the coefficient list c (Ratpoints.ModulusCandidate.ofPrime): no factors counted or the count -1, a prime of the table, one of the first Ratpoints.numPrimes, with its sieve entry (Ratpoints.primeEntry) of the table of Ratpoints.Sieve.examinePrime.

• nf_le : e.nf ≤ 0

  No factors counted, or the count -1.

• exists_eq : ∃ pn < numPrimes, ∃ (r : Float), e.p = primeTable[pn]! ∧ e.ssp = some (primeEntry (Sieve.examinePrime c (degree c) primeTable[pn]!) r)

  A prime of the table with its sieve entry.

structure Ratpoints.ModulusCandidate.IsComposite (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) (e : ModulusCandidate) : Prop

The candidate of a composite modulus as Ratpoints.addModuli offers it for the curve with the coefficient list c, the tables of the loop of the tables primeSe and the records of the prime powers pws: the count of its factors, with codes that Ratpoints.makeModulus can read and whose moduli multiply to the modulus, odd, between 1 and Ratpoints.maxPrimeEven, and no sieve entry yet.

• nf_eq : e.nf = ↑e.fac.length

  The count of the factors.

• fac_ne_nil : e.fac ≠ []

  At least one factor.

• ssp_eq : e.ssp = none

  No sieve entry yet.

• one_lt : 1 < e.p

  The modulus is above 1.

• lt_maxPrimeEven : e.p < maxPrimeEven

  The modulus is below Ratpoints.maxPrimeEven.

• odd : e.p % 2 = 1

  The modulus is odd.

• isFactorCode (code : ℕ) : code ∈ e.fac → IsFactorCode c primeSe pws code

  The codes can be read.

• prod_eq : (List.map (fun (code : ℕ) => (factorOfCode primeSe pws code).modulus) e.fac).prod = e.p

  The moduli of the factors multiply to the modulus.

theorem Ratpoints.ModulusCandidate.IsComposite.extend {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws pws' : Array Sieve.Power} {e : ModulusCandidate} (h : IsComposite c primeSe pws e) (hx : pws.Extends pws') : IsComposite c primeSe pws' e

def Ratpoints.ModulusCandidate.IsPrimeOrComposite (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) (e : ModulusCandidate) : Prop

A candidate of the pool before the stages: a prime (Ratpoints.ModulusCandidate.IsPrime) or a composite modulus (Ratpoints.ModulusCandidate.IsComposite).

Equations

• Ratpoints.ModulusCandidate.IsPrimeOrComposite c primeSe pws e = (Ratpoints.ModulusCandidate.IsPrime c e ∨ Ratpoints.ModulusCandidate.IsComposite c primeSe pws e)

theorem Ratpoints.ModulusCandidate.IsPrimeOrComposite.extend {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws pws' : Array Sieve.Power} {e : ModulusCandidate} (h : IsPrimeOrComposite c primeSe pws e) (hx : pws.Extends pws') : IsPrimeOrComposite c primeSe pws' e

theorem Ratpoints.ModulusCandidate.IsPrimeOrComposite.of_eq {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {e e' : ModulusCandidate} (h : IsPrimeOrComposite c primeSe pws e) (hnf : e'.nf = e.nf) (hp : e'.p = e.p) (hs : e'.ssp = e.ssp) (hf : e'.fac = e.fac) : IsPrimeOrComposite c primeSe pws e'

A candidate with the count of factors, the modulus, the sieve entry and the codes of a candidate is a candidate: the predicate reads neither the density, the key, the cost nor the mask.

theorem Ratpoints.ModulusCandidate.IsPrimeOrComposite.phase1Key {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {e : ModulusCandidate} (h : IsPrimeOrComposite c primeSe pws e) (ct U D cc : Float) : IsPrimeOrComposite c primeSe pws (Ratpoints.phase1Key ct U D cc e)

A candidate keyed for the first stage is a candidate.

The prime powers

structure Ratpoints.PowerTable.WF (c : List ℤ) (tab : PowerTable) : Prop

The prime powers examined so far by Ratpoints.addModuli for the curve with the coefficient list c: each record that the table holds is that of a prime power of the table, and each index that it holds for a prime power p ^ e, p at the position pn, is that of a record of the tables of Ratpoints.Sieve.examinePower for it.

• isExamined (pw : Sieve.Power) : pw ∈ tab.pws → Sieve.Power.IsExamined c pw

  Each record is that of a prime power of the table.

• idx (pn e i : ℕ) : List.lookup (pn, e) tab.idx = some (some i) → ∃ (pw : Sieve.Power), tab.pws[i]? = some pw ∧ ∃ (u : Bool) (pinf : Bool), pw = (Sieve.examinePower c (degree c) primeTable[pn]! e u pinf).run

  Each index is that of the record of its prime power.

theorem Ratpoints.PowerTable.WF.push {c : List ℤ} {tab : PowerTable} (h : WF c tab) {pn e : ℕ} (hpn : pn < numPrimes) (he : 1 ≤ e) (u pinf b : Bool) : WF c { pws := if b = true then tab.pws.push (Sieve.examinePower c (degree c) primeTable[pn]! e u pinf).run else tab.pws, idx := ((pn, e), if b = true then some tab.pws.size else none) :: tab.idx }

theorem Ratpoints.powerIndex_spec (c : List ℤ) (u pinf : Bool) (pn p e : ℕ) (tab : PowerTable) : ⦃ PowerTable.WF c tab ∧ pn < numPrimes ∧ 1 ≤ e ∧ p = primeTable[pn]! ⦄ powerIndex c (degree c) u pinf pn p e tab ⦃ fun (r : Option ℕ × PowerTable) => PowerTable.WF c r.2 ∧ tab.pws.Extends r.2.pws ∧ ∀ (i : ℕ), r.1 = some i → ∃ (pw : Sieve.Power), r.2.pws[i]? = some pw ∧ ∃ (u : Bool) (pinf : Bool), pw = (Sieve.examinePower c (degree c) primeTable[pn]! e u pinf).run ⦄

The contract of Ratpoints.powerIndex for the prime power p ^ e, e ≥ 1, of the prime p = primeTable[pn], one of the first Ratpoints.numPrimes: the prime powers examined stay those of the table (Ratpoints.PowerTable.WF), the records extended, and the index it returns is that of a record of the tables of Ratpoints.Sieve.examinePower for p ^ e.

theorem Ratpoints.isFactorCode_of_getD_eq_some {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} (hse : IsExaminedPrimeSe c primeSe) (pws : Array Sieve.Power) {k : ℕ} {t : Sieve.Entry} {r : Float} (h : primeSe.getD k none = some (t, r)) : IsFactorCode c primeSe pws k

The code of a prime whose table the loop of the tables holds can be read.

theorem Ratpoints.modulus_factorOfCode_of_getD_eq_some {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} (hse : IsExaminedPrimeSe c primeSe) (pws : Array Sieve.Power) {k : ℕ} {t : Sieve.Entry} {r : Float} (h : primeSe.getD k none = some (t, r)) : (factorOfCode primeSe pws k).modulus = primeTable[k]!

The factor of the code of a prime whose table the loop of the tables holds has the prime as its modulus.

theorem Ratpoints.isFactorCode_add_of_getElem?_eq_some {c : List ℤ} (primeSe : Array (Option (Sieve.Entry × Float))) {pws : Array Sieve.Power} {i pn e : ℕ} {pw : Sieve.Power} (hpn : pn < numPrimes) (he : 1 ≤ e) (h : pws[i]? = some pw) {u pinf : Bool} (hpw : pw = (Sieve.examinePower c (degree c) primeTable[pn]! e u pinf).run) : IsFactorCode c primeSe pws (numPrimes + i)

The code numPrimes + i of the record i of the tables of a prime power of the table can be read.

theorem Ratpoints.modulus_factorOfCode_add_of_getElem?_eq_some {c : List ℤ} (primeSe : Array (Option (Sieve.Entry × Float))) {pws : Array Sieve.Power} {i pn e : ℕ} {pw : Sieve.Power} (h : pws[i]? = some pw) {u pinf : Bool} (hpw : pw = (Sieve.examinePower c (degree c) primeTable[pn]! e u pinf).run) : (factorOfCode primeSe pws (numPrimes + i)).modulus = primeTable[pn]! ^ e

The factor of the code numPrimes + i of the record i of the tables of a prime power p ^ e of the table has the modulus p ^ e.

theorem Ratpoints.takeFactor_spec (c : List ℤ) (u : Bool) (primeSe : Array (Option (Sieve.Entry × Float))) (pinf : Array Bool) (p e : ℕ) (st : FacState) : ⦃ IsExaminedPrimeSe c primeSe ∧ PowerTable.WF c st.tab ∧ st.pn < numPrimes ∧ 1 ≤ e ∧ p = primeTable[st.pn]! ⦄ takeFactor c (degree c) u primeSe pinf p e st ⦃ fun (st' : FacState) => PowerTable.WF c st'.tab ∧ st.tab.pws.Extends st'.tab.pws ∧ st'.rest = st.rest ∧ (st'.ok = true → st'.pn = st.pn + 1 ∧ ∃ (code : ℕ), st'.fac = st.fac.push code ∧ IsFactorCode c primeSe st'.tab.pws code ∧ (factorOfCode primeSe st'.tab.pws code).modulus = p ^ e) ∧ st.pn ≤ st'.pn ⦄

The contract of Ratpoints.takeFactor for the factor p ^ e, e ≥ 1, of the prime p = primeTable[st.pn], one of the first Ratpoints.numPrimes: the prime powers examined stay those of the table, the records extended, the cofactor kept and the position not lowered, and while the candidate is possible the code of the factor is appended, one that Ratpoints.makeModulus can read (Ratpoints.IsFactorCode), with the modulus p ^ e.

structure Ratpoints.FacState.WF (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) (m : ℕ) (st : FacState) : Prop

The state st of the factorization of the candidate m (Ratpoints.FacState) for the curve with the coefficient list c and the tables of the loop of the tables primeSe: the prime powers examined are those of the table (Ratpoints.PowerTable.WF), and while the candidate is possible the cofactor is positive and times the moduli of the factors taken, whose codes Ratpoints.makeModulus can read, makes m.

• tab : PowerTable.WF c st.tab

  The prime powers examined are those of the table.

• rest_pos : st.ok = true → 0 < st.rest

  The cofactor is positive.

• isFactorCode : st.ok = true → ∀ code ∈ st.fac, IsFactorCode c primeSe st.tab.pws code

  The codes of the factors can be read.

• mul_prod : st.ok = true → st.rest * (List.map (fun (code : ℕ) => (factorOfCode primeSe st.tab.pws code).modulus) st.fac.toList).prod = m

  The cofactor times the moduli of the factors makes m.

theorem Ratpoints.FacState.WF.of_eq {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {m : ℕ} {b st : FacState} (h : WF c primeSe m b) (hr : st.rest = b.rest) (hok : st.ok = b.ok) (hf : st.fac = b.fac) (ht : st.tab = b.tab) : WF c primeSe m st

A state of the factorization with the cofactor, the flag, the codes and the table of the prime powers of one of m is one of m: the predicate reads neither the position of the next prime, the product of the densities nor the mask.

theorem Ratpoints.FacState.WF.of_ok_eq_false {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {m : ℕ} {st : FacState} (ht : PowerTable.WF c st.tab) (hok : st.ok = false) : WF c primeSe m st

A state of the factorization whose candidate is refused is one of every m.

theorem Ratpoints.FacState.WF.of_takeFactor {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {m : ℕ} {b st : FacState} (hb : WF c primeSe m b) (hok : b.ok = true) {rest q : ℕ} (hrest : 0 < rest) (hR : rest * q = b.rest) (ht : PowerTable.WF c st.tab) (hx : b.tab.pws.Extends st.tab.pws) (hr : st.rest = rest) (hs : st.ok = true → ∃ (code : ℕ), st.fac = b.fac.push code ∧ IsFactorCode c primeSe st.tab.pws code ∧ (factorOfCode primeSe st.tab.pws code).modulus = q) : WF c primeSe m st

The state of the factorization after the factor p ^ e of the cofactor b.rest = rest p ^ e is taken (Ratpoints.takeFactor), from one of m whose candidate is still possible: one of m.

def Ratpoints.FactorLoopInvariant (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) (m : ℕ) (st₀ : FacState) : Std.WP.WhileInvariant (Option FacState × FacState) Prop

The invariant of the loop of Ratpoints.factorCandidate over the primes, whose state is the value of a return and the state of the factorization, from the state st₀: both are states of the factorization of m (Ratpoints.FacState.WF) with the records of the prime powers of st₀ extended.

Equations

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

def Ratpoints.DivideInvariant (R p : ℕ) : Std.WP.WhileInvariant (ℕ × ℕ) Prop

The invariant of the loop of Ratpoints.factorCandidate that divides the prime p off the cofactor R, on the cofactor left and the exponent: the cofactor left is positive and times p ^ e makes R, it is R before the first division, and p does not divide it at the end.

Equations

• Ratpoints.DivideInvariant R p = Std.WP.WhileInvariant.mk fun (exit : Bool) (s : ℕ × ℕ) => 0 < s.1 ∧ s.1 * p ^ s.2 = R ∧ (s.2 = 0 → s.1 = R) ∧ (exit = true → s.1 % p ≠ 0)

theorem Ratpoints.factorCandidate_spec (c : List ℤ) (u : Bool) (primeSe : Array (Option (Sieve.Entry × Float))) (pinf : Array Bool) (pnLim m : ℕ) (st : FacState) : ⦃ IsExaminedPrimeSe c primeSe ∧ pnLim ≤ numPrimes ∧ FacState.WF c primeSe m st ⦄ factorCandidate c (degree c) u primeSe pinf pnLim st ⦃ fun (st' : FacState) => FacState.WF c primeSe m st' ∧ st.tab.pws.Extends st'.tab.pws ⦄

The contract of Ratpoints.factorCandidate over the first pnLim ≤ numPrimes primes: the state of the factorization of m stays one (Ratpoints.FacState.WF), with the records of the prime powers extended. The loop ends, since the position of the next prime rises or the candidate is refused, and the inner loops, since the position rises and the cofactor drops.

theorem Ratpoints.FacState.WF.isComposite {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {m : ℕ} {st : FacState} (h : WF c primeSe m st) (hok : st.ok = true) (hr : ¬1 < st.rest) (hm : 1 < m ∧ m < maxPrimeEven ∧ m % 2 = 1) {e : ModulusCandidate} (hnf : e.nf = ↑st.fac.size) (hf : e.fac = st.fac.toList) (hs : e.ssp = none) (hp : e.p = m) : ModulusCandidate.IsComposite c primeSe st.tab.pws e

The candidate of a composite modulus 1 < m < maxPrimeEven, odd, from a state of its factorization that ends with the candidate possible and the cofactor 1: the codes of its factors, whose moduli multiply to m.

theorem Ratpoints.offerModulus_spec (c : List ℤ) (u : Bool) (primeSe : Array (Option (Sieve.Entry × Float))) (pinf : Array Bool) (pnLim : ℕ) (ct U D : Float) (m : ℕ) (tab : PowerTable) : ⦃ IsExaminedPrimeSe c primeSe ∧ pnLim ≤ numPrimes ∧ PowerTable.WF c tab ∧ 1 < m ∧ m < maxPrimeEven ∧ m % 2 = 1 ⦄ offerModulus c (degree c) u primeSe pinf pnLim ct U D m tab ⦃ fun (r : Option ModulusCandidate × PowerTable) => PowerTable.WF c r.2 ∧ tab.pws.Extends r.2.pws ∧ ∀ (e : ModulusCandidate), r.1 = some e → ModulusCandidate.IsComposite c primeSe r.2.pws e ⦄

The contract of Ratpoints.offerModulus for an odd 1 < m < maxPrimeEven: the prime powers examined stay those of the table, the records extended, and the candidate it offers is a composite modulus whose codes Ratpoints.makeModulus can read and whose factors multiply to m (Ratpoints.ModulusCandidate.IsComposite).

theorem Ratpoints.PowerTable.wf_empty (c : List ℤ) : WF c { }

def Ratpoints.AddModuliInvariant (c : List ℤ) (primeSe : Array (Option (Sieve.Entry × Float))) : Std.WP.WhileInvariant (Array ModulusCandidate × PowerTable × ℕ) Prop

The invariant of the loop of Ratpoints.addModuli over the candidates m: the candidates of the pool (Ratpoints.ModulusCandidate.IsPrimeOrComposite) for the records of the prime powers examined so far, which are those of the table, and m odd from 9 on.

Equations

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

theorem Ratpoints.addModuli_spec (c : List ℤ) (u : Bool) (pool : Array ModulusCandidate) (primeSe : Array (Option (Sieve.Entry × Float))) (pinf : Array Bool) (pnLim : ℕ) (ct cc U D : Float) : ⦃ IsExaminedPrimeSe c primeSe ∧ pnLim ≤ numPrimes ∧ ∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe #[] e ⦄ addModuli c (degree c) u pool primeSe pinf pnLim ct cc U D ⦃ fun (r : Array ModulusCandidate × Array Sieve.Power) => ∀ e ∈ r.1, ModulusCandidate.IsPrimeOrComposite c primeSe r.2 e ⦄

The contract of Ratpoints.addModuli, for any values of the doubles: from a pool of candidates of the primes, it returns a pool of candidates of primes and composite moduli (Ratpoints.ModulusCandidate.IsPrimeOrComposite) for the records of the prime powers that it returns.

The sieve entries

structure Ratpoints.IsChoiceEntry (c : List ℤ) (n : ℕ) (se : Sieve.SieveEntry) : Prop

A sieve entry that the choice of the moduli makes for the curve with the coefficient list c, at the position n of the entries: an entry of its modulus (Ratpoints.IsModulusEntry), with the reference and the kind of builder of its position (Ratpoints.Sieve.SieveEntry.refInit), and a prime entry of the table (Ratpoints.Sieve.SieveEntry.IsPrimeEntry) when it counts no factors.

• isModulusEntry : IsModulusEntry c se.p se

  An entry of its modulus.

• refInit : (se.ref, se.init) = Sieve.SieveEntry.refInit n se.factors

  The reference and the kind of builder of its position.

• isPrimeEntry : se.nf = 0 → se.IsPrimeEntry

  A prime entry when it counts no factors.

theorem Ratpoints.isChoiceEntry_primeEntry (c : List ℤ) {pn : ℕ} (hpn : pn < numPrimes) (r : Float) (n : ℕ) : IsChoiceEntry c n (primeEntry (Sieve.examinePrime c (degree c) primeTable[pn]!) r)

The sieve entry of a prime of the table (Ratpoints.primeEntry), one of the first Ratpoints.numPrimes, with its table, is one that the choice makes, at every position.

theorem Ratpoints.ModulusCandidate.IsComposite.isSound {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {e : ModulusCandidate} (h : IsComposite c primeSe pws e) (f : Sieve.Factor) : f ∈ List.map (factorOfCode primeSe pws) e.fac → Sieve.Factor.IsSound c e.p f

The factors of a composite candidate whose codes can be read are sound for its modulus.

theorem Ratpoints.makeModulus_spec (c : List ℤ) (e : ModulusCandidate) (n : ℕ) (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) : ⦃ ModulusCandidate.IsComposite c primeSe pws e ⦄ makeModulus e n primeSe pws ⦃ fun (se : Sieve.SieveEntry) => IsChoiceEntry c n se ⦄

The contract of Ratpoints.makeModulus: the sieve entry of a composite candidate whose codes can be read is one that the choice makes at the position n (Ratpoints.IsChoiceEntry).

structure Ratpoints.ChoicePoolWF (c : List ℤ) (sp2 : ℕ) (pool : Array ModulusCandidate) : Prop

The candidates of the pool pool after the stages, whose second ends at sp2: those of the first two stages each with its sieve entry, made for its position (Ratpoints.IsChoiceEntry), and those from sp2 on primes (Ratpoints.ModulusCandidate.IsPrime).

• exists_isChoiceEntry_of_lt (n : ℕ) (h : n < pool.size) : n < sp2 → ∃ (se : Sieve.SieveEntry), pool[n].ssp = some se ∧ IsChoiceEntry c n se

  The candidates of the first two stages have their sieve entries.

• isPrime (n : ℕ) (h : n < pool.size) : sp2 ≤ n → ModulusCandidate.IsPrime c pool[n]

  The candidates from sp2 on are primes.

structure Ratpoints.StageEntriesInvariant (c : List ℤ) (pool₀ : Array ModulusCandidate) (k : ℕ) (pool : Array ModulusCandidate) : Prop

The invariant of the loop of Ratpoints.stageEntries after the positions below k, from the pool pool₀: the size kept, the candidates below k with their sieve entries made for their positions, and the others as they were.

• size_eq : pool.size = pool₀.size

  The size is kept.

• exists_isChoiceEntry_of_lt (n : ℕ) (h : n < pool.size) : n < k → ∃ (se : Sieve.SieveEntry), pool[n].ssp = some se ∧ IsChoiceEntry c n se

  The candidates below k have their sieve entries, made for their positions.

• getElem!_eq (n : ℕ) : n < pool.size → k ≤ n → pool[n]! = pool₀[n]!

  The other candidates are as they were.

theorem Ratpoints.ModulusCandidate.IsPrimeOrComposite.isPrime_of_not_ssp_isNone {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {e : ModulusCandidate} (h : IsPrimeOrComposite c primeSe pws e) (hs : ¬e.ssp.isNone = true) : IsPrime c e

theorem Ratpoints.ModulusCandidate.IsPrimeOrComposite.isComposite_of_ssp_isNone {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {e : ModulusCandidate} (h : IsPrimeOrComposite c primeSe pws e) (hs : e.ssp.isNone = true) : IsComposite c primeSe pws e

theorem Ratpoints.ModulusCandidate.IsPrime.exists_isChoiceEntry {c : List ℤ} {e : ModulusCandidate} (h : IsPrime c e) (n : ℕ) : ∃ (se : Sieve.SieveEntry), e.ssp = some se ∧ IsChoiceEntry c n se

A prime candidate has the sieve entry of its prime, which the choice makes, at every position.

theorem Ratpoints.stageEntriesInvariant_zero (c : List ℤ) (pool : Array ModulusCandidate) : StageEntriesInvariant c pool [].length pool

theorem Ratpoints.StageEntriesInvariant.isComposite {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {pool p : Array ModulusCandidate} {sp2 : ℕ} (hpre : (∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) ∧ NfEqZeroFrom pool sp2 ∧ sp2 ≤ pool.size) {pref suff : List ℕ} {cur : ℕ} (hl : ForIn.toList [:sp2] = pref ++ cur :: suff) (h : StageEntriesInvariant c pool pref.length p) (hn : p[cur]!.ssp.isNone = true) : ModulusCandidate.IsComposite c primeSe pws p[cur]!

theorem Ratpoints.StageEntriesInvariant.set {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {pool p : Array ModulusCandidate} {sp2 : ℕ} (hpre : (∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) ∧ NfEqZeroFrom pool sp2 ∧ sp2 ≤ pool.size) {pref suff : List ℕ} {cur : ℕ} (hl : ForIn.toList [:sp2] = pref ++ cur :: suff) (h : StageEntriesInvariant c pool pref.length p) {se : Sieve.SieveEntry} (hse : IsChoiceEntry c cur se) : StageEntriesInvariant c pool (pref ++ [cur]).length (p.set! cur (have __src := p[cur]!; { r := __src.r, key := __src.key, cost := __src.cost, p := __src.p, mask := __src.mask, ssp := some se, nf := __src.nf, fac := __src.fac }))

theorem Ratpoints.StageEntriesInvariant.skip {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {pool p : Array ModulusCandidate} {sp2 : ℕ} (hpre : (∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) ∧ NfEqZeroFrom pool sp2 ∧ sp2 ≤ pool.size) {pref suff : List ℕ} {cur : ℕ} (hl : ForIn.toList [:sp2] = pref ++ cur :: suff) (h : StageEntriesInvariant c pool pref.length p) (hn : ¬p[cur]!.ssp.isNone = true) : StageEntriesInvariant c pool (pref ++ [cur]).length p

theorem Ratpoints.StageEntriesInvariant.post {c : List ℤ} {primeSe : Array (Option (Sieve.Entry × Float))} {pws : Array Sieve.Power} {pool p : Array ModulusCandidate} {sp2 : ℕ} (hpre : (∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) ∧ NfEqZeroFrom pool sp2 ∧ sp2 ≤ pool.size) (h : StageEntriesInvariant c pool (ForIn.toList [:sp2]).length p) : ChoicePoolWF c sp2 p ∧ p.size = pool.size

theorem Ratpoints.stageEntries_spec (c : List ℤ) (pool : Array ModulusCandidate) (sp2 : ℕ) (primeSe : Array (Option (Sieve.Entry × Float))) (pws : Array Sieve.Power) : ⦃ (∀ e ∈ pool, ModulusCandidate.IsPrimeOrComposite c primeSe pws e) ∧ NfEqZeroFrom pool sp2 ∧ sp2 ≤ pool.size ⦄ stageEntries pool sp2 primeSe pws ⦃ fun (r : Array ModulusCandidate) => ChoicePoolWF c sp2 r ∧ r.size = pool.size ⦄

The contract of Ratpoints.stageEntries: after the stages, which leave composite moduli only before sp2, every candidate before sp2 has its sieve entry, made for its position, and those from sp2 on are primes (Ratpoints.ChoicePoolWF).

theorem Ratpoints.ChoicePoolWF.push {c : List ℤ} {sp2 : ℕ} {pool : Array ModulusCandidate} (h : ChoicePoolWF c sp2 pool) (hs : sp2 ≤ pool.size) {e : ModulusCandidate} (he : ModulusCandidate.IsPrime c e) : ChoicePoolWF c sp2 (pool.push e)

theorem Ratpoints.ChoicePoolWF.swapIfInBounds {c : List ℤ} {sp2 : ℕ} {pool : Array ModulusCandidate} (h : ChoicePoolWF c sp2 pool) {i j : ℕ} (hi : sp2 ≤ i) (hj : sp2 ≤ j) : ChoicePoolWF c sp2 (pool.swapIfInBounds i j)

theorem Ratpoints.examinePrime?_value (c : List ℤ) (d p : ℕ) (u : Bool) : ⦃ True ⦄ Sieve.examinePrime? c d p u ⦃ fun (r : Option (Sieve.Entry × Array ℕ × ℕ × Float)) => r = (Sieve.examinePrime? c d p u).run ⦄

The result of Ratpoints.Sieve.examinePrime? as its own value, for the contracts of the loops that bind it and read it through its own lemmas.

theorem Ratpoints.isPrime_ofPrime {c : List ℤ} {pn : ℕ} (hpn : pn < numPrimes) {u : Bool} {t : Sieve.Entry} {cm : Array ℕ} {code : ℕ} {r : Float} (h : (Sieve.examinePrime? c (degree c) primeTable[pn]! u).run = some (t, cm, code, r)) (key cost : Float) : ModulusCandidate.IsPrime c (have __src := ModulusCandidate.ofPrime pn t r code; { r := __src.r, key := key, cost := cost, p := __src.p, mask := __src.mask, ssp := __src.ssp, nf := __src.nf, fac := __src.fac })

The candidate of a prime of the table, one of the first Ratpoints.numPrimes, from its examination, which says something, is a prime candidate, whatever its key and cost.

theorem Ratpoints.lookFurther_spec (c : List ℤ) (u : Bool) (st : ThirdState) : ⦃ st.pnLim < numPrimes ⦄ lookFurther c (degree c) u st ⦃ fun (r : Option ThirdState) => (r = none → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (st' : ThirdState), r = some st' → st'.pnLim = st.pnLim + 1 ∧ st'.sp3 = st.sp3 ∧ (st'.pool = st.pool ∨ ∃ (e : ModulusCandidate), ModulusCandidate.IsPrime c e ∧ st'.pool = st.pool.push e) ⦄

The contract of Ratpoints.lookFurther for a position below Ratpoints.numPrimes: at none the curve has no points; otherwise one more prime is looked at, and the pool gains at most the candidate of a prime.

def Ratpoints.ThirdState.WF (c : List ℤ) (sp2 : ℕ) (st : ThirdState) : Prop

The state of the third stage (Ratpoints.ThirdState) after the first two stages, which end at sp2: the pool after the stages (Ratpoints.ChoicePoolWF), the end of the third stage between sp2 and the size of the pool.

Equations

• Ratpoints.ThirdState.WF c sp2 st = (Ratpoints.ChoicePoolWF c sp2 st.pool ∧ sp2 ≤ st.sp3 ∧ st.sp3 ≤ st.pool.size)

def Ratpoints.ThirdStageInvariant (c : List ℤ) (sp2 : ℕ) : Std.WP.WhileInvariant (Option (Except ℕ ThirdState) × ThirdState) Prop

The invariant of the loop of Ratpoints.thirdStage, whose state is the value of a return and the state of the stage: the value of a return is an exit, at which the curve has no points; the state of the stage, from the end sp2 of the first two (Ratpoints.ThirdState.WF).

Equations

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

theorem Ratpoints.thirdStage_spec (c : List ℤ) (u mayExtend : Bool) (sp3Extra : ℤ) (sp3Want : ℕ) (perSurv perDenom : Float) (sp2 : ℕ) (st : ThirdState) : ⦃ ThirdState.WF c sp2 st ⦄ thirdStage c (degree c) u mayExtend sp3Extra sp3Want perSurv perDenom st ⦃ fun (r : Except ℕ ThirdState) => (∀ (p : ℕ), r = Except.error p → ∀ (H : ℕ) (q : ℤ × ℤ × ℤ), ¬IsPoint c H q) ∧ ∀ (t : ThirdState), r = Except.ok t → ThirdState.WF c sp2 t ⦄

The contract of Ratpoints.thirdStage, for any values of the doubles: at an exit the curve has no points; otherwise the pool stays one after the stages (Ratpoints.ThirdState.WF), the end of the third stage within it. The loop ends, since the stage grows or one more prime is looked at.