theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_total_prefix_cost_c2 (i k m : ℕ) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (hη1 : η ≤ 1) (hηε : η < ε) (hbudget : 416 * η ≤ ε / 4) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M ν : ℝ), 1 ≤ M → ε ≤ ν → ν ≤ 1 / 10 → x = 4 * M * x ^ ν → ∀ (N : Finset ℕ), (∀ n ∈ N, x ^ ν ≤ ↑n ∧ ↑n ≤ 2 * x ^ ν) → ∀ (U : Finset ℕ) (α : ℕ → ℝ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∀ K ∈ wExtractedKeyBox (x ^ η), ∀ (b : ℕ) (β γ ζ : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) → have L := x ^ ((5 - 5 * ν) / 9 - ε); have V := wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊L⌋₊) a (c2FiveSmallMask x η) (x ^ c2RExponent ν ε) (x ^ c2SExponent ν ε) (highOmegaCutoff x) b K; (3072 * M * ∑ n ∈ U, α n ^ 2) * ↑(Nat.log 2 ⌈L ^ 2 / M * x ^ η⌉₊ + 1) * (x ^ η) ^ 7 * wAnalyticVariationConstant (x ^ η) * wAnalyticKeyPrefixMajorant V K (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a ≤ C * x ^ 2 * x ^ (-(ε / 4))

The full actual retained contribution, including alpha, shell count, keys, variation, coprime partition and five dyadic coordinates.