The common well-factorable linear sieve at the prescribed external level

The same explicit families cover the full domain 2 <= z <= sqrt Q. All constants and thresholds precede the density data and the original K. The zero lower edge uses the proved O(epsilon) bound for the genuine f; the truncated upper edge uses its own proved Euler-normalized density.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_externalFamilyDensity_ff : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (z : ℝ), 2 ≤ z → z ≤ √Q → (∀ p ∈ P, ↑p < z) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → have D := externalInternalLevel Q ε; have V := ∏ p ∈ P, (1 - ω p / ↑p); have E := C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); 4 ≤ D ∧ V * (JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log Q / Real.log z) - E) ≤ externalDensity false P D ε z (SmallRosser.primeDensity ω) ∧ externalDensity true P D ε z (SmallRosser.primeDensity ω) ≤ V * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log z) + E)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_external_sieve_common_family {ι : Type u_1} : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (z : ℝ), 2 ≤ z → z ≤ √Q → (∀ p ∈ P, ↑p < z) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → have D := externalInternalLevel Q ε; have V := ∏ p ∈ P, (1 - ω p / ↑p); have E := C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (∀ (upper : Bool), ↑(externalTags upper P D ε z).card < Real.exp (8 * ε⁻¹ ^ 3) ∧ ∀ t ∈ externalTags upper P D ε z, WellFactorable (externalTerm upper P D ε z t) Q) ∧ ∀ (I : Finset ι) (a : ι → ℕ) (X : ℝ), 0 ≤ X → X * V * (JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log Q / Real.log z) - E) + externalRemainder false P D ε z I a X (SmallRosser.primeDensity ω) ≤ sequenceSifted I a P ∧ sequenceSifted I a P ≤ X * V * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log z) + E) + externalRemainder true P D ε z I a X (SmallRosser.primeDensity ω)

One fixed, constructed family, its genuine F/f main terms, original signed divisor remainders, source cardinality and all real level splits.