theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_upperErrSum_le_prefixSum {N : ℕ} (hEven : Even N) {ε z y : ℝ} (Q : ℕ) (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) : ∑ p ∈ goldbachClosedPrimes N z y, LinearSieve.upperErrSum (goldbachS3BoundingSieve N hEven ε z p) (Q / p + 1) (LinearSieve.upperRosserWeight (goldbachS1ProdPrimes N z) (Q / p + 1)) ≤ ∑ k ∈ Finset.Icc 1 Q, BombieriVinogradov.standardPrimeAPPrefixMaxError N k

The actual conditional Rosser errors inject into the unweighted full modulus sum. In particular the divisor 1 is not removed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3Closed_upperRosser_paid (U : ℝ) (hU : 0 < U) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (y : ℝ), ↑N ^ (4 / 53) ≤ y → y ≤ ↑N ^ (1 / 3) → ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) y) ≤ BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * ∑ p ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) y, 1 / ↑p.totient * ∑ d ∈ (goldbachS1ProdPrimes N (↑N ^ (4 / 53))).divisors, LinearSieve.upperRosserWeight (goldbachS1ProdPrimes N (↑N ^ (4 / 53))) (LiuWeight.panModulusCutoff N B / p + 1) d / ↑d.totient + C * ↑N / Real.log ↑N ^ U

Actual closed S3 with the BV remainder paid, retaining the exact finite upper Rosser main sum and the strict-endpoint genuine logarithmic integral. Both constants precede epsilon, and the threshold is uniform in y.