theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_key_kscale (k m : ℕ) {Cscale ε η : ℝ} (hCscale : 1 ≤ Cscale) (hε : 0 < ε) (hη : 0 < η) (hη1 : η ≤ 1) (hηε : η < ε) (hbudget : 400 * η ≤ ε / 4) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M ν : ℝ), 1 ≤ M → ε ≤ ν → ν ≤ 1 / 10 + ε / 10 → x = 4 * M * x ^ ν → ∀ (N : Finset ℕ), (∀ n ∈ N, x ^ ν ≤ ↑n ∧ ↑n ≤ 2 * x ^ ν) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ Cscale * x → ∀ K ∈ wExtractedKeyBox (x ^ η), ∀ (b : ℕ) (β γ ζ : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) → have U := wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊) a (c2FiveSmallMask x η) (x ^ c2RExponent ν ε) (x ^ c2SExponent ν ε) (highOmegaCutoff x) b K; wAnalyticKeyPrefixMajorant U K (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a ≤ C * (x ^ ν) ^ 2 * x ^ (η - ε / 2) * ↑(Finset.image wAnalyticDyadicKey U).card

All actual rectangular prefixes, coprimality cells, signs and dyadic blocks. Only the explicit dyadic cardinality remains for the analytic cost producer.