The zero mode of the large beta-gcd exclusion

The bound applies to every further submask of gcd(n₁,n₂)>Y. It is an absolute zero-mode bound, not a restriction of the signed unmasked Siegel--Walfisz cancellation. The original progression sum and the other four gcd exclusions still require separate estimates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_eq_modulus_sum (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) : wMaskedZeroMode M N Q β c a P = M * dyadicCutoffMass * ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, c q * c r / ↑(q.lcm r) * ∑ p ∈ N ×ˢ N, if WCompatible q r p.1 p.2 ∧ P ((q, r), p) then β p.1 * β p.2 else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.masked_beta_pair_abs_le_largeGCD (N Q : Finset ℕ) (β : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (Y : ℝ) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) {q r : ℕ} (hq : q ∈ reducedModuli Q a) (hr : r ∈ reducedModuli Q a) : |∑ p ∈ N ×ˢ N, if WCompatible q r p.1 p.2 ∧ P ((q, r), p) then β p.1 * β p.2 else 0| ≤ ∑ p ∈ largeGCDPairs N Y, |β p.1 * β p.2|

Discarding compatibility or imposing further masks only enlarges the absolute beta-pair majorant, so the large-gcd gain survives every submask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedZeroMode_abs_le_largeGCD {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {T L Y : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (hY : 0 < Y) (M : ℝ) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (P : WOriginalTuple → Prop) (hP : ∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) : |wMaskedZeroMode M N Q β c a P| ≤ |M * dyadicCutoffMass| * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y)) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

Uniform inverse-square-root saving for the actual zero mode under any submask of a large beta gcd. Both coefficient signs are retained.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wLargeBetaGCDZeroMode_abs_le {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {T L Y : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (hY : 0 < Y) (M : ℝ) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : |wMaskedZeroMode M N Q β c a fun (t : WOriginalTuple) => Y < ↑(t.2.1.gcd t.2.2)| ≤ |M * dyadicCutoffMass| * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y)) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

Direct specialization to the first exclusion d=gcd(N₁,N₂)>Y.