theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Prod_le_rpow_half_and_lt_two_thirds {N : ℕ} {b γ : ℝ} {rs : ℕ × ℕ} (hN : 2 ≤ N) (hγ : γ < 1 / 3) (hrs : rs ∈ goldbachC10Pairs N b (↑N ^ γ)) : ↑(goldbachC10Prod rs) ≤ ↑N ^ ((1 + γ) / 2) ∧ ↑N ^ ((1 + γ) / 2) < ↑N ^ (2 / 3)

The actual product support of C10, with no fixed gap imposed below gamma=1/3.