theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9_third_prime_eventually_large {e : ℝ} (he : 0 < e) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ y ∈ fouvryG9Carrier N e, ↑N ^ (1 / 3) ≤ ↑(y.1 / y.2.1)

Fixed positive product windows force a large third prime eventually. The threshold depends on e; nonemptiness alone at finite N does not suffice.