Genuine upper density at the external near-two edge

The family is the accepted upper family on primes strictly below sqrt D. For large dimension constants its bounded aggregate replaces, rather than inflates, the internal analytic estimate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.EdgeDensity.exists_signedFamilyDensity_upper_edge : ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 / 8 → ∃ (D₀ : ℝ), 4 ≤ D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → ∀ (ω : ArithmeticFunction ℝ), ω.IsMultiplicative → (∀ p ∈ P, 0 ≤ ω p / ↑p ∧ ω p / ↑p < 1) → ∀ (K : ℝ), 0 ≤ K → SmallRosser.DimensionOneProductBound P (⇑(SmallRosser.primeDensity ω)) K → ∀ (z : ℝ), √D < z → z ≤ √(D ^ (1 + ε + ε ^ 9)) → (∀ p ∈ P, ↑p < z) → signedFamilyDensity true ({p ∈ P | ↑p < √D}) D ε (geometricSieveLabel D ε) (SmallRosser.primeDensity ω) ≤ (∏ p ∈ P, (1 - ω p / ↑p)) * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log (D ^ (1 + ε + ε ^ 9)) / Real.log z) + C * (ε + (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log D ^ (-(1 / 3))))

The absolute constant is chosen before epsilon; the threshold precedes the prime carrier, multiplicative density, original dimension constant and external cutoff. The weights are exactly the already accepted family.