theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFloorKey_phase_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} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) : have v := wGCDTuple (wExtractedOriginal t.1); |↑t.2| * (|M * y| / (↑K.D * ↑v.k₁ * ↑t.1.1.2.1 * ↑t.1.1.2.2) + |↑a| / (↑v.n₁ * ↑v.k₁ * ↑t.1.1.2.1 * ↑t.1.1.2.2 * ↑K.D')) ≤ (3 + 4 * Cscale) * Z