theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachComposite_lowerRosser_finite {N : ℕ} (hEven : Even N) (ε z : ℝ) (p D : ℕ) (hprimeD : ∀ q ∈ (goldbachS1ProdPrimes N z).primeFactors, q < D) : BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * (1 / ↑p.totient * ∑ d ∈ (goldbachS1ProdPrimes N z).divisors, LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N z) D d / ↑d.totient) - LinearSieve.lowerErrSum (goldbachS3BoundingSieve N hEven ε z p) D (LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N z) D) ≤ ↑(literalH (goldbachDifferenceCarrier N ε) N p z)

The original divisibility-conditioned carrier satisfies the lower Rosser inequality for every outer modulus, including a square of a prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachOrderedPair_lowerRosser_finite {N : ℕ} (hEven : Even N) (ε z : ℝ) (Q : ℕ) (T : Finset (ℕ × ℕ)) (hprimeD : ∀ a ∈ T, ∀ q ∈ (goldbachS1ProdPrimes N z).primeFactors, q < Q / (a.1 * a.2) + 1) : BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * ∑ a ∈ T, 1 / ↑(a.1 * a.2).totient * ∑ d ∈ (goldbachS1ProdPrimes N z).divisors, LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N z) (Q / (a.1 * a.2) + 1) d / ↑d.totient - ∑ a ∈ T, LinearSieve.lowerErrSum (goldbachS3BoundingSieve N hEven ε z (a.1 * a.2)) (Q / (a.1 * a.2) + 1) (LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N z) (Q / (a.1 * a.2) + 1)) ≤ ∑ a ∈ T, ↑(literalH (goldbachDifferenceCarrier N ε) N (a.1 * a.2) z)

Exact signed summation on the given pair family. No main-density term is discarded, and no product image is substituted for the pair labels.