theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport_mem_full {N m : ℕ} (hm : m ∈ goldbachG12ActiveProductSupport N) : m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (3 / 11))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12PiLiEndpoints_bounds {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ goldbachG12ActiveProductSupport N) : ↑N ^ (4 / 53) ≤ goldbachG11PiLiLo N ε m ∧ goldbachG11PiLiLo N ε m ≤ goldbachG11PiLiHi N m ∧ goldbachG11PiLiHi N m ≤ ↑N / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductFirstPrimeFiber_linked_iff {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport 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.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductFirstPrimeFiber_eq_linkedWindow {N m : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport 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.