The actual retained coprime cell, with all three energies and their normalizations produced internally. No cancellation/envelope hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_retained_cell_c2 (k m : ℕ) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (hη1 : η ≤ 1) (hηε : η < ε) (hbudget : 400 * η ≤ ε / 4) : ∃ (C : ℝ), 0 < C ∧ ∀ (x M ν : ℝ), 4 ≤ x → 1 ≤ M → ε ≤ ν → ν ≤ 1 / 10 → x = 4 * M * x ^ ν → ∀ (N : Finset ℕ), (∀ n ∈ N, x ^ ν ≤ ↑n ∧ ↑n ≤ 2 * x ^ ν) → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → ∀ K ∈ wExtractedKeyBox (x ^ η), ∀ (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β γ ζ : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) → (wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊x ^ c2RExponent ν ε * x ^ c2SExponent ν ε⌋₊) a (c2FiveSmallMask x η) (x ^ c2RExponent ν ε) (x ^ c2SExponent ν ε) (highOmegaCutoff x) b K) j positive).Nonempty → wBlockAmplitude K j * ‖∑ t ∈ wCoprimeFiber x N (x ^ c2SExponent ν ε) (wGramPrefix N a x η (x ^ c2RExponent ν ε) (x ^ c2SExponent ν ε) M (x ^ η) K b j cap positive) c, ↑(wExtractedCoefficient (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1‖ ≤ C * (x ^ ν) ^ 2 * x ^ (-(ε / 2))