theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_sieveDivisor_coprime (N : ℕ) {ε Z : ℝ} (hN : 1 ≤ N) (hεu : ε < 2 / 15) {r d : ℕ} (hr : r ∈ goldbachS2Primes N (↑N ^ (9 / 19 - ε))) (hZ : Z ≤ ↑N ^ (1 / 4)) (hd : d ∣ goldbachS1ProdPrimes N Z) : r.Coprime d

Every actual S2 large prime is coprime to every divisor of the standard sieving-prime product at a cutoff at most N^(1/4). No gate-loss estimate is needed on this support. This does not yet construct the switched sieve.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_gated_sum_eq_sum (N : ℕ) {ε Z : ℝ} (hN : 1 ≤ N) (hεu : ε < 2 / 15) {d : ℕ} (hZ : Z ≤ ↑N ^ (1 / 4)) (hd : d ∣ goldbachS1ProdPrimes N Z) (w : ℕ → ℝ) : (∑ r ∈ goldbachS2Primes N (↑N ^ (9 / 19 - ε)), if r.Coprime d then w r else 0) = ∑ r ∈ goldbachS2Primes N (↑N ^ (9 / 19 - ε)), w r

The actual large-prime main sum has no coprimality deletion on these sieving divisors, for any real mass attached to each large prime.