theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_le_sifted_B8Plus_with_paid_finite_error (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ (3 / 11))) ≤ ↑(goldbachB8PlusSiftedAtoms N Z).card + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The actual S4 is transported to the labelled one-prefix switched count, with the bad-companion and small-output losses both absorbed. This leaves the switched sifted count itself to be estimated analytically.