theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PaperSplitIntegral_eq_low_high : goldbachB9PaperSplitIntegral = 36 / 5 * fouvryG9RelaxedIntegralLow + 8 * goldbachB9HighMainIntegral

The literal paper coefficient is exactly the two proved analytic coefficients.

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

The full original S5 sum has the paper's split-integral upper bound. The strict low and closed high terms partition all original labels exactly.