theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_actual_weighted_euler_eventually {e : ℝ} (he : 0 < e) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ (k : ℕ × ℕ × ℕ), (fouvryG9GridCell N e ρ k).Nonempty → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p ∧ 2 < p) → fouvryG9RectangleEulerMass N ρ k P ≤ LiLiuPrereqWF.g9BaseEuler P * (1 + 1 / (↑N ^ (4 / 53) / 2 - 2)) ^ 3 * fouvryG9RectangleMass N ρ k

The true eventual actual-cell Euler bound. The positive product window is fixed before N0; no extra third-prime witness remains as an input.