theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4Pairs_eq_empty_of_cube_bound (N : ℕ) (u : ℝ) (hu : 0 ≤ u) (hcut : ↑N ≤ u ^ 3) : goldbachS4Pairs N u = ∅

Above the cube boundary the literal S4 pair carrier is empty, including its closed endpoint: equality would force a specified prime to divide N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_cube_cutoff_eq_zero (A : Finset ℕ) (N : ℕ) : goldbachS4 A N (↑N ^ (1 / 3)) = 0

The actual S4 count vanishes at the real cube-root cutoff.