theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_le_fouvryTau (N m : ℕ) : |goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m| ≤ ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 1) m)

The existing literal normalized G11 coefficient supplies the order-one bound. Neither primality of the output nor a new SW assumption enters this coefficient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_normalized_Fouvry_rectangle (j A : ℕ) {Cscale η : ℝ} (hCscale : 1 ≤ Cscale) (hη : 0 < η) : ∀ᶠ (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) → ∀ (c : ℕ → ℝ), AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - η)) c → |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U (AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval z.lower z.upper) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - η)⌋₊) (goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (fun (p : ℕ) => if p.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p else 0) c ↑N| ≤ x / Real.log x ^ A

The proved prime-SW Fouvry rectangle, now instantiated with the actual G11 coefficient. The same individual signed WF member is retained on the full level.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_signedError_mul_alpha (U V Q : Finset ℕ) (α β c : ℕ → ℝ) (a : ℤ) (k : ℝ) : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U V Q (fun (m : ℕ) => k * α m) β c a = k * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U V Q α β c a

Exact scalar transport of the entire signed error; no absolute-value triangle.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_signedError_productCoefficient (N : ℕ) (U V Q : Finset ℕ) (β c : ℕ → ℝ) : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U V Q (fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) β c ↑N = 400 * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U V Q (goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) β c ↑N

All original labelled multiplicities are restored exactly.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_Fouvry_rectangle (j A : ℕ) {Cscale η : ℝ} (hCscale : 1 ≤ Cscale) (hη : 0 < η) : ∀ᶠ (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) → ∀ (c : ℕ → ℝ), AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - η)) c → |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) c ↑N| ≤ x / Real.log x ^ A

Actual unnormalized G11 rectangle discrepancy, with the factor 400 paid by one extra logarithm. The coefficient and its original multiplicities stay intact.