theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedIntegral_envelope_loss (B C τ η ν d W : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hη : 0 < η) (hν : 0 < ν) (hd : 0 < d) (hW0 : 0 ≤ W) (hW : ∀ u ∈ Set.Icc 3 (1141 / 132), LiLiuPrereqBuchstab.buchstab u ≤ W) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → goldbachG12BuchstabSieveEnvelope N (goldbachG11SieveCutoff B N) 3 C (τ * Real.exp Real.eulerMascheroniConstant) η ≤ (8 * (1 + τ) ^ 3 * (W + η) * ((goldbachG12PrimeIntegral fun (x : ℝ) => 1) + ν) + 3 * d) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Exact envelope: exponent A=3; the three actual remainders are paid separately. The coefficient is the uniform level coefficient 8, not the author's low-band weight.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedIntegral_choose_loss (W δ : ℝ) (hδ : 0 < δ) : ∃ (t : ℝ), 0 < t ∧ t ≤ 1 ∧ 8 * (1 + t) ^ 3 * (W + t) * ((goldbachG12PrimeIntegral fun (x : ℝ) => 1) + t) < (8 * W * goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ

Continuity selects one strictly positive common loss; no free mesh, distribution, or target-shaped premise is left in the final consumers.