theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11NormalizedIntegral_consumed (W δ ε : ℝ) (hW0 : 0 ≤ W) (hδ : 0 < δ) (hW : ∀ u ∈ Set.Icc (17 / 4) (37 / 4), LiLiuPrereqBuchstab.buchstab u ≤ W) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (Zlow : ℝ), 1 ≤ Zlow → Zlow ≤ √↑N → ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Zlow) + ((goldbachWeightHighFirstCoefficient ε - 8 * W * goldbachG11PrimeIntegral fun (x : ℝ) => 1) - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Real D19 consumer of the actual Buchstab-sieve predecessor. The old signed base and low positive-prefix count are retained literally, without estimating any other branch. Sieve constants and cutoffs have all been internalized.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11NormalizedIntegral_one_consumed (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (Zlow : ℝ), 1 ≤ Zlow → Zlow ≤ √↑N → ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Zlow) + ((goldbachWeightHighFirstCoefficient ε - 8 * goldbachG11PrimeIntegral fun (x : ℝ) => 1) - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Unconditional integral D19 interface (W=1). It is a signed lower bound, not a positivity theorem and not the sharper author-weight coefficient.