theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Rectangle_upper_transport (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (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 (fouvryG9LongProducts N ρ k) (fouvryG9RectanglePrimeSupport N ρ k) (fouvryG9LongAlpha N ρ k) (fouvryG9RectangleBeta N) (↑N) d| ≤ H / ↑d.totient) : have U := fouvryG9LongProducts N ρ k; have V := fouvryG9RectanglePrimeSupport N ρ k; have α := fouvryG9LongAlpha N ρ k; have β := fouvryG9RectangleBeta N; have D := LiLiuPrereqWF.externalInternalLevel Q η; fouvryG9RectangleSifted N ρ k P ≤ ∑ t ∈ LiLiuPrereqWF.externalTags true P D η z, ∑ d ∈ (P.prod id).divisors, (LiLiuPrereqWF.externalTerm true P D η z t) d * AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9IntegerFibreCenter U V α β d + ∑ 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 upper-sieve transport for the actual rectangle. The explicit local count majorant is an input to this layer, not an assumed distribution theorem.