theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EulerFactor_normalized (B τ : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) (hτ1 : τ ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → (Real.exp Real.eulerMascheroniConstant + τ * Real.exp Real.eulerMascheroniConstant) * goldbachB10PrimeProduct N (goldbachG11SieveCutoff B N) ≤ 8 * (1 + τ) ^ 3 * SingularSeries.liuSingularSeries N / Real.log ↑N

Actual uniform square-root-level Euler/JR factor. This does not assert the paper's stronger low-band coefficient.