Power payment for the same large-common-modulus mask

Here T is the upper beta endpoint. The saving depends on a positive lower power bound for both lengths, not just on the common-modulus threshold. The original progression sum and its zero mode keep exactly the same mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_wMaskedOriginal_zero_largeDelta_power_saving_kscale {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {ρ η Cscale : ℝ} (hρ : 0 < ρ) (hρη : ρ ≤ η) (hCscale : 1 ≤ Cscale) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℝ), 1 ≤ M → 1 ≤ T → M * T ≤ x → x ^ ρ ≤ M → x ^ ρ ≤ T → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ 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 → x ^ η < ↑(t.1.1.gcd t.1.2)) → |wMaskedOriginal M N Q β c a P| + |wMaskedZeroMode M N Q β c a P| ≤ 2 * M * T ^ 2 * x ^ (-ρ / 2)

The original and zero-mode terms are paid together on an arbitrary submask of the large common-modulus condition. The threshold is uniform in all changing data. The positive beta order is removed in the dyadic API.