theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9S5Low_integral_upper (τ : ℝ) (hτ : 0 < τ) (e : ℝ) (he : 0 < e) (he1 : e ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N e) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ (36 / 5 * fouvryG9RelaxedIntegralLow + τ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The actual low-first-prime S5 bound with the literal weighted integral. All sieve, distribution, prefix, mesh and perturbation parameters are internal. The product-window e is fixed before the natural-number threshold.