theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Rectangle_upper_transport (N : ℕ) (U V P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hPN : ∀ p ∈ P, p.Coprime N) {Q θ z H : ℝ} (hQ : 0 ≤ Q) (hD : 2 ≤ LiLiuPrereqWF.externalInternalLevel Q θ) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) (hH : 0 ≤ H) (hr : ∀ d ∈ Finset.Icc 1 ⌊Q⌋₊, |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy 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| ≤ H / ↑d.totient) : have D := LiLiuPrereqWF.externalInternalLevel Q θ; 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, goldbachG11RectangleWeight N (m, p) * LiLiuPrereqWF.externalDensity true P D θ z (LiLiuPrereqWF.progressionDensity (m * p)) + ∑ t ∈ LiLiuPrereqWF.externalTags true P D θ z, |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError U V (Finset.Ioc 0 ⌊Q⌋₊) α β (fun (d : ℕ) => (LiLiuPrereqWF.externalTerm true P D θ z t) d) ↑N| + ↑(LiLiuPrereqWF.externalTags true P D θ z).card * H * (4 / D ^ θ ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2

Finite transport for the literal G11 rectangle. The arbitrary-modulus majorant is exposed here and supplied by the actual grid producer downstream.