theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSiftedCount_normalized_kernel (δ η : ℝ) (hδ : 0 < δ) (hη : 0 < η) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → have Z := √(↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1)); 2 ≤ Z ∧ Z ≤ √↑N ∧ ↑(goldbachB10SiftedCount N 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) Z) ≤ ((8 + δ) * goldbachK9High N + η) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The actual high BoundingSieve, uniform Euler product and relative Li estimate. Only the scalar cutoff geometry is borrowed from the full-domain consumer.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstClosed_normalized_upper (δ ε : ℝ) (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))) ≤ ((8 + δ) * goldbachK9High N + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Independent upper bound for actual high S5; no free analytic or sieve input remains.