theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RemainderMajorant_actual {κ : ℝ} (hκ : 0 < κ) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 1 ≤ N → ∀ (e ρ : ℝ), 0 < e → 1 < ρ → ρ ≤ 5 / 4 → ∀ (k : ℕ × ℕ × ℕ), (fouvryG9GridCell N e ρ k).Nonempty → 3 ≤ ρ ^ k.1 → ∀ (d : ℕ), 0 < d → d ≤ N → |AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.bilinearDiscrepancy (fouvryG9LongProducts N ρ k) (fouvryG9RectanglePrimeSupport N ρ k) (fouvryG9LongAlpha N ρ k) (fouvryG9RectangleBeta N) (↑N) d| ≤ C * ↑N ^ (1 + κ) / ↑d.totient

Uniform inverse-totient majorant for the actual G9 remainder. The positive constant is selected before N, the grid, the cell and the modulus. The only assumptions are the stated geometric conditions and 0 < d ≤ N.