theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachOrderedPair_lowerErrSum_le_prefixSum {N : ℕ} (hEven : Even N) {ε z y₁ y₂ : ℝ} (Q : ℕ) (hε : 0 ≤ ε) (hm : 2 ≤ goldbachS1Endpoint N ε) (T : Finset (ℕ × ℕ)) (hT : ∀ a ∈ T, a.1 ∈ goldbachClosedPrimes N z y₁ ∧ a.2 ∈ goldbachClosedPrimes N z y₂ ∧ a.1 ≤ a.2) : ∑ 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)) ≤ ∑ k ∈ Finset.Icc 1 Q, BombieriVinogradov.standardPrimeAPPrefixMaxError N k

The complete lower Rosser error on the given ordered family is paid once by the full modulus prefix. Square pairs and the divisor one are retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachOrderedPair_lowerRosser_paid (U : ℝ) (hU : 0 < U) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (T : Finset (ℕ × ℕ)), (∀ a ∈ T, a.1 ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ a.2 ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (3 / 11)) ∧ a.1 ≤ a.2) → BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * ∑ a ∈ T, 1 / ↑(a.1 * a.2).totient * ∑ d ∈ (goldbachS1ProdPrimes N (↑N ^ (4 / 53))).divisors, LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N (↑N ^ (4 / 53))) (LiuWeight.panModulusCutoff N B / (a.1 * a.2) + 1) d / ↑d.totient - C * ↑N / Real.log ↑N ^ U ≤ ∑ a ∈ T, ↑(literalH (goldbachDifferenceCarrier N ε) N (a.1 * a.2) (↑N ^ (4 / 53)))

Actual ordered-pair sifted counts with the unconditional BV error paid. Constants and the common threshold precede every changing pair family.