Full zero-mode estimate with the lcm weight retained

The all-positive-modulus beta-AP input in F87 (1.3) is applied at the actual gcd, without a small/large gcd split. A fixed-order divisor majorant and the harmonic lcm mean pay all modulus weights. This estimates the full unpruned W zero mode minus U zero mode, not the nonzero Fourier remainder.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.one_le_fouvryTau_succ (κ : ℕ) {q : ℕ} (hq : q ≠ 0) : 1 ≤ (fouvryTau (κ + 1)) q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_lcm_weight_mul_quotient_tau_le_log (j κ : ℕ) {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) : ∑ q ∈ Q, ∑ r ∈ Q, |c q * c r / ↑(q.lcm r)| * ↑((fouvryTau κ) (q / q.gcd r)) ≤ (1 + Real.log L) ^ (2 * (j * (κ + 1)) ^ 2 + 1)

The extra sieve-order weight costs only a fixed logarithmic power. The successor majorant is essential at order zero, where tau_0 itself need not be at least one. No gcd is replaced by a cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain_sub_smoothUMain_abs_le_coprimeAP_lcm {k : ℕ} (hk : 1 ≤ k) (j κ : ℕ) {T L E : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (hE : 0 ≤ E) (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 : ℤ) (hAP : ∀ q ∈ Q, ∀ (δ : ℕ), δ ∣ q → 0 < δ → ∀ b ∈ betaReducedResidues δ, |betaCoprimeAPDiscrepancy N β δ (q / δ) b| ≤ E * ↑((fouvryTau κ) (q / δ))) : |smoothWMain M N Q β c a - smoothUMain M N Q β c a| ≤ 2 * |M * dyadicCutoffMass| * E * (T * (1 + Real.log T) ^ (k - 1)) * (1 + Real.log L) ^ (2 * (j * (κ + 1)) ^ 2 + 1)

An independent AP bound, applied at every divisor of the given moduli, pays the entire signed covariance sum. In particular no intermediate-gcd error is left in this estimate.