The very-large-gcd endpoint of the actual zero-mode covariance

When the gcd exceeds the beta support endpoint, each residue class contains at most one supported integer. Centering is an orthogonal projection, so the covariance is bounded by the beta square sum without any AP hypothesis. This does not estimate the intermediate gcd range.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass_sq_eq_highDelta (N : Finset ℕ) (β : ℕ → ℝ) (q δ b : ℕ) (hN : ∀ n ∈ N, n < δ) : betaResidueMass N β q δ b ^ 2 = betaResidueMass N (fun (n : ℕ) => β n ^ 2) q δ b

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_betaResidueMass_centered_sq_le_highDelta (N : Finset ℕ) (β : ℕ → ℝ) {q δ : ℕ} (hδ : 0 < δ) (hdq : δ ∣ q) (hN : ∀ n ∈ N, n < δ) : ∑ b ∈ betaReducedResidues δ, (betaResidueMass N β q δ b - coprimeMass N β q / ↑δ.totient) ^ 2 ≤ ∑ n ∈ N, β n ^ 2

The centered energy is at most the original beta energy, with the actual coprime sieve and the canonical reduced classes retained.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance_abs_le_highDelta {T : ℝ} (hT : 0 ≤ T) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) {q r : ℕ} (hδ : T < ↑(q.gcd r)) : |betaCovariance N β q r| ≤ ∑ n ∈ N, β n ^ 2

No progression estimate is needed once the gcd exceeds the support.