theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_reciprocal_totient {N d : ℕ} (hN : 3 ≤ N) (hd : 0 < d) : 1 / ↑d.totient ≤ SieveTheory.Richert1969.richertReciprocalTotientConstant * Real.log ↑N / ↑(min d N)

The existing Mertens totient bound also pays moduli beyond the endpoint. The monotonicity step is applied to log(d)/d, not to the totient itself.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_AP_count_le {N d : ℕ} (hd : 0 < d) (b : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.range (N + 1)) (h : ℕ) : (primeSWSum S fun (n : ℕ) => n.Coprime h ∧ n ≡ b [MOD d]) ≤ ↑N / ↑d + 1

The literal progression mass is bounded by N/d+1, with no prime-density premise.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSW_large_modulus_envelope {N d : ℕ} (hN : 3 ≤ N) (hd : 0 < d) (S : Finset ℕ) (hS : S ⊆ Finset.range (N + 1)) (h b : ℕ) : |betaCoprimeAPDiscrepancy S primeSWBeta d h b| ≤ ↑N / ↑d + 1 + (↑N + 1) * (SieveTheory.Richert1969.richertReciprocalTotientConstant * Real.log ↑N / ↑(min d N))

Large-modulus envelope for the original independently sieved discrepancy. The main term is divided by phi(d), including when d exceeds the support.