theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.high_integral_enclosure : goldbachB9HighMainIntegral ≤ highH (7 / 27) - highH 0 ∧ highH (7 / 27) - highH 0 ≤ goldbachB9HighMainIntegral + 7 / 27 / 10000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral_eight_mul_le_392796161 : 8 * goldbachB9HighMainIntegral ≤ 392796161 / 100000000

The actual high double integral, not the full G9 integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral_scalar_accuracy : 0 ≤ 392796161 / 100000000 - 8 * goldbachB9HighMainIntegral ∧ 392796161 / 100000000 - 8 * goldbachB9HighMainIntegral ≤ 1 / 1000000

Complete one-sided budget includes the analytic remainder and upward rounding.

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

Literal high-S5 consumer: epsilon domain, cutoff, threshold, and scale unchanged. There is no (1-epsilon) factor in the high producer.