theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachQuadruple_exceptions_normalized (delta : ℝ) (hdelta : 0 < delta) : ∃ (N0 : ℕ), 4 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ∀ (eps : ℝ), 0 ≤ eps → ∀ (b : ℝ), ↑(∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) b, goldbachG11RSquareCount (goldbachDifferenceCarrier N eps) v + ∑ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) b, goldbachG11NCount (goldbachDifferenceCarrier N eps) N v) ≤ delta * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)