theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_prime_ne_lower_cutoff (N p : ℕ) (hp : Nat.Prime p) : ↑p ≠ ↑N ^ (4 / 53)

The canonical lower cutoff cannot itself be prime: its fourth-power numerator is incompatible with the prime valuation of a fifty-third power.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_prime_lower_cutoff_iff (N p : ℕ) (hp : Nat.Prime p) : ↑N ^ (4 / 53) ≤ ↑p ↔ ↑N ^ (4 / 53) < ↑p

Changing the lower prime cutoff from closed to strict costs no boundary prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductSupport_one_lt {N m : ℕ} {z b : ℝ} (hm : m ∈ goldbachG11ProductSupport N z b) : 1 < m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductSupport_not_dvd {N m : ℕ} {z b : ℝ} (hm : m ∈ goldbachG11ProductSupport N z b) : ¬m ∣ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_product_upper_cutoff_iff {N m : ℕ} {z b : ℝ} (hm : m ∈ goldbachG11ProductSupport N z b) (r : ℕ) : r * m < N ↔ r * m ≤ N

The upper product equality is also absent on the actual coprime mother support.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber_endpoint_iff {N m r : ℕ} {ε b : ℝ} (hm : m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) b) : r ∈ goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m ↔ Nat.Prime r ∧ ¬r ∣ N ∧ ↑N ^ (4 / 53) < ↑r ∧ r ≤ m.minFac ∧ ε * ↑N < ↑(r * m) ∧ r * m ≤ N ∧ Nat.Prime (N - r * m)