theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_active_product_bounds {N r : ℕ} {ε : ℝ} {u : GoldbachG11SwitchedBody} (hN : 2 ≤ N) (hu : u ∈ goldbachG11SwitchedBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hr : r ∈ goldbachG11FirstPrimeFiber N ε (↑N ^ (4 / 53)) u) : ε * ↑N ^ (29 / 33) < ↑(goldbachG11SwitchedBodyProd u) ∧ ↑(goldbachG11SwitchedBodyProd u) < ↑N ^ (49 / 53)

Bounds for an actually inhabited first-prime fibre, not for the entire mother support.