Same-mask zero mode for the two supported-modulus exclusions

An arbitrary further mask implying δ₁ > Y or δ₂ > Y is bounded after taking absolute values. Beta and modulus coefficients remain signed; the beta input is only its absolute mass. No Siegel--Walfisz hypothesis, mask symmetry, or restriction of unmasked cancellation is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_abs_le_modulus_pair_mass (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (F : Finset (ℕ × ℕ)) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → t.1 ∈ F) : |wMaskedZeroMode M N Q β c a P| ≤ (|M * dyadicCutoffMass| * ∑ p ∈ F, |c p.1 * c p.2 / ↑(p.1.lcm p.2)|) * (∑ n ∈ N, |β n|) ^ 2

Any finite enclosure of the masked modulus pairs pays the same-mask zero mode by its exact inverse-lcm mass times the squared absolute beta mass.

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

Uniform square-root saving for either canonical supported-modulus exclusion and every further modulus/beta-dependent submask. Constants precede all changing data; beta is arbitrary and the residue is any integer.