theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeC2_goldbach_rectangle_kscale (i j A : ℕ) {Cscale ε : ℝ} (hCscale : 1 ≤ Cscale) (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : PrimeC2Interval) (M ν : ℝ), 1 ≤ M → 4 * M * z.scale = x → ε ≤ ν → ν ≤ 1 / 10 + ε / 10 → z.scale = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → ∀ (U : Finset ℕ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → |signedError U (primeSWInterval z.lower z.upper) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊) α (fun (n : ℕ) => if n.Coprime N then primeSWBeta n else 0) c ↑N| ≤ x / Real.log x ^ A

Literal Goldbach residue and literal coprimality-filtered prime coefficient. This is a rectangular contribution, not the curved G9 region.