Actual five-coordinate counting and slow-variation costs.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_variation_le {Z : ℝ} (hZ : 1 ≤ Z) : wAnalyticVariationConstant Z ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * 113 ^ 5 * Z ^ 5

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_coordinate_bound {x L M η : ℝ} (hx : 2 ≤ x) (hL0 : 0 ≤ L) (hL : L ≤ x) (hM : 1 ≤ M) (_hη : 0 ≤ η) (hη1 : η ≤ 1) (N : Finset ℕ) (hN : ∀ n ∈ N, ↑n ≤ x) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : wAnalyticCoordinateBound (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ ≤ ⌈x ^ 4⌉₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_dyadic_card_le {x L M η : ℝ} (hx : 2 ≤ x) (hL0 : 0 ≤ L) (hL : L ≤ x) (hM : 1 ≤ M) (hη : 0 ≤ η) (hη1 : η ≤ 1) (N : Finset ℕ) (hN : ∀ n ∈ N, 0 < n) (hNX : ∀ n ∈ N, ↑n ≤ x) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) : ↑(Finset.image wAnalyticDyadicKey (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ b K)).card ≤ (2 + 4 * Real.log x / Real.log 2) ^ 5

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_log_cost_subpower (p : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 2 ≤ x → (2 + 4 * Real.log x / Real.log 2) ^ p ≤ C * x ^ δ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_analytic_prefactor_subpower {η δ : ℝ} (hη : 0 ≤ η) (hη1 : η ≤ 1) (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x L M : ℝ), 2 ≤ x → 0 ≤ L → L ≤ x → 1 ≤ M → ∀ (N : Finset ℕ), (∀ n ∈ N, 0 < n) → (∀ n ∈ N, ↑n ≤ x) → ∀ (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey), ↑(Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊ + 1) * (x ^ η) ^ 7 * wAnalyticVariationConstant (x ^ η) * ↑(Finset.image wAnalyticDyadicKey (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ b K)).card ≤ C * x ^ (12 * η + δ)

The actual shell count, five dyadic coordinates, key loss and variation are paid together, uniformly before the finite carrier and all scales.