theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock_parameter_budget_kscale {Cscale M T x Z y : ℝ} (hC : 1 ≤ Cscale) (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) (hy : y ∈ Set.Icc (1 / 2) 3) {N Q : Finset ℕ} (hN : ∀ n ∈ N, T ≤ ↑n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} (ha : |↑a| ≤ Cscale * x) {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) j positive) : |wBlockPhaseA K j positive (M * y)| + |wBlockPhaseB K j positive a| ≤ 112 * (Cscale * Z)