theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedIntegral_envelope (W δ : ℝ) (hW0 : 0 ≤ W) (hδ : 0 < δ) (hW : ∀ u ∈ Set.Icc (17 / 4) (37 / 4), LiLiuPrereqBuchstab.buchstab u ≤ W) : ∃ (τ : ℝ), 0 < τ ∧ τ ≤ 1 ∧ ∀ (B C : ℝ), 0 ≤ B → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → goldbachG11BuchstabSieveEnvelope N (goldbachG11SieveCutoff B N) 3 C (τ * Real.exp Real.eulerMascheroniConstant) τ ≤ ((8 * W * goldbachG11PrimeIntegral fun (x : ℝ) => 1) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The loss is selected before all later sieve constants. It is not an assumption on the target bound; all analytic error terms are absorbed for every fixed B,C.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_normalizedIntegral (W δ : ℝ) (hW0 : 0 ≤ W) (hδ : 0 < δ) (hW : ∀ u ∈ Set.Icc (17 / 4) (37 / 4), LiLiuPrereqBuchstab.buchstab u ≤ W) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ ((8 * W * goldbachG11PrimeIntegral fun (x : ℝ) => 1) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual G11, uniform in every nonnegative window epsilon. The only optional input is a scalar raw Buchstab majorant on [17/4,37/4].

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

Unconditional W=1 closure. This is not the paper's sharper low-band bound and makes no assertion about final D19 positivity.