The actual non-squarefree support of the unmasked family

The small Rosser factor is squarefree and its prime range is disjoint from every large box. Consequently a repeated prime in a nonzero coefficient must be a rough prime. This is a statement about the original full-integer weights; no squarefree mask is applied and no preservation of well-factorability by a mask is asserted.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedSmallWeight_squarefree (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (r n : ℕ) (hn : (signedSmallWeight upper P D ε r) n ≠ 0) : Squarefree n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.separated_mul_not_small_prime_sq {B C : Finset ℕ} {f g : ArithmeticFunction ℝ} (hBC : Disjoint B C) (hg : PrimeSupported C g) (hf : ∀ (n : ℕ), f n ≠ 0 → Squarefree n) {n p : ℕ} (hn : (f * g) n ≠ 0) (hp : Nat.Prime p) (hpB : p ∈ B) : ¬p ^ 2 ∣ n

A square in the small range cannot occur in a separated convolution whose small factor is supported on squarefree integers.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_not_small_prime_sq (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (t : List ℕ) (hD : 1 ≤ D) (hε : 0 ≤ ε) {n p : ℕ} (hn : (signedFamilyTerm upper P D ε t) n ≠ 0) (hp : Nat.Prime p) (hps : p ∈ geometricSmallPrimes P D ε) : ¬p ^ 2 ∣ n

All repeated primes of a nonzero family coefficient lie above the genuine small-prime cutoff, irrespective of the tag or its parity.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_squarefree_dvd_primorial (upper : Bool) (P : Finset ℕ) (D ε : ℝ) (t : List ℕ) {n : ℕ} (hn : (signedFamilyTerm upper P D ε t) n ≠ 0) (hsf : Squarefree n) : n ∣ P.prod id

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_exceptional_support (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (t : List ℕ) (hD : 1 ≤ D) (hε : 0 ≤ ε) {n : ℕ} (hn : (signedFamilyTerm upper P D ε t) n ≠ 0) (hnot : ¬n ∣ P.prod id) : ∃ p ∈ P \ geometricSmallPrimes P D ε, Nat.Prime p ∧ D ^ ε ^ 2 ≤ ↑p ∧ p ^ 2 ∣ n

The precise exceptional support when replacing the primorial-restricted remainder by the full-modulus remainder.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedFamilyTerm_exceptional_mass_le (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (t : List ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) (ht : t ∈ signedTags upper P D ε label) (T : ℕ) : ∑ n ∈ Finset.Icc 1 T with ¬n ∣ P.prod id, |(signedFamilyTerm upper P D ε t) n| * (↑n.totient)⁻¹ ≤ 4 / D ^ ε ^ 2 * (1 + Real.log ↑T) ^ 2

Each fixed unmasked member has a small canonical density outside the primorial. The bound is uniform in the tag and uses the real rough cutoff.