theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_kernel_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 K := goldbachB10MainLogProductSum N (↑N ^ β) (↑N ^ γ); ↑(goldbachB10SiftedCount N ε (↑N ^ β) (↑N ^ γ) Z) ≤ ((8 * (1 - ε) + δ) * K + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Physical join of the normalized sieve and the actual Li-to-kernel mass bound. Only the actual weighted prime-pair sum remains; no integral limit is assumed.