theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_power_error_le_log_scale_eventually (C κ δ : ℝ) (hC : 0 ≤ C) (hκ : 0 < κ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (α : ℝ), κ ≤ α → C * ↑N ^ (1 - α) ≤ δ * ↑N / Real.log ↑N ^ 2

Uniformly absorb a fixed polynomial loss into the analytic counting scale. The threshold precedes the exponent alpha.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_twelve_switched_log_scale_eventually (ε δ : ℝ) (hε : 0 < ε) (hεu : ε < 2 / 15) (hδ : 0 < δ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (α β γ : ℝ), 1 / 18 < α → α < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → ↑(goldbachWeightTwelveSwitchedRHS (goldbachDifferenceCarrier N ε) N ε (↑N ^ α) (↑N ^ β) (↑N ^ γ) (↑N ^ (9 / 19 - ε))) - δ * ↑N / Real.log ↑N ^ 2 ≤ 4 * ↑(D19 N)

The actual switched twelve-term lower bound with arbitrary analytic-scale loss. This does not assert positivity of the labelled main expression.