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

The original fibre, with exactly the two common real endpoints. The output-prime and coprimality filters have not entered the coefficient.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow (N : ℕ) (ε : ℝ) (m : ℕ) : Finset ℕ

Geometric prime window, before imposing the output-prime condition.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m = {r ∈ Finset.range (N + 1) | Nat.Prime r ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m < ↑r ∧ ↑r ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber_eq_linkedWindow {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport N ε) : goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m = {r ∈ goldbachG11LinkedPrimeWindow N ε m | ¬r ∣ N ∧ Nat.Prime (N - r * m)}

Exact original carrier; no prime, repeated factor or endpoint was discarded.