theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_primeKernelIntegral_nonneg {β : ℝ} (hβ : 4 / 53 ≤ β) (hβu : β ≤ 1 / 3) : 0 ≤ goldbachS3_primeKernelIntegral β

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_normalized_upper (β δ ε : ℝ) (hβ : 4 / 53 < β) (hβu : β ≤ 1 / 3) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ β)) ≤ ((1 - ε) * (53 / 2) * Real.exp (-Real.eulerMascheroniConstant) * goldbachS3_primeKernelIntegral β + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Fully paid normalization of the actual closed S3, for each fixed beta. The strict mother carrier and the genuine source-factor integral are retained.