Unconditional complete Weil and Fouvry interval estimates

The odd-prime-power Gauss argument and the separate two-power stationary bound supply every primitive local estimate. Exact frequency descent and twisted CRT then give the divisor/gcd envelope for every positive modulus. The existing Fourier completion yields Fouvry's Lemma 3, uniformly in signed frequencies and real interval endpoints; no complete-sum estimate remains as a hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_power_primitive_weil (p k : ℕ) [Fact (Nat.Prime p)] (a d : ℤ) (hprimitive : ¬↑p ∣ a ∨ ¬↑p ∣ d) : ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑(p ^ k)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_weil (q : ℕ) [NeZero q] (a d : ℤ) : ‖completeKloosterman q (↑a) d‖ ≤ ↑q.divisors.card * √↑(q.gcd (a.natAbs.gcd d.natAbs)) * √↑q

The full complete-sum bound, including modulus one, nonprimitive frequency pairs, and zero or negative frequencies.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_weil_zmod (q : ℕ) [NeZero q] (m : ZMod q) (d : ℤ) : ‖completeKloosterman q m d‖ ≤ ↑q.divisors.card * √↑(q.gcd (m.val.gcd d.natAbs)) * √↑q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval_fouvry {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℕ) (x : NeZero q) (d : ℤ) (X Y : ℝ), X ≤ Y → Y - X ≤ ↑q → ‖reciprocalInterval q d X Y‖ ≤ C * √↑(q.gcd d.natAbs) * ↑q ^ (1 / 2 + ε)

F87 Lemma 3 for the actual reciprocal sum over X < c ≤ Y, with a single constant for all positive moduli, signed frequencies, and intervals of length at most the modulus.