theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPrime_ne_rpow_of_not_dvd (N r a b : ℕ) (hr : Nat.Prime r) (hrN : ¬r ∣ N) (hb : 0 < b) : ↑r ≠ ↑N ^ (↑a / ↑b)

A prime at an exact nonnegative rational-power endpoint must divide N. Thus it is absent from the Goldbach sifting prime carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes_eq_halfOpen_rpow (N a b : ℕ) (z : ℝ) (hb : 0 < b) : goldbachClosedPrimes N z (↑N ^ (↑a / ↑b)) = goldbachHalfOpenPrimes N z (↑N ^ (↑a / ↑b))

Closed and half-open prime carriers agree at these rational-power endpoints; there is no extra endpoint error to absorb.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3Closed_eq_halfOpen_rpow (A : Finset ℕ) (N a b : ℕ) (z : ℝ) (hb : 0 < b) : goldbachS3Closed A N z (↑N ^ (↑a / ↑b)) = goldbachS3HalfOpen A N z (↑N ^ (↑a / ↑b))