theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_buchstabSieve (A ρ δ η : ℝ) (hA : 0 < A) (hρ : 0 < ρ) (hδ : 0 < δ) (hη : 0 < η) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 0 ≤ ε → ∀ (Z Δ : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → 2 = Real.log Δ / Real.log Z → Δ ≤ √↑N / Real.log ↑N ^ B → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ goldbachG11BuchstabSieveEnvelope N Z A C ρ η + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The actual G11 count, with the finite Buchstab main sum and the exceptional prime divisors of N retained explicitly. The sieve ratio is fixed at two.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11BuchstabSieve_consumed (A ρ δ η : ℝ) (hA : 0 < A) (hρ : 0 < ρ) (hδ : 0 < δ) (hη : 0 < η) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (Zlow : ℝ), 1 ≤ Zlow → Zlow ≤ √↑N → ∀ (Z Δ : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → 2 = Real.log Δ / Real.log Z → Δ ≤ √↑N / Real.log ↑N ^ B → ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Zlow) + (goldbachWeightHighFirstCoefficient ε - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) - goldbachG11BuchstabSieveEnvelope N Z A C ρ η ≤ 4 * ↑(D19 N)

Actual D19 consumer: no prime-output count or unnormalized X remains in the negative G11 envelope. The finite prime-label sum and other signed terms remain.