VW pairs

The paper stipulates u < 0 < m and w ≤ 0 < v. These bounds are formalised by typing all four variables as natural numbers, negating u and w as needed.

The bound w ≤ (m + 1) * primorial m is not used in any proof and has been removed. The bound primorial m < v has been simplified to m < v.

Note that the paper's algorithm does not necessarily guarantee q < v (without the negations performed in this file). For example, take m = 5, q = 30, u = -2, then step 1 sets v = 29, w = -31 and both numbers are unchanged in the rest of the algorithm because 29 and 31 are big primes.

The coprimality condition only requires 0 < u ≤ m and is proved separately.

structure VWPair (u m : ℕ) : Type

VWPair u m holds v and w and states that -u, m, v, -w satisfy the conditions in Lemma 2.2.

• v : ℕ

  v in the paper

• w : ℕ

  w in the paper, negated

• eq_add : self.w = u + self.v

  u = v + w in the paper

• m_lt_v : m < self.v

  m < v

• w_odd : Odd self.w

  w is odd

• not_dvd (k : ℕ) (hk : k ∈ Finset.Icc 3 m) : ¬k ∣ self.v ∧ ¬k ∣ self.w

  No number in [3,m] divides v or w

theorem VWPair.nonempty_double_not_dvd (v w p : ℕ) (hp : 3 ≤ p) : {i : Fin p | ¬p ∣ v + ↑i ∧ ¬p ∣ w + ↑i}.Nonempty

theorem VWPair.nonempty_double_not_dvd_four (v w : ℕ) : {i : Fin 4 | ¬4 ∣ v + ↑i ∧ ¬2 ∣ w + ↑i}.Nonempty

Note the divisor of 2 and not 4 for w.

def VWPair.fourAndOddPrimes (m : ℕ) : Finset ℕ

The finset consisting of 4 and all odd primes at most m.

Equations

• VWPair.fourAndOddPrimes m = insert 4 ({p ∈ Finset.Icc 3 m | Nat.Prime p})

theorem VWPair.zero_notMem_fourAndOddPrimes {m : ℕ} : 0 ∉ fourAndOddPrimes m

theorem VWPair.fourAndOddPrimes_pairwise_coprime {m : ℕ} : (↑(fourAndOddPrimes m)).Pairwise Nat.Coprime

def VWPair.nonDividingShift (v w p : ℕ) : ℕ

Produce a number i < p such that v + i and w + i are both not divisible by p. When p = 4, w + i is additionally guaranteed to be odd. Return 0 for p ≤ 2.

Equations

• VWPair.nonDividingShift v w p = if p = 4 then ↑({i : Fin 4 | ¬4 ∣ v + ↑i ∧ ¬2 ∣ w + ↑i}.min' ⋯) else if hp : 3 ≤ p then ↑({i : Fin p | ¬p ∣ v + ↑i ∧ ¬p ∣ w + ↑i}.min' ⋯) else 0

theorem VWPair.not_dvd_nonDividingShift_of_three_le {v w p : ℕ} (hp : 3 ≤ p) : ¬p ∣ v + nonDividingShift v w p ∧ ¬p ∣ w + nonDividingShift v w p

def VWPair.crtShift (v w m : ℕ) : ℕ

crtShift v w m is a number that can be added to v, w such that

• no number in [3,m] divides the resulting v or w
• the resulting w is odd.

This number is calculated through the Chinese remainder theorem.

Equations

• VWPair.crtShift v w m = ↑(Nat.chineseRemainderOfFinset (VWPair.nonDividingShift v w) id (VWPair.fourAndOddPrimes m) ⋯ ⋯)

theorem VWPair.crtShift_modEq {v w m p : ℕ} (mi : p ∈ fourAndOddPrimes m) : crtShift v w m ≡ nonDividingShift v w p [MOD p]

theorem VWPair.crtShift_not_dvd {v w m k : ℕ} (hk : k ∈ Finset.Icc 3 m) : ¬k ∣ v + crtShift v w m ∧ ¬k ∣ w + crtShift v w m

theorem VWPair.odd_add_crtShift {v w m : ℕ} : Odd (w + crtShift v w m)

def VWPair.of (u m : ℕ) : VWPair u m

Lemma 2.2. A VWPair u m always exists.

Equations

• VWPair.of u m = { v := m + 1 + VWPair.crtShift (m + 1) (m + 1 + u) m, w := m + 1 + u + VWPair.crtShift (m + 1) (m + 1 + u) m, eq_add := ⋯, m_lt_v := ⋯, w_odd := ⋯, not_dvd := ⋯ }

theorem VWPair.of_coprime {u m : ℕ} (hu : 0 < u) (hm : u ≤ m) : (of u m).v.Coprime (of u m).w

When 0 < u ≤ m, v and w are coprime.

def vwTup {n m s B : ℕ} (vw : VWPair (m + ∑ i ∈ Finset.range n, primeChain s i) B) (i : Fin (n + 3)) : ℤ

An (n + 3)-tuple reducing to chainTup n m s.

Equations

• vwTup vw i = Fin.addCases (fun (x : Fin n) => ↑(primeChain s ↑x)) (fun (x : Fin 3) => match x with | 0 => ↑vw.v | 1 => -↑vw.w | 2 => ↑m) i

theorem vwTup_compl {n : ℕ} : {Fin.natAdd n 0, Fin.natAdd n 1}ᶜ = insert (Fin.natAdd n 2) (Finset.map (Fin.castAddEmb 3) Finset.univ)

theorem isSubsumBlock_vwTup {n m s B : ℕ} {vw : VWPair (m + ∑ i ∈ Finset.range n, primeChain s i) B} (hB : m + ∑ i ∈ Finset.range n, primeChain s i ≤ B) : IsSubsumBlock (vwTup vw) {Fin.natAdd n 0, Fin.natAdd n 1}

theorem tupReduce_vwTup {n m s B : ℕ} {vw : VWPair (m + ∑ i ∈ Finset.range n, primeChain s i) B} {c₂ : n + 1 = n + 3 - {Fin.natAdd n 0, Fin.natAdd n 1}.card} : tupReduce (vwTup vw) {Fin.natAdd n 0, Fin.natAdd n 1} c₂ = chainTup n m s

theorem strongSSC_vwTup {n m s B : ℕ} {vw : VWPair (m + ∑ i ∈ Finset.range n, primeChain s i) B} (hm : 0 < m) (hs : m ≤ s) (hB : m + ∑ i ∈ Finset.range n, primeChain s i ≤ B) : StrongSSC (vwTup vw)