theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_finiteLoss_le_sqrt (N : ℕ) (ε Z : ℝ) (hN : 1 ≤ N) (hZ : 0 ≤ Z) (hZu : Z ≤ √↑N) : 400 * ↑(goldbachBadCount (goldbachDifferenceCarrier N ε) N) + 400 * ↑⌊Z⌋₊ ≤ 1200 * √↑N

Pay labelled bad atoms and labelled small prime outputs; this does not assert the still separate finite S4-to-switched-carrier comparison.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_finiteLoss_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε Z : ℝ), 0 ≤ Z → Z ≤ √↑N → 400 * ↑(goldbachBadCount (goldbachDifferenceCarrier N ε) N) + 400 * ↑⌊Z⌋₊ ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The threshold is uniform in epsilon and every later moving cutoff Z. Only the actual finite transfer loss is paid, not the switched sifted count.