theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_authorRough_le_kernel (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Real.log ↑N / ↑N * goldbachG12WeightedRough N (goldbachG12AuthorPrimeWeight N) ≤ goldbachG12PrimeKernel G12SharpWeight.weight N + η * goldbachG12PrimeKernel goldbachG11AuthorWeight N

The original weighted rough mother reaches the sharp step kernel. Only the vanishing rough-count error uses the continuous author kernel.