theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAPWindow_eq_sdiff {N m : ℕ} {ε : ℝ} (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ goldbachG12ActiveProductSupport N) : goldbachG11LinkedAPWindow N ε m d b = Wu2004MeanValue.scaledPrimeSet (↑m * goldbachG11PiLiHi N m) d b m \ Wu2004MeanValue.scaledPrimeSet (↑m * goldbachG11PiLiLo N ε m) d b m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAPWindow_card_eq_inverse {N m : ℕ} {ε : ℝ} (d b : ℕ) (hN : 2 ≤ N) (hm : m ∈ goldbachG12ActiveProductSupport N) (hmd : m.Coprime d) : ↑(goldbachG11LinkedAPWindow N ε m d b).card = ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊goldbachG11PiLiHi N m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d)) - ↑(AnalyticNumberTheory.Sieve.primesInAP ⌊goldbachG11PiLiLo N ε m⌋₊ d (AnalyticNumberTheory.Sieve.natInvMod d m * b % d))

Exact count difference, retaining the closed high endpoint and inverse residue.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedPrimeWindow_product_le {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport N) (hr : r ∈ goldbachG11LinkedPrimeWindow N ε m) : r * m ≤ N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedPrimeWindow_output_pos {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport N) (hr : r ∈ goldbachG11LinkedPrimeWindow N ε m) : 0 < N - r * m

On the geometric mother, the actual output is positive, not truncated to zero.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAPWindow_eq_output_dvd {N m : ℕ} {ε : ℝ} (d : ℕ) (hm : m ∈ goldbachG12ActiveProductSupport N) : goldbachG11LinkedAPWindow N ε m d N = {r ∈ goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}

The progression counted by the source is literally divisibility of the output.