theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_natAbs_support {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) {v : ℕ × ℕ} (hv : v ∈ goldbachG11GridLong N ε ρ k ×ˢ goldbachG11GridShort N ρ k) : (↑N - ↑v.1 * ↑v.2).natAbs ≤ 4 * N

The natural absolute difference retains overhanging and zero outputs.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_remainder_majorant {κ : ℝ} (hκ : 0 < κ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 1 ≤ N → ∀ (ε ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → 4 ≤ ↑N ^ (4 / 53) → ∀ k ∈ goldbachG11GridUsed N ε ρ, ∀ (d : ℕ), 0 < d → d ≤ N → |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) (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) (↑N) d| ≤ C * ↑N ^ (1 + κ) / ↑d.totient

A literal modulus-by-modulus remainder majorant on every occupied G11 rectangle. The imported finite-fibre lemma supplies the mass and centre bounds.