Payment of the unchanged arithmetic weight at a fixed enlarged shift scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKSecondary_weight_paid {Cscale κ δ ρ C Csec Ccoeff : ℝ} (hscale : 1 ≤ Cscale) (hκ : 0 ≤ κ) (hδ : 0 < δ) (hC : 0 ≤ C) (hCsec : 0 ≤ Csec) : ∃ (Cw : ℝ), 0 < Cw ∧ ∀ (x : ℝ), 1 ≤ x → ∀ (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ), |↑a| ≤ Cscale * x → 2 ^ j 0 ≤ 8 * x ^ 6 → ↑(wGramSecondaryNumeratorMax a K F j) ≤ 16 * Cscale * x ^ 9 → 16 * 2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4 ≤ 16 * x ^ 4 → directPaySecondaryWeight κ δ ρ C Csec Ccoeff x a K F j ≤ Cw * x ^ (4 * ρ + 4 * κ + 11 * δ)

Both scale losses are fixed constants, not additional powers of x.