theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleDivCount_eq (N d : ℕ) (U V : Finset ℕ) : LiLiuPrereqWF.weightedDivCount (U ×ˢ V) (fun (v : ℕ × ℕ) => (↑N - ↑v.1 * ↑v.2).natAbs) (goldbachG11RectangleWeight N) d = AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreDivisibility U V (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

The original weighted divisibility sum is literally the product-indexed integer AP count. In particular, zero and negative overhang are not truncated.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSiftedMass_external_upper (N : ℕ) (U V P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D θ z : ℝ} (hD : 2 ≤ D) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) : have α := fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m); have β := fun (p : ℕ) => if p.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta p else 0; goldbachG11RectangleSiftedMass N U V P ≤ ∑ m ∈ U, ∑ p ∈ V, α m * β p * LiLiuPrereqWF.externalDensity true P D θ z (LiLiuPrereqWF.progressionDensity (m * p)) + ∑ t ∈ LiLiuPrereqWF.externalTags true P D θ z, ∑ d ∈ (P.prod id).divisors, (LiLiuPrereqWF.externalTerm true P D θ z t) d * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy U V α β (↑N) d

The real G11 rectangular sifted count with the unchanged external family. The main term retains its exact coprime density; the remainder is still on primorial divisors, not yet the full-modulus distribution estimate.