theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_Fouvry_externalFamily_rectangle (A : ℕ) {Cscale η θ : ℝ} (hCscale : 1 ≤ Cscale) (hη : 0 < η) (hθ : 0 < θ) (hθu : θ < 1 / 8) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval) (M ν : ℝ), 1 ≤ M → 4 * M * z.scale = x → η ≤ ν → ν ≤ 1 / 10 + η / 10 → z.scale = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (P : Finset ℕ) (y : ℝ), 2 ≤ LiLiuPrereqWF.externalInternalLevel (x ^ ((5 - 5 * ν) / 9 - η)) θ → ∑ t ∈ LiLiuPrereqWF.externalTags true P (LiLiuPrereqWF.externalInternalLevel (x ^ ((5 - 5 * ν) / 9 - η)) θ) θ y, |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U (AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval z.lower z.upper) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - η)⌋₊) (fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (p : ℕ) => if p.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p else 0) (fun (d : ℕ) => (LiLiuPrereqWF.externalTerm true P (LiLiuPrereqWF.externalInternalLevel (x ^ ((5 - 5 * ν) / 9 - η)) θ) θ y t) d) ↑N| ≤ x / Real.log x ^ A

Each original external-family member is supplied internally, and the whole finite family is paid. This is one rectangle, not the full moving-region sum.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_Fouvry_internalLevel_eventually (D₀ : ℝ) (hD₀ : 0 ≤ D₀) {η θ : ℝ} (hηu : η < 1 / 8) (hθ : 0 < θ) (hθu : θ < 1 / 8) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ ν ≤ 1 / 10 + η / 10, D₀ ≤ LiLiuPrereqWF.externalInternalLevel (x ^ ((5 - 5 * ν) / 9 - η)) θ

Uniform growth of the unchanged internal level, before all moving short exponents.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_Fouvry_externalFamily_rectangle_paid (A : ℕ) {Cscale η θ : ℝ} (hCscale : 1 ≤ Cscale) (hη : 0 < η) (hηu : η < 1 / 8) (hθ : 0 < θ) (hθu : θ < 1 / 8) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval) (M ν : ℝ), 1 ≤ M → 4 * M * z.scale = x → η ≤ ν → ν ≤ 1 / 10 + η / 10 → z.scale = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → ∀ (U : Finset ℕ), (∀ m ∈ U, M ≤ ↑m ∧ ↑m ≤ 2 * M) → ∀ (P : Finset ℕ) (y : ℝ), ∑ t ∈ LiLiuPrereqWF.externalTags true P (LiLiuPrereqWF.externalInternalLevel (x ^ ((5 - 5 * ν) / 9 - η)) θ) θ y, |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U (AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval z.lower z.upper) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - η)⌋₊) (fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (p : ℕ) => if p.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p else 0) (fun (d : ℕ) => (LiLiuPrereqWF.externalTerm true P (LiLiuPrereqWF.externalInternalLevel (x ^ ((5 - 5 * ν) / 9 - η)) θ) θ y t) d) ↑N| ≤ x / Real.log x ^ A

Fully supplied external-family discrepancy on one actual G11 rectangle. No coefficient, SW, WF-member, cardinality or internal-level premise remains.