theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11WeightedGridMass_le_paidKernel : ∃ (C : ℝ), 0 < C ∧ ∀ (η : ℝ), 0 < η → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ (h : ℝ → ℝ) (H : ℝ), 0 ≤ H → (∀ (r : ℝ), 0 ≤ h r) → (∀ (r : ℝ), h r ≤ H) → Real.log ↑N / ↑N * goldbachG11WeightedGridMass N ε ρ h ≤ ρ ^ 2 * (561522 / 1000000 + η) * goldbachG11PrimeKernel h N + C * H * (ρ - 1) + 16800 * H * Real.log ↑N / ↑N ^ (4 / 53)

All actual grid extensions are now paid: ordered rough mother, ordering collar and newly admitted ambient prime divisors. The threshold precedes all changing epsilon, rho and bounded nonnegative weights.