theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_normalized_upper (δ : ℝ) (hδ : 0 < δ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε γ : ℝ), 0 < ε → ε < 1 → γ < 1 / 3 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (β : ℝ), 1 / 18 < β → have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have Z := Δ ^ (1 / 2); have X := goldbachB10MainMass N ε (↑N ^ β) (↑N ^ γ); ↑(goldbachB10SiftedCount N ε (↑N ^ β) (↑N ^ γ) Z) ≤ (8 + δ) * SingularSeries.liuSingularSeries N * X / Real.log ↑N + δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The already-produced paid upper bound and sieve-product estimate combine to the genuine coefficient 8 + δ once the cutoff is normalized by Z = ((N^(1/2))/log(N)^(B+1))^(1/2). The theorem retains the real main mass X and pays the full remainder into a true δ · 𝔖_Liu(N) · N / log(N)^2 term, with B chosen before ε, γ and N₀ chosen before β.