The Jacobi test by tables

The test by tables (Ratpoints.Sieve.jacobiSetup, Ratpoints.Sieve.jacobiTest) computes the symbol of the binary algorithm, (lcf / b*) for 1 ≤ b ≤ bHigh, where b* is the largest divisor of b prime to 2 lcf: it takes 2 and the odd primes of lcf out of b and reads the symbol off the sign of b* mod 8 and the tables of the non-squares modulo the primes of lcf with an odd exponent, by quadratic reciprocity. The proof has two layers: the contracts describe the loops, the tables of the non-squares giving the Legendre symbol, the set-up the tables of lcf (Ratpoints.Sieve.IsJacobiInfo) and the test the exclusive or of the sign and the entries over the part of b free of 2 and of the primes of the tables; and Ratpoints.Sieve.jacobiSym_eq_ite_foldl reads the Jacobi symbol off the tables. So the test lets the denominator of every point of a curve of even degree through. The set-up gives tables only for bHigh ≤ Ratpoints.mulModLimit, so that the denominators of the test stay below 2 ^ 32, where RP_MULDIV with the reciprocals that the tables hold, those of their primes, is exact (Ratpoints.Sieve.run_jacobiTest).

Main definitions

• Ratpoints.Sieve.IsJacobiInfo: what the tables of the test by tables say of the leading coefficient.

Main statements

• Ratpoints.Sieve.nonSquares_spec, Ratpoints.Sieve.legendreSym_eq_ite_getElem!_nonSquares: the tables of the non-squares give the Legendre symbol; Ratpoints.Sieve.ite_getElem!_jacobiSigns: the signs.
• Ratpoints.Sieve.jacobiSetup_spec, Ratpoints.Sieve.jacobiTest_spec: the contracts of the set-up, whose tables hold primes of Ratpoints.primeTable with their reciprocals, and of the test by tables.
• Ratpoints.Sieve.jacobiSym_eq_ite_foldl: the Jacobi symbol read off the tables.
• Ratpoints.Sieve.run_jacobiTest: the test by tables decides whether (lcf / b*) = 1.
• Ratpoints.Sieve.run_jacobiTest_of_sq_eq: the test by tables passes the denominator of every point of a curve of even degree.

Implementation notes

The contracts are proved with vcgen, with loop invariants that are named definitions, in a file with Mathlib, since they speak of primes, their valuations and the Legendre symbol. A contract that needs the exact value of a component that its loop calls takes a specification ⦃True⦄ x ⦃fun r ↦ r = Id.run x⦄ of it (Ratpoints.Setup.valuation_value for the valuation, a private one for the table of the non-squares), since the registered contract would give only what it says of the value. The test reduces by the reciprocals that the tables hold, which the set-up makes those of their primes, and the reductions are exact (Ratpoints.Sieve.mulDiv_magic), since these are primes of Ratpoints.primeTable, below 1022, and the denominators are at most Ratpoints.mulModLimit < 2 ^ 32 (Ratpoints.mul_lt_two_pow_64_of_le_mulModLimit). The proofs use only that Ratpoints.mulModLimit is below 2 ^ 64 and 2 ^ 32 (Ratpoints.mulModLimit_lt_size, Ratpoints.mulModLimit_lt_two_pow_32, which decide checks next to the constant), never the values of Ratpoints.mulModLimit, Ratpoints.jacobiPrimes and Ratpoints.jacobiTable.

The tables of the non-squares and the signs

def Ratpoints.Sieve.NonSquaresInvariant (q : ℕ) (pref : List ℕ) (st : Array Bool × ℕ) : Prop

The invariant of the loop of Ratpoints.Sieve.nonSquares on q after the steps x ≤ k, k the length of pref: the table has q entries, s = (k + 1) ^ 2 mod q, and an entry r < q is false exactly when r = x ^ 2 mod q for some 1 ≤ x ≤ k.

Equations

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

theorem Ratpoints.Sieve.nonSquaresInvariant_nil {q : ℕ} (hq : q % 2 = 1 ∧ 1 < q) : NonSquaresInvariant q [] (Array.replicate q true, 1)

theorem Ratpoints.Sieve.NonSquaresInvariant.size_eq_and_getElem!_eq_false_iff {q s : ℕ} {ns : Array Bool} (h : NonSquaresInvariant q (ForIn.toList [1:q / 2 + 1]) (ns, s)) : ns.size = q ∧ ∀ r < q, ns[r]! = false ↔ ∃ (x : ℕ), 1 ≤ x ∧ x ≤ q / 2 ∧ x * x % q = r

theorem Ratpoints.Sieve.NonSquaresInvariant.set! {q cur s s' : ℕ} {pref suff : List ℕ} {ns : Array Bool} (hq : q % 2 = 1 ∧ 1 < q) (hl : ForIn.toList [1:q / 2 + 1] = pref ++ cur :: suff) (h : NonSquaresInvariant q pref (ns, s)) (hs : s' = if q ≤ s + 2 * cur + 1 then s + 2 * cur + 1 - q else s + 2 * cur + 1) : NonSquaresInvariant q (pref ++ [cur]) (ns.set! s false, s')

The step x of Ratpoints.Sieve.nonSquares clears the entry of s = x ^ 2 mod q and moves on to (x + 1) ^ 2 mod q = s + 2 x + 1, less q at most once, since 2 x + 1 ≤ q for odd q.

theorem Ratpoints.Sieve.nonSquares_spec (q : ℕ) : ⦃ q % 2 = 1 ∧ 1 < q ⦄ nonSquares q ⦃ fun (ns : Array Bool) => ns.size = q ∧ ∀ r < q, ns[r]! = false ↔ ∃ (x : ℕ), 1 ≤ x ∧ x ≤ q / 2 ∧ x * x % q = r ⦄

The table of the non-squares modulo an odd q > 1 has q entries, an entry r < q being false exactly when r is the square modulo q of one of 1, …, q / 2.

theorem Ratpoints.Sieve.legendreSym_eq_ite_getElem!_nonSquares {q r : ℕ} [hq : Fact (Nat.Prime q)] (hq2 : q ≠ 2) (hr0 : r ≠ 0) (hr : r < q) : legendreSym q ↑r = if (nonSquares q).run[r]! = true then -1 else 1

The table of Ratpoints.Sieve.nonSquares gives the Legendre symbol of a residue r ≠ 0 modulo an odd prime q: its entry is true exactly where the symbol is -1.

theorem Ratpoints.Sieve.ite_getElem!_jacobiSigns {b : ℕ} (hb : b % 2 = 1) (n3 : ℕ) (neg : Bool) (v : ℕ) : (if (jacobiSigns n3 neg v)[b % 8]! = true then -1 else 1) = ZMod.χ₄ ↑b ^ (n3 + if neg = true then 1 else 0) * ZMod.χ₈ ↑b ^ v

The signs of Ratpoints.Sieve.jacobiSigns for odd b: the entry of b mod 8, read as -1 for true, is χ₄(b) ^ (n₃ + neg) χ₈(b) ^ v, the product of the signs of (-1 / b) ^ neg, of the reciprocity of the n₃ primes ≡ 3 (mod 4) and of (2 / b) ^ v.

The set-up of the tables

def Ratpoints.Sieve.IsJacobiInfo (lcf : ℤ) (ji : JacobiInfo) : Prop

What the tables ji of the Jacobi test say of the leading coefficient lcf (Ratpoints.Sieve.jacobiSetup): its primes are odd primes of lcf, each with the table of the non-squares modulo it (Ratpoints.Sieve.nonSquares) exactly when its exponent in lcf is odd; |lcf| is 2 ^ v₂(lcf) times the powers of these primes with their exponents in lcf; and the signs are those of Ratpoints.Sieve.jacobiSigns for the number of these primes with an odd exponent that are 3 (mod 4), the sign of lcf and v₂(lcf).

Equations

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

def Ratpoints.Sieve.JacobiSetupInvariant (lcf : ℤ) (v w : ℕ) (qs : Array (ℕ × Option (Array Bool))) : Prop

The invariant of the loop of Ratpoints.Sieve.jacobiSetup on lcf with the exponent v of 2 in it, on the cofactor w and the entries qs: for lcf = 0, w = 0; otherwise |lcf| is 2 ^ v w times the powers of the primes of qs with their exponents in lcf, w is odd, and the entries are odd primes of lcf from Ratpoints.primeTable that do not divide w, each with the table of the non-squares exactly when its exponent in lcf is odd.

Equations

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

theorem Ratpoints.Sieve.jacobiSetupInvariant_empty {lcf : ℤ} {v r : ℕ} (hv : (v, r) = (Setup.valuation lcf 2).run) : JacobiSetupInvariant lcf v (lcf.natAbs / 2 ^ v) #[]

def Ratpoints.Sieve.JacobiSetupLoopInvariant (lcf : ℤ) (v : ℕ) (suff : List ℕ) (st : Option (Option JacobiInfo) × ℕ × Array (ℕ × Option (Array Bool)) × Array ℕ × ℕ × ℕ) : Prop

The invariant of the loop of Ratpoints.Sieve.jacobiSetup over the primes of the table, with the primes suff still to come, on the result of an early return, the cofactor, the entries, the reciprocals, the number n3 and the space taken by the tables: without a result, Ratpoints.Sieve.JacobiSetupInvariant of the cofactor and the entries, with the reciprocals those of the primes of the entries in their order (Ratpoints.Sieve.magic) and n3 the number of the entries with a table whose prime is 3 (mod 4); and a result, which is none, only at the end.

Equations

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

theorem Ratpoints.Sieve.jacobiSetupLoopInvariant_empty {lcf : ℤ} {v r : ℕ} (hv : (v, r) = (Setup.valuation lcf 2).run) (suff : List ℕ) (u : ℕ) : JacobiSetupLoopInvariant lcf v suff (none, lcf.natAbs / 2 ^ v, #[], #[], 0, u)

theorem Ratpoints.Sieve.jacobiSetupLoopInvariant_some_none (lcf : ℤ) (v w n3 u : ℕ) (qs : Array (ℕ × Option (Array Bool))) (ms : Array ℕ) : JacobiSetupLoopInvariant lcf v [] (some none, w, qs, ms, n3, u)

theorem Ratpoints.Sieve.JacobiSetupLoopInvariant.of_cons {lcf : ℤ} {v w n3 u cur : ℕ} {qs : Array (ℕ × Option (Array Bool))} {ms : Array ℕ} {suff suff' : List ℕ} {o : Option (Option JacobiInfo)} (h : JacobiSetupLoopInvariant lcf v (cur :: suff) (o, w, qs, ms, n3, u)) : JacobiSetupLoopInvariant lcf v suff' (none, w, qs, ms, n3, u)

Before the last prime, the loop of Ratpoints.Sieve.jacobiSetup has not returned, and its state passes on unchanged to any primes to come.

theorem Ratpoints.Sieve.JacobiSetupInvariant.dvd_natAbs {lcf : ℤ} {v w : ℕ} {qs : Array (ℕ × Option (Array Bool))} (h : JacobiSetupInvariant lcf v w qs) (h0 : lcf ≠ 0) : w ∣ lcf.natAbs

theorem Ratpoints.Sieve.JacobiSetupInvariant.padicValNat_eq {lcf : ℤ} {v w q e m : ℕ} {qs : Array (ℕ × Option (Array Bool))} (h0 : lcf ≠ 0) (h : JacobiSetupInvariant lcf v w qs) (hq : Nat.Prime q) (hm : w = q ^ e * m) (hqm : ¬q ∣ m) (hqw : q ∣ w) : padicValNat q lcf.natAbs = e

The exponent e of a prime q of the cofactor w = q ^ e m, q ∤ m, is v_q(lcf), since q is neither 2 nor one of the primes taken out before.

theorem Ratpoints.Sieve.JacobiSetupInvariant.push {lcf : ℤ} {v w cur e r : ℕ} {pref suff : List ℕ} {qs : Array (ℕ × Option (Array Bool))} {ns : Option (Array Bool)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (h : JacobiSetupInvariant lcf v w qs) (hw : ¬(w % cur != 0) = true) (he : (e, r) = (Setup.valuation (↑w) cur).run) (hns : ns = if e % 2 = 1 then some (nonSquares cur).run else none) : JacobiSetupInvariant lcf v (w / cur ^ e) (qs.push (cur, ns))

An entry (q, ns) for a prime q of the cofactor w = q ^ e m, q ∤ m, with its exponent e = v_q(lcf) and the table of the non-squares exactly for odd e, leaves the cofactor m.

theorem Ratpoints.Sieve.JacobiSetupLoopInvariant.push {lcf : ℤ} {v w n3 n3' u u' cur e r : ℕ} {pref suff : List ℕ} {qs : Array (ℕ × Option (Array Bool))} {ms : Array ℕ} {o : Option (Option JacobiInfo)} {ns : Option (Array Bool)} (hl : ForIn.toList primeTable = pref ++ cur :: suff) (h : JacobiSetupLoopInvariant lcf v (cur :: suff) (o, w, qs, ms, n3, u)) (hw : ¬(w % cur != 0) = true) (he : (e, r) = (Setup.valuation (↑w) cur).run) (hns : ns = if e % 2 = 1 then some (nonSquares cur).run else none) (hn3 : n3' = n3 + if (ns.isSome && cur &&& 2 != 0) = true then 1 else 0) : JacobiSetupLoopInvariant lcf v suff (none, w / cur ^ e, qs.push (cur, ns), ms.push (magic cur), n3', u')

An entry for the prime cur of the table that divides the cofactor w, with the table of the non-squares exactly for an odd exponent e, and the count n3 of the entries with a table whose prime is 3 (mod 4); the space u' taken by the tables is free.

theorem Ratpoints.Sieve.JacobiSetupLoopInvariant.false_of_some {lcf : ℤ} {v w n3 u : ℕ} {qs : Array (ℕ × Option (Array Bool))} {ms : Array ℕ} {o : Option (Option JacobiInfo)} {a : Option JacobiInfo} {ji : JacobiInfo} (h : JacobiSetupLoopInvariant lcf v [] (o, w, qs, ms, n3, u)) (ho : o = some a) (ha : a = some ji) : False

theorem Ratpoints.Sieve.JacobiSetupLoopInvariant.isJacobiInfo {lcf : ℤ} {bHigh v r w n3 u : ℕ} {qs : Array (ℕ × Option (Array Bool))} {ms : Array ℕ} {o : Option (Option JacobiInfo)} {ji : JacobiInfo} (hb : ¬mulModLimit < bHigh) (hv : (v, r) = (Setup.valuation lcf 2).run) (h : JacobiSetupLoopInvariant lcf v [] (o, w, qs, ms, n3, u)) (ho : o = none) (hw : ¬(w != 1) = true) (hji : some { primes := qs.toList, magic := ms, sign := jacobiSigns n3 (decide (lcf < 0)) v } = some ji) : bHigh ≤ mulModLimit ∧ lcf ≠ 0 ∧ IsJacobiInfo lcf ji ∧ (∀ x ∈ ji.primes, x.1 ∈ primeTable) ∧ ji.magic.toList = List.map (fun (x : ℕ × Option (Array Bool)) => magic x.1) ji.primes

At the end of the loop of Ratpoints.Sieve.jacobiSetup with the cofactor 1, lcf ≠ 0, the tables are those of lcf, their primes are from Ratpoints.primeTable, and they hold the reciprocals of their primes.

theorem Ratpoints.Sieve.jacobiSetup_spec (lcf : ℤ) (bHigh : ℕ) : ⦃ True ⦄ jacobiSetup lcf bHigh ⦃ fun (r : Option JacobiInfo) => ∀ (ji : JacobiInfo), r = some ji → bHigh ≤ mulModLimit ∧ lcf ≠ 0 ∧ IsJacobiInfo lcf ji ∧ (∀ x ∈ ji.primes, x.1 ∈ primeTable) ∧ ji.magic.toList = List.map (fun (x : ℕ × Option (Array Bool)) => magic x.1) ji.primes ⦄

The set-up of the test by tables gives tables only for bHigh ≤ Ratpoints.mulModLimit and lcf ≠ 0, and then the tables of lcf (Ratpoints.Sieve.IsJacobiInfo), whose primes are from Ratpoints.primeTable and which hold their reciprocals, so that the reductions of the test by them are exact.

The test by tables

structure Ratpoints.Sieve.JacobiTestPre (ji : JacobiInfo) (b : ℕ) : Prop

The precondition of Ratpoints.Sieve.jacobiTest on the tables ji and the denominator b, under which the reductions by the reciprocals that the tables hold are exact.

• pos : 0 < b

  The denominator is positive.

• lt_size : b < UInt64.size

  The denominator is below 2 ^ 64.

• prime_mul_lt (x : ℕ × Option (Array Bool)) : x ∈ ji.primes → Nat.Prime x.1 ∧ b * x.1 < 2 ^ 64

  The entries are primes q with b q < 2 ^ 64.

• magic_eq : ji.magic.toList = List.map (fun (x : ℕ × Option (Array Bool)) => magic x.1) ji.primes

  The tables hold the reciprocals of their primes.

def Ratpoints.Sieve.JacobiTestInvariant (ji : JacobiInfo) (b : ℕ) (pref : List (ℕ × Option (Array Bool))) (b' : ℕ) : Prop

The invariant of the first loop of Ratpoints.Sieve.jacobiTest on the tables ji and the denominator b, after the entries pref: the current b' is odd and positive, has the part of b free of 2 and of the primes of ji, is prime to the primes of pref, and is at most b, so that the reductions by the reciprocals of the primes stay exact (Ratpoints.Sieve.mulDiv_magic).

Equations

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

def Ratpoints.Sieve.JacobiDivideInvariant (ji : JacobiInfo) (b : ℕ) (pref : List (ℕ × Option (Array Bool))) (q : ℕ) : Std.WP.WhileInvariant ℕ Prop

The invariant of the loop of Ratpoints.Sieve.jacobiTest that divides b' by the prime q as often as it divides: that of the first loop, and q ∤ b' at the exit.

Equations

• Ratpoints.Sieve.JacobiDivideInvariant ji b pref q = Std.WP.WhileInvariant.mk fun (exit : Bool) (b' : ℕ) => Ratpoints.Sieve.JacobiTestInvariant ji b pref b' ∧ (exit = true → ¬q ∣ b')

theorem Ratpoints.Sieve.jacobiTestInvariant_nil {ji : JacobiInfo} {b t : ℕ} (h : JacobiTestPre ji b) (ht : t = (UInt64.ofNat b).toBitVec.ctz.toNat) : JacobiTestInvariant ji b [] (b >>> t)

theorem Ratpoints.Sieve.JacobiTestInvariant.mulDiv_getElem!_magic {ji : JacobiInfo} {b b' q i : ℕ} {o : Option (Array Bool)} {pref : List (ℕ × Option (Array Bool))} {pref' suff' : List ((ℕ × Option (Array Bool)) × ℕ)} (hpre : JacobiTestPre ji b) (hl : ji.primes.zipIdx = pref' ++ ((q, o), i) :: suff') (h : JacobiTestInvariant ji b pref b') : mulDiv b' ji.magic[i]! = b' / q

The quotient by the prime q of the entry at the position i of the tables ji, by the reciprocal that the tables hold there, is exact for the current b' ≤ b, since b q < 2 ^ 64.

theorem Ratpoints.Sieve.JacobiTestInvariant.sub_mulDiv_getElem!_magic_mul {ji : JacobiInfo} {b b' q i : ℕ} {o : Option (Array Bool)} {pref : List (ℕ × Option (Array Bool))} {pref' suff' : List ((ℕ × Option (Array Bool)) × ℕ)} (hpre : JacobiTestPre ji b) (hl : ji.primes.zipIdx = pref' ++ ((q, o), i) :: suff') (h : JacobiTestInvariant ji b pref b') : b' - mulDiv b' ji.magic[i]! * q = b' % q

The remainder by the prime q of the entry at the position i of the tables ji, by the reciprocal that the tables hold there, is exact for the current b' ≤ b, since b q < 2 ^ 64.

theorem Ratpoints.Sieve.JacobiTestInvariant.eq_prod_filter {ji : JacobiInfo} {b b' : ℕ} (h : JacobiTestInvariant ji b ji.primes b') : b' = (List.filter (fun (p : ℕ) => decide (p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes)) b.primeFactorsList).prod

At the end of the first loop of Ratpoints.Sieve.jacobiTest, b' is the part of b free of 2 and of the primes of the tables.

def Ratpoints.Sieve.JacobiTestSignInvariant (ji : JacobiInfo) (b' : ℕ) (pref : List (ℕ × Option (Array Bool))) (s : Bool) : Prop

The invariant of the second loop of Ratpoints.Sieve.jacobiTest on the tables ji and the odd part b' free of their primes, after the entries pref: the sign s is the exclusive or of the sign of b' mod 8 and the entries of b' mod q in the tables of the primes q of pref.

Equations

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

theorem Ratpoints.Sieve.jacobiTestSignInvariant_nil (ji : JacobiInfo) (b' : ℕ) : JacobiTestSignInvariant ji b' [] ji.sign[b' % 8]!

theorem Ratpoints.Sieve.JacobiTestSignInvariant.not_eq_not_foldl {ji : JacobiInfo} {b b' : ℕ} {s : Bool} (h : JacobiTestInvariant ji b ji.primes b') (hs : JacobiTestSignInvariant ji b' ji.primes s) : (!s) = !List.foldl (fun (s : Bool) (x : ℕ × Option (Array Bool)) => x.2.elim s fun (ns : Array Bool) => s ^^ ns[(List.filter (fun (p : ℕ) => decide (p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes)) b.primeFactorsList).prod % x.1]!) ji.sign[(List.filter (fun (p : ℕ) => decide (p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes)) b.primeFactorsList).prod % 8]! ji.primes

theorem Ratpoints.Sieve.JacobiTestSignInvariant.append_some {ji : JacobiInfo} {b b' q i : ℕ} {s : Bool} {pref : List (ℕ × Option (Array Bool))} {pref' suff' : List ((ℕ × Option (Array Bool)) × ℕ)} {o : Option (Array Bool)} {ns : Array Bool} (hpre : JacobiTestPre ji b) (hb : JacobiTestInvariant ji b ji.primes b') (hl : ji.primes.zipIdx = pref' ++ ((q, o), i) :: suff') (hs : JacobiTestSignInvariant ji b' pref s) (ho : o = some ns) : JacobiTestSignInvariant ji b' (pref ++ [(q, o)]) (s ^^ ns[b' - mulDiv b' ji.magic[i]! * q]!)

theorem Ratpoints.Sieve.JacobiTestSignInvariant.append_none {ji : JacobiInfo} {b' q : ℕ} {s : Bool} {pref : List (ℕ × Option (Array Bool))} {o o' : Option (Array Bool)} (hs : JacobiTestSignInvariant ji b' pref s) (hn : ∀ (ns : Array Bool), o' = some ns → False) (ho : o = o') : JacobiTestSignInvariant ji b' (pref ++ [(q, o)]) s

theorem Ratpoints.Sieve.JacobiTestInvariant.jacobiDivideInvariant {ji : JacobiInfo} {b b' q : ℕ} {pref : List (ℕ × Option (Array Bool))} (h : JacobiTestInvariant ji b pref b') : JacobiDivideInvariant ji b pref q false b'

theorem Ratpoints.Sieve.JacobiDivideInvariant.exit {ji : JacobiInfo} {b b' q i mb : ℕ} {pref : List (ℕ × Option (Array Bool))} {pref' suff' : List ((ℕ × Option (Array Bool)) × ℕ)} {o : Option (Array Bool)} (hpre : JacobiTestPre ji b) (hl : ji.primes.zipIdx = pref' ++ ((q, o), i) :: suff') (hq : (b' - mulDiv b' ji.magic[i]! * q != 0) = true) (h : b' = mb ∧ JacobiDivideInvariant ji b pref q false b') : JacobiDivideInvariant ji b pref q true b'

theorem Ratpoints.Sieve.JacobiDivideInvariant.jacobiTestInvariant {ji : JacobiInfo} {b b' q : ℕ} {pref : List (ℕ × Option (Array Bool))} {o : Option (Array Bool)} (h : JacobiDivideInvariant ji b pref q true b') : JacobiTestInvariant ji b (pref ++ [(q, o)]) b'

theorem Ratpoints.Sieve.JacobiDivideInvariant.div {ji : JacobiInfo} {b b' q i mb : ℕ} {o : Option (Array Bool)} {pref : List (ℕ × Option (Array Bool))} {pref' suff' : List ((ℕ × Option (Array Bool)) × ℕ)} (hpre : JacobiTestPre ji b) (hl : ji.primes.zipIdx = pref' ++ ((q, o), i) :: suff') (hq : ¬(b' - mulDiv b' ji.magic[i]! * q != 0) = true) (h : b' = mb ∧ JacobiDivideInvariant ji b pref q false b') : mulDiv b' ji.magic[i]! < mb ∧ JacobiDivideInvariant ji b pref q false (mulDiv b' ji.magic[i]!)

Dividing b' by a prime q of the tables keeps the part of b' free of 2 and of the primes of the tables.

theorem Ratpoints.Sieve.jacobiTest_spec (ji : JacobiInfo) (b : ℕ) : ⦃ JacobiTestPre ji b ⦄ jacobiTest ji b ⦃ fun (r : Bool) => r = !List.foldl (fun (s : Bool) (x : ℕ × Option (Array Bool)) => x.2.elim s fun (ns : Array Bool) => s ^^ ns[(List.filter (fun (p : ℕ) => decide (p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes)) b.primeFactorsList).prod % x.1]!) ji.sign[(List.filter (fun (p : ℕ) => decide (p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes)) b.primeFactorsList).prod % 8]! ji.primes ⦄

The test by tables on 0 < b < 2 ^ 64, for tables whose entries are primes q with b q < 2 ^ 64 and which hold the reciprocals of their primes, so that the reductions by them are exact: the exclusive or of the sign of b* mod 8 and the entries of b* mod q in the tables of the primes q, negated, for b* the part of b free of 2 and of the primes of the tables.

The Jacobi symbol by the tables

theorem Ratpoints.Sieve.ite_foldl_xor_eq_mul_prod {b : ℕ} (L : List (ℕ × Option (Array Bool))) (s : Bool) : (if List.foldl (fun (s : Bool) (x : ℕ × Option (Array Bool)) => x.2.elim s fun (ns : Array Bool) => s ^^ ns[b % x.1]!) s L = true then -1 else 1) = (if s = true then -1 else 1) * (List.map (fun (x : ℕ × Option (Array Bool)) => x.2.elim 1 fun (ns : Array Bool) => if ns[b % x.1]! = true then -1 else 1) L).prod

theorem Ratpoints.Sieve.jacobiSym_pow_eq_mul {q b e : ℕ} {o : Option (Array Bool)} [hq : Fact (Nat.Prime q)] (hq2 : q ≠ 2) (hb : b % 2 = 1) (hqb : ¬q ∣ b) (ho : o = if e % 2 = 1 then some (nonSquares q).run else none) : jacobiSym (↑q) b ^ e = (if (o.isSome && q &&& 2 != 0) = true then ZMod.χ₄ ↑b else 1) * o.elim 1 fun (ns : Array Bool) => if ns[b % q]! = true then -1 else 1

The factor J(q | b) ^ e of an odd prime q ∤ b of the leading coefficient with its exponent e, for odd b: 1 for even e, and for odd e, with the table ns of the non-squares modulo q, the entry of b mod q read as a sign, times χ₄(b) when q ≡ 3 (mod 4).

theorem Ratpoints.Sieve.jacobiSym_natAbs_eq_mul_prod {lcf : ℤ} {v b : ℕ} {L : List (ℕ × Option (Array Bool))} (h : lcf.natAbs = 2 ^ v * (List.map (fun (x : ℕ × Option (Array Bool)) => x.1 ^ padicValNat x.1 lcf.natAbs) L).prod) (hb : b % 2 = 1) : jacobiSym (↑lcf.natAbs) b = ZMod.χ₈ ↑b ^ v * (List.map (fun (x : ℕ × Option (Array Bool)) => jacobiSym (↑x.1) b ^ padicValNat x.1 lcf.natAbs) L).prod

theorem Ratpoints.Sieve.prod_map_jacobiSym_pow_eq {lcf : ℤ} {L : List (ℕ × Option (Array Bool))} (h : ∀ x ∈ L, Nat.Prime x.1 ∧ x.1 ≠ 2 ∧ x.1 ∣ lcf.natAbs ∧ x.2 = if padicValNat x.1 lcf.natAbs % 2 = 1 then some (nonSquares x.1).run else none) {b : ℕ} (hb : b % 2 = 1) (hq : ∀ x ∈ L, ¬x.1 ∣ b) : (List.map (fun (x : ℕ × Option (Array Bool)) => jacobiSym (↑x.1) b ^ padicValNat x.1 lcf.natAbs) L).prod = ZMod.χ₄ ↑b ^ (List.filter (fun (x : ℕ × Option (Array Bool)) => x.2.isSome && x.1 &&& 2 != 0) L).length * (List.map (fun (x : ℕ × Option (Array Bool)) => x.2.elim 1 fun (ns : Array Bool) => if ns[b % x.1]! = true then -1 else 1) L).prod

theorem Ratpoints.Sieve.jacobiSym_eq_ite_foldl {lcf : ℤ} {ji : JacobiInfo} (hji : IsJacobiInfo lcf ji) {b : ℕ} (hb : b % 2 = 1) (hq : ∀ x ∈ ji.primes, ¬x.1 ∣ b) : jacobiSym lcf b = if List.foldl (fun (s : Bool) (x : ℕ × Option (Array Bool)) => x.2.elim s fun (ns : Array Bool) => s ^^ ns[b % x.1]!) ji.sign[b % 8]! ji.primes = true then -1 else 1

The Jacobi symbol by the tables. The symbol (lcf / b) of an odd b prime to the primes of the tables ji of lcf is read off the tables, by quadratic reciprocity: the exclusive or of the sign of b mod 8 and the entries of b mod q in the tables of the primes q with an odd exponent, read as -1 for true.

theorem Ratpoints.Sieve.IsJacobiInfo.coprime_two_mul_natAbs_iff {lcf : ℤ} {ji : JacobiInfo} (hji : IsJacobiInfo lcf ji) {p : ℕ} (hp : Nat.Prime p) : p.Coprime (2 * lcf.natAbs) ↔ p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes

For the tables of lcf, the primes prime to 2 lcf are those other than 2 and the primes of the tables, which are all the odd primes of lcf.

theorem Ratpoints.Sieve.IsJacobiInfo.prod_filter_primeFactorsList_eq {lcf : ℤ} {ji : JacobiInfo} (hji : IsJacobiInfo lcf ji) (b : ℕ) : (List.filter (fun (p : ℕ) => decide (p ≠ 2 ∧ p ∉ List.map Prod.fst ji.primes)) b.primeFactorsList).prod = b.coprimePart (2 * lcf.natAbs)

theorem Ratpoints.Sieve.run_jacobiTest {lcf : ℤ} {bHigh : ℕ} {ji : JacobiInfo} (hji : (jacobiSetup lcf bHigh).run = some ji) {b : ℕ} (hb : b ≠ 0) (hbH : b ≤ bHigh) : (jacobiTest ji b).run = decide (jacobiSym lcf (b.coprimePart (2 * lcf.natAbs)) = 1)

The test by tables. It decides whether (lcf / b*) = 1, b* the largest divisor of b prime to 2 lcf, for 1 ≤ b ≤ bHigh when the set-up gives tables. The C code refuses the tables for a b_high above Ratpoints.mulModLimit, RP_MULMOD_LIMIT (find_points.c:688), so that jacobi_test divides only numbers below 2 ^ 32, where its multiplication by the reciprocal RP_MULDIV is exact (rp-private.h:389-393).

theorem Ratpoints.Sieve.run_jacobiTest_of_sq_eq {c : List ℤ} (hd : degree c % 2 = 0) {bHigh : ℕ} {ji : JacobiInfo} (hji : (jacobiSetup (c.getD (degree c) 0) bHigh).run = some ji) {a y : ℤ} {b : ℕ} (hb : b ≠ 0) (hbH : b ≤ bHigh) (hab : a.gcd ↑b = 1) (hy : y ^ 2 = binaryForm c a ↑b) : (jacobiTest ji b).run = true

The Jacobi test by the tables of the leading coefficient, when they apply, passes the denominator b ≤ bHigh of every point of a curve of even degree: it computes whether the Jacobi symbol (c_d / b*) is 1.