theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorBad_normalized_paid (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Real.log ↑N / ↑N * (67200 * ↑N / ↑N ^ (4 / 53)) ≤ δ

The normalized exceptional divisor mass vanishes independently of epsilon.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorSource_integral_budget (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), Real.log ↑N / ↑N * (400 * goldbachG12WeightedSource N ε (goldbachG12AuthorPrimeWeight N)) ≤ 564383 / 1000000 * goldbachG12PrimeIntegral goldbachG11AuthorWeight + δ

Full actual author-weighted linked source, with all product multiplicities. The threshold precedes epsilon, which remains completely arbitrary.