theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight_global_upper (r : ℝ) : goldbachG11AuthorWeight r ≤ 8

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeKernel_author_add (N : ℕ) (t : ℝ) : goldbachG11PrimeKernel (fun (r : ℝ) => goldbachG11AuthorWeight r + t) N = goldbachG11PrimeKernel goldbachG11AuthorWeight N + t * goldbachG11PrimeKernel (fun (x : ℝ) => 1) N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Author_divisor_tail_paid (H d : ℝ) (hd : 0 < d) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 16800 * H * Real.log ↑N / ↑N ^ (4 / 53) ≤ d

Pay the already counted ambient-prime-divisor tail on the normalized mother scale. Reuses the same logarithm/power estimate as the frozen payments.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Author_choose_loss (C δ : ℝ) (hδ : 0 < δ) : ∃ (t : ℝ), 0 < t ∧ t ≤ 1 / 8 ∧ (1 + t) ^ 2 * (561522 / 1000000 + t) * (goldbachG11PrimeIntegral goldbachG11AuthorWeight + (|goldbachG11PrimeIntegral fun (x : ℝ) => 1| + 2) * t) + 9 * C * t + 3 * t < 561522 / 1000000 * goldbachG11PrimeIntegral goldbachG11AuthorWeight + δ

Choose one strictly positive common loss. The three t terms cover the new divisor tail, actual distribution error, and original G11 exceptional loss.