theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachOrderedPair_prime_not_dvd_small {N p d : ℕ} {z : ℝ} (hp : Nat.Prime p) (hzp : z ≤ ↑p) (hd : d ∣ goldbachS1ProdPrimes N z) : ¬p ∣ d

A prime at or above the sieve threshold cannot divide a small sieve divisor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachOrderedPair_mul_injective {N r s r' s' d e : ℕ} {z : ℝ} (hr : Nat.Prime r) (hs : Nat.Prime s) (hrs : r ≤ s) (hzr : z ≤ ↑r) (hr' : Nat.Prime r') (hs' : Nat.Prime s') (hrs' : r' ≤ s') (hzr' : z ≤ ↑r') (hd : d ∣ goldbachS1ProdPrimes N z) (he : e ∣ goldbachS1ProdPrimes N z) (heq : r * s * d = r' * s' * e) : r = r' ∧ s = s' ∧ d = e

Ordered pairs of primes above the sieve threshold, together with a small sieve divisor, are uniquely determined by their product. Repeated primes are allowed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachOrderedPair_prefix_doubleSum_le (N Q : ℕ) (z : ℝ) (T : Finset (ℕ × ℕ)) (hT : ∀ a ∈ T, Nat.Prime a.1 ∧ Nat.Prime a.2 ∧ a.1 ≤ a.2 ∧ z ≤ ↑a.1) : ∑ a ∈ T, ∑ d ∈ (goldbachS1ProdPrimes N z).divisors with d < Q / (a.1 * a.2) + 1, BombieriVinogradov.standardPrimeAPPrefixMaxError N (a.1 * a.2 * d) ≤ ∑ k ∈ Finset.Icc 1 Q, BombieriVinogradov.standardPrimeAPPrefixMaxError N k

The whole ordered-pair prefix error sum injects once into the ordinary full modulus prefix sum. There is no multiplicity factor, coprimality condition on N, strict-pair condition, or additional upper cutoff.