theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedIntegral_envelope (W δ : ℝ) (hW0 : 0 ≤ W) (hδ : 0 < δ) (hW : ∀ u ∈ Set.Icc 3 (1141 / 132), LiLiuPrereqBuchstab.buchstab u ≤ W) : ∃ (τ : ℝ), 0 < τ ∧ τ ≤ 1 ∧ ∀ (B C : ℝ), 0 ≤ B → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → goldbachG12BuchstabSieveEnvelope N (goldbachG11SieveCutoff B N) 3 C (τ * Real.exp Real.eulerMascheroniConstant) τ ≤ ((8 * W * goldbachG12PrimeIntegral 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.goldbachG12OutputTotal_le_normalizedIntegral (W δ : ℝ) (hW0 : 0 ≤ W) (hδ : 0 < δ) (hW : ∀ u ∈ Set.Icc 3 (1141 / 132), LiLiuPrereqBuchstab.buchstab u ≤ W) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ ((8 * W * goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual original-cross output upper bound, with its complete sieve error paid.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12OutputTotal_le_uniformIntegral (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ ((8 * (564383 / 1000000) * goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Unconditional uniform-level bound, using the certified unbounded Buchstab majorant. This is not the author's low/high weighted coefficient.