theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_g3_scalar_le_84289 : 8 * Real.log (10 / 9) ≤ 84289 / 100000

A fixed six-term logarithm estimate, certified by an analytic remainder.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_g3_upper_84289_small_epsilon (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS2 (goldbachDifferenceCarrier N ε) N (↑N ^ (9 / 19 - ε))) ≤ (84289 / 100000 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The real S2 count retains the epsilon-dependent prime cutoff. The epsilon bound precedes epsilon, then the threshold depends on epsilon.