theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected_I10_upper (δ : ℝ) (hδ : 0 < δ) (ε : ℝ) : 0 < ε → ε < 1 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachG10Corrected (goldbachDifferenceCarrier N ε) N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma)) ≤ (8 * (1 - ε) * goldbachB10I10 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The separately named corrected G10 has the actual integral upper bound. This does not identify the corrected count with the original printed G10.