theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RemainderMajorant_support {N : ℕ} {e ρ : ℝ} (he : 0 < e) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ × ℕ} (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) {p : ℕ × ℕ} (hp : p ∈ fouvryG9LongProducts N ρ k ×ˢ fouvryG9RectanglePrimeSupport N ρ k) : (↑N - ↑p.1 * ↑p.2).natAbs ≤ 4 * N

The actual enlarged rectangle has uniformly bounded integer differences.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RemainderMajorant_fibres {κ : ℝ} (hκ : 0 < κ) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) (U V : Finset ℕ), ∀ r ≤ 4 * N, (∑ p ∈ U ×ˢ V, if (↑N - ↑p.1 * ↑p.2).natAbs = r then fouvryG9LongAlpha N ρ k p.1 * fouvryG9RectangleBeta N p.2 else 0) ≤ 2 * C₀ * (5 * ↑N) ^ κ

Fixed-exponent uniform fiber constant, with the zero product handled by τ(0)=0.