theorem MathlibNt.SieveTheory.LiLiuPrereqWF.g9WF_external_family_at_level {δ η : ℝ} (hδ : 0 ≤ δ) (hδu : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) : ∃ (N₀ : ℝ), ∀ (N T : ℝ), N₀ ≤ N → 1 ≤ T → T ≤ N ^ (1 / 10) → ∀ (upper : Bool) (P : Finset ℕ) (z : ℝ), have Q := N ^ (5 / 9 - δ) / T ^ (5 / 9); have D := externalInternalLevel Q η; ↑(externalTags upper P D η z).card < Real.exp (8 * η⁻¹ ^ 3) ∧ ∀ t ∈ externalTags upper P D η z, AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (n : ℕ) => (externalTerm upper P D η z t) n

A genuine common external family at each original G9 level, with all coefficients supplied by the accepted normalized sieve producer.