theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9S5Low_kernel_upper (τ ξ ζ : ℝ) (hτ : 0 < τ) (hξ : 0 < ξ) (hζ : 0 < ζ) {e ε δ ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ < 1 / 4) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N e) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ (4 * (1 + τ) * (1 + ξ) * (ρ ^ 3 * fouvryG9RelaxedPairKernel N ρ δ) + ζ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Literal low S5 reaches the actual relaxed kernel with all previous losses paid.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LowIntegral_nonneg : 0 ≤ fouvryG9RelaxedIntegralLow

Positivity of the literal weighted low integral, using its proved single form.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Low_final_budget (B τ : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) : ∃ (κ : ℝ), 0 < κ ∧ κ ≤ 1 / 4 ∧ 4 * (1 + κ) ^ 2 * (B + κ) + κ ≤ 4 * B + τ

A common small budget pays the two multiplicative and one additive errors.