theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10_normalized_upper (δ : ℝ) (hδ : 0 < δ) (ε γ : ℝ) : 0 < ε → ε < 1 → γ < 1 / 3 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (β : ℝ), 1 / 18 < β → ↑(goldbachPi10 N ε (↑N ^ β) (↑N ^ γ)) ≤ (8 + δ) * SingularSeries.liuSingularSeries N * goldbachB10MainMass N ε (↑N ^ β) (↑N ^ γ) / Real.log ↑N + δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

Exact normalized upper bound for the actual integer-valued Pi10 count. The auxiliary cutoff is eliminated from the statement and the full 400 * floor Z loss is paid into the final δ * 𝔖_Liu(N) * N / log(N)^2 remainder.