theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_upper_paid (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ρ : ℝ), 0 < ρ → ∃ (z₀ : ℝ), ∀ (ε γ : ℝ), 0 < ε → ε < 1 → γ < 1 / 3 → ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (β : ℝ), 1 / 18 < β → ∀ (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 X := goldbachB10MainMass N ε (↑N ^ β) (↑N ^ γ); have S := goldbachB10BoundingSieve N hEven ε (↑N ^ β) (↑N ^ γ) Z X; ↑(goldbachB10SiftedCount N ε (↑N ^ β) (↑N ^ γ) Z) ≤ X * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + C * ↑N / Real.log ↑N ^ U

Actual B10 upper linear sieve with the common main mass and the complete remainder paid. The genuine factor is used only on its proved ratio window. The main mass still uses the literal floor endpoint.