theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9ExternalError_total (A : ℕ) {e ε δ η ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (P : ℕ × ℕ × ℕ → Finset ℕ) (z : ℕ × ℕ × ℕ → ℝ), have D := fun (k : ℕ × ℕ × ℕ) => LiLiuPrereqWF.externalInternalLevel (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) η; ∑ k ∈ fouvryG9GridUsed N e ρ, ∑ t ∈ LiLiuPrereqWF.externalTags true (P k) (D k) η (z k), |fouvryG9RectangleError N ρ δ k fun (n : ℕ) => (LiLiuPrereqWF.externalTerm true (P k) (D k) η (z k) t) n| ≤ ↑N / Real.log ↑N ^ A

Total error for the actual normalized external upper family. Both the well-factorability and the finite-family cardinality are produced internally. The prime carriers and cutoffs may vary after the common threshold.