theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_sharpBuchstabIntegral (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ ((8 * (561522 / 1000000) * goldbachG11PrimeIntegral fun (x : ℝ) => 1) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual G11 with the proved sharp Buchstab constant, at the uniform sieve level. This is not the author's stronger low-band coefficient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11SharpBuchstabIntegral_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 * (561522 / 1000000) * goldbachG11PrimeIntegral fun (x : ℝ) => 1) - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

The sharp function constant is physically consumed by the actual signed D19 bound. The signed base and the low-prefix count remain unestimated.