theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirst_actual_instance (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) ≤ ((8 + δ) * ∑ rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)), 1 / (↑(rs.1 * rs.2) * (1 - Real.log ↑(rs.1 * rs.2) / Real.log ↑N)) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)