Large-D genuine F/f density for the actual geometric rough carrier

The threshold is chosen before the cutoff, prime set, density, and product constant. The moving range follows from z ≥ D^(ε²) and an explicit power budget. When z < D^(ε²), the actual rough carrier is empty instead.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.coarseCoordinate_sqrt_bounds {D z : ℝ} (hD : 2 ≤ D) (hz : 2 ≤ z) (hzD : z ≤ √D) : z ≤ D ∧ 2 ≤ Real.log D / Real.log z

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.coarse_rounded_power_budget {D ε z : ℝ} (hD : 2 ≤ D) (hε : 0 < ε) (hz : 1 < z) (huz : D ^ ε ^ 2 ≤ z) (hlarge : (2 / ε ^ 2) ^ 13 ≤ Real.log D) : SmallRosser.roundedSieveCoordinate D z ^ 13 ≤ Real.log ↑⌈D⌉₊

No dependence on the carrier or K occurs in this rounded moving-range budget. The power 13 is the actual source/envelope budget, not a fixed-s substitute.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.roughOrdinaryDensity_empty (upper : Bool) {D : ℝ} (hD : 1 < D) (g : ℕ → ℝ) : roughOrdinaryDensity upper D ∅ g = 1

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

Genuine F/f density of the SAME ordinary coefficient appearing in the finite signed-family comparison. The absolute constant precedes ε; the large-D threshold precedes all prime sets, densities, cutoffs, and K. The original product constant and unrounded log D / log z are retained.