theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKMain_loss_le (Cscale κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff : ℝ) (hscale : 1 ≤ Cscale) {x : ℝ} (hx : 1 ≤ x) (hκ : 0 ≤ κ) (hδ : 0 < δ) (hC : 0 ≤ Cnonzero) (hCa : 0 ≤ Ca) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (ha : ↑a.natAbs ≤ Cscale * x) (hd : ↑K.1.2.1 ≤ x) (hF : ↑F ≤ 2 * x) (hn : 2 ^ j 2 ≤ 2 * x) (hr : 2 ^ j 3 ≤ x) (hs : 2 ^ j 4 ≤ x) (hH : 2 ^ j 0 ≤ 32 * x ^ 7) : directPayMainLoss κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a K F j ≤ directPayMainLossConstant κ δ Cnonzero Cτ Cjoint Ca Ccoeff * Cscale ^ (2 * δ) * x ^ (4 * ρ + 14 * δ + 4 * κ)

Two and only two arithmetic powers of the fixed multiplier are charged.