Fixed-residue-scale power payment for a large supported beta factor

Here T is the upper beta endpoint. The sparse square-divisor envelope saves x ^ (-η / 4) before paying the divisor loss and logarithms. The original sum and zero mode retain the same arbitrary mask, and neither length requires a positive power lower bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_wMaskedOriginal_zero_largeSupport_power_saving_kscale {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {η Cscale : ℝ} (hη : 0 < η) (hCscale : 1 ≤ Cscale) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℝ), 1 ≤ M → 1 ≤ T → M * T ≤ x → ∀ (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 ^ η < ↑(wGCDData t.1.1 t.1.2 t.2.1 t.2.2).d₁) → |wMaskedOriginal M N Q β c a P| + |wMaskedZeroMode M N Q β c a P| ≤ 2 * M * T ^ 2 * x ^ (-η / 8)

Uniform power saving for the original and zero-mode terms on every submask of the large canonical d₁ condition. The threshold precedes all changing data; nondivisibility is later supplied by betaClean.