Fixed-scale divisor growth on the actual nonzero progression difference. Only its arithmetic bound uses the auxiliary scale; physical M, T, x, Y and the actual tuple mask are unchanged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_modulus_support_kscale (Cscale : ℝ) (hCscale : 1 ≤ Cscale) (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (M T L x Y : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → M * T ≤ x → L ≤ x → 0 < Y → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (β c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ Cscale * x → (∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(wGCDTuple t).δ₁ ∨ Y < ↑(wGCDTuple t).δ₂) → |wMaskedOriginal M N Q β c a P| ≤ C * x ^ ε * (M * (1 + Real.log L) + L) * (∑ n ∈ N, |β n|) ^ 2 / √Y