theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleError_total (j A : ℕ) {e ε δ ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ ≤ 1 / 2) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (c : ℕ × ℕ × ℕ → ℕ → ℝ), (∀ k ∈ fouvryG9GridUsed N e ρ, AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) (c k)) → ∑ k ∈ fouvryG9GridUsed N e ρ, |fouvryG9RectangleError N ρ δ k (c k)| ≤ ↑N / Real.log ↑N ^ A

Total absolute distribution error of the genuine positive G9 rectangular majorant. Every cell may use its own original-level well-factorable weight. There is no assumed per-cell error estimate: expanded C2 supplies it.