theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Plus_upperErrSum_le_levelRemainder (N : ℕ) (hEven : Even N) (Z Δ : ℝ) : have S := goldbachB10BoundingSieve N hEven 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z (goldbachB9PlusMainMass N); LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ ∑ d ∈ S.prodPrimes.divisors with d < ⌊Δ⌋₊ + 1, |BoundingSieve.rem d|

The full Rosser error is dominated on its actual strict-level support, including one.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Plus_upperErrSum_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (Z : ℝ), have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have S := goldbachB10BoundingSieve N hEven 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z (goldbachB9PlusMainMass N); LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ C * ↑N / Real.log ↑N ^ U

No comparison of Z with either factor of the closed C10 support is needed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSiftedCount_upper_paid (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (ρ : ℝ), 0 < ρ → ∃ (z₀ : ℝ), ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (Z s : ℝ), z₀ ≤ Z → 2 ≤ Z → s = Real.log (↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1)) / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → have S := goldbachB10BoundingSieve N hEven 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z (goldbachB9PlusMainMass N); ↑(goldbachB10SiftedCount N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z) ≤ goldbachB9PlusMainMass N * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + C * ↑N / Real.log ↑N ^ U

The genuine zero-prefix sieve with its fixed full Li mass and all errors paid. The constants and N threshold precede the Rosser tolerance and cutoff.