theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachB8LogGridMajorant (n : ℕ) (hn : 0 < n) : Filter.Tendsto (goldbachB8LogGridMajorant n) Filter.atTop (nhds (goldbachB8LogGridUpperSum n))

The mesh is fixed before the prime-size limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PairLogKernel_le_gridUpperSum_eventually (n : ℕ) (hn : 0 < n) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB8PairLogKernel N ≤ goldbachB8LogGridUpperSum n + η

Actual finite kernel bounded by the fixed-mesh limit, with the prime-size threshold after the mesh and tolerance. No mesh-to-integral limit is assumed.