theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedCount_upper_paid (τ : ℝ) (hτ : 0 < τ) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), have Z := ↑N ^ (1 / 4); have T := ↑N ^ (9 / 19 - ε); have S := goldbachS2SwitchedBoundingSieve N hEven T Z; ↑(goldbachS2SwitchedSiftedCount N T Z) ≤ goldbachS2SwitchedMainMass N T * (Real.exp Real.eulerMascheroniConstant * (1 + τ)) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + C * ↑N / Real.log ↑N ^ 4

The actual switched S2 sifted count with the genuine Z = N^(1/4) cutoff and Δ = N^(1/2) / log(N)^(B+1) has its full Rosser remainder paid into the available logarithmic saving.