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

Pay the rough-count error with the already proved continuous author kernel bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_authorSource_kernel_budget (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), Real.log ↑N / ↑N * (400 * goldbachG12WeightedSource N ε (goldbachG12AuthorPrimeWeight N)) ≤ goldbachG12PrimeKernel G12SharpWeight.weight N + δ

The full author-weighted linked source reaches the sharp kernel. The exceptional r-divides-N term is paid; no extra coprimality is assumed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_authorLowHigh_kernel_terminal (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), Real.log ↑N / ↑N * 400 * (goldbachG12AuthorLowMotherMass N ε + 8 * G12ClippedWindow.highMass N ε) ≤ goldbachG12PrimeKernel G12SharpWeight.weight N + δ

Actual low physical mother plus eight times the original UNGATED high mass. The threshold precedes all epsilon, and the target is the literal sharp step prime kernel.