The common well-factorable sieve on the internal level domain

The explicitly defined family is independent of the sequence and of every factorization. Its actual cardinality, order-one well-factorability, genuine F/f main terms, and actual signed remainders occur together below.

The range is z ≤ sqrt D, while the weight level is Q = D^(1+epsilon+epsilon^9). This is not the missing extension to z ≤ sqrt Q. The remainder here is restricted to primorial divisors; full-modulus use still requires the previously proved transport and its costs.

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

A constructed, bounded-size, common WF family with its own analytic density and finite sieve bounds. Repeated values and zero sequence entries are allowed; no distribution estimate is assumed.