Composite outer-modulus bridges for the original S3 sieve. No new carrier, center, or sieve record is introduced.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_multSum_eq_primesInAP {N : ℕ} (hEven : Even N) {ε z : ℝ} {k d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hkd : k.Coprime d) : BoundingSieve.multSum d = ↑(BombieriVinogradov.primesInAP (goldbachS1Endpoint N ε) (k * d) (N % (k * d)))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_rem_eq_standardPrimeAPError {N : ℕ} (hEven : Even N) {ε z : ℝ} {k d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hkd : k.Coprime d) (hd : d ∣ goldbachS1ProdPrimes N z) : BoundingSieve.rem d = BombieriVinogradov.standardPrimeAPError (goldbachS1Endpoint N ε) (k * d) (N % (k * d))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_mod_mem_unitResidues {N k d : ℕ} {z : ℝ} (hk : 0 < k) (hkN : k.Coprime N) (hd : d ∣ goldbachS1ProdPrimes N z) : N % (k * d) ∈ AnalyticNumberTheory.Sieve.unitResidues (k * d)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_abs_rem_le_prefix {N : ℕ} (hEven : Even N) {ε z : ℝ} {k d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hk : 0 < k) (hkd : k.Coprime d) (hkN : k.Coprime N) (hd : d ∣ goldbachS1ProdPrimes N z) : |BoundingSieve.rem d| ≤ BombieriVinogradov.standardPrimeAPPrefixMaxError N (k * d)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_pair_coprime_of_dvd_prodPrimes {N r s d : ℕ} {z y₁ y₂ : ℝ} (hr : r ∈ goldbachClosedPrimes N z y₁) (hs : s ∈ goldbachClosedPrimes N z y₂) (hd : d ∣ goldbachS1ProdPrimes N z) : (r * s).Coprime d

Only each outer prime versus the small sieve matters; r = s is allowed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_pair_coprime_N {N r s : ℕ} {z y₁ y₂ : ℝ} (hr : r ∈ goldbachClosedPrimes N z y₁) (hs : s ∈ goldbachClosedPrimes N z y₂) : (r * s).Coprime N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_pair_rem_eq_standardPrimeAPError {N : ℕ} (hEven : Even N) {ε z y₁ y₂ : ℝ} {r s d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hr : r ∈ goldbachClosedPrimes N z y₁) (hs : s ∈ goldbachClosedPrimes N z y₂) (hd : d ∣ goldbachS1ProdPrimes N z) : BoundingSieve.rem d = BombieriVinogradov.standardPrimeAPError (goldbachS1Endpoint N ε) (r * s * d) (N % (r * s * d))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_pair_abs_rem_le_prefix {N : ℕ} (hEven : Even N) {ε z y₁ y₂ : ℝ} {r s d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hr : r ∈ goldbachClosedPrimes N z y₁) (hs : s ∈ goldbachClosedPrimes N z y₂) (hd : d ∣ goldbachS1ProdPrimes N z) : |BoundingSieve.rem d| ≤ BombieriVinogradov.standardPrimeAPPrefixMaxError N (r * s * d)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_square_rem_eq {N : ℕ} (hEven : Even N) {ε z y : ℝ} {r d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hr : r ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : BoundingSieve.rem d = ↑(BombieriVinogradov.primesInAP (goldbachS1Endpoint N ε) (r ^ 2 * d) (N % (r ^ 2 * d))) - BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) / (↑(r ^ 2).totient * ↑d.totient)

The diagonal keeps φ(r²), not φ(r)².

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachCompositeSieve_square_abs_rem_le_prefix {N : ℕ} (hEven : Even N) {ε z y : ℝ} {r d : ℕ} (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (hr : r ∈ goldbachClosedPrimes N z y) (hd : d ∣ goldbachS1ProdPrimes N z) : |BoundingSieve.rem d| ≤ BombieriVinogradov.standardPrimeAPPrefixMaxError N (r ^ 2 * d)