theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_uniformScalar_numeric (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (10385101 / 100000000 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual G11 on the original difference carrier, with the cutoff uniform over all nonnegative epsilon. This consumes the proved uniform sieve factor 8 and the real Buchstab bound 561522/1000000; it is not an author-weight estimate.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_uniformScalar_numeric_fixed : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ε : ℝ), 0 ≤ ε → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ 10385101 / 100000000 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The strict rational upward rounding absorbs a positive asymptotic loss. Consequently the fixed number itself bounds the actual count eventually, with N₀ chosen before every epsilon >= 0.