Fixed orders, including zero, pay the actual cleaned and split coefficients. Constants are chosen before every support, family, signed shift and scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_tau_subpower (k : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (n : ℕ), ↑n ≤ X → ↑((fouvryTau k) n) ≤ C * X ^ δ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_fixedOrder_envelopes (k j : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (N : Finset ℕ) (β γ ζ : ℕ → ℝ) (a : ℤ) (ξ : ℝ), (∀ n ∈ N, ↑n ≤ X) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau j) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau j) n)) → (∀ n ∈ N, |betaClean β a n| ≤ C * X ^ δ) ∧ (∀ (n : ℕ), ↑n ≤ X → |γ n| ≤ C * X ^ δ) ∧ (∀ (n : ℕ), ↑n ≤ X → |ζ n| ≤ C * X ^ δ) ∧ ∀ (n : ℕ), ↑n ≤ X → |factorConvolution γ (betaLowOmega ζ ξ) n| ≤ C * X ^ δ

This simultaneously pays beta, both original WF factors, and the actual first modulus coefficient, whose order is twice the factor order.