theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10SwitchErrors_le_880 (N : ℕ) (ε β : ℝ) (hε : 0 < ε) (hN : 1 ≤ N) (hβ : β ≤ 1 / 2) (hz : 2 ≤ ↑N ^ β) : ↑(400 * goldbachBadCount (goldbachDifferenceCarrier N ε) N + 40 * goldbachQA (goldbachDifferenceCarrier N ε) N (↑N ^ β)) ≤ 880 * ↑N ^ (1 - β)

Payment for the actual additional bad and square masses of the candidate switch.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected_eventually_le_pi10_add_880 (ε : ℝ) (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (β γ : ℝ), 1 / 18 < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → ↑(goldbachG10Corrected (goldbachDifferenceCarrier N ε) N (↑N ^ β) (↑N ^ γ)) ≤ ↑(goldbachPi10 N ε (↑N ^ β) (↑N ^ γ)) + 880 * ↑N ^ (1 - β)

A parameter-uniform paid upper bound for the separately named candidate G10. This does not assert an analytic upper bound for the labelled prime source.