theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_le_analyticMain : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 1 < K ∧ ∀ (A : ℕ) (ε ρ δ θ : ℝ), 0 < ε → ε ≤ 1 → 1 < ρ → ρ ≤ 5 / 4 → 0 < δ → δ < 1 / 4 → 0 < θ → θ < 1 / 8 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ goldbachG11GridAnalyticMain N ε ρ δ θ C K + 5 * ↑N / Real.log ↑N ^ A

Both original-count distribution branches and their evaluated arithmetic main terms. The remaining task is weighted prime-box/Buchstab aggregation.