Elementary prime-power cancellation

Translation by the last nonzero prime-power layer preserves units. If just one frequency is divisible by the prime, it multiplies the complete sum by a nontrivial constant character, forcing the sum to vanish. The argument works in characteristic two as well; it uses no quadratic Gauss-sum formula.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_symm (q : ℕ) [NeZero q] (a d : ℤ) : completeKloosterman q (↑a) d = completeKloosterman q (↑d) a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.zmod_isUnit_add_square_zero {q : ℕ} (u t : ZMod q) (ht : t ^ 2 = 0) : IsUnit (u + t) ↔ IsUnit u

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.zmod_inv_add_square_zero {q : ℕ} (u t : ZMod q) (hu : IsUnit u) (ht : t ^ 2 = 0) : (u + t)⁻¹ = u⁻¹ - t * u⁻¹ ^ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_vanish_of_square_zero_shift (q : ℕ) [NeZero q] (a t : ZMod q) (d : ℤ) (ht : t ^ 2 = 0) (hdt : ↑d * t = 0) (hat : ZMod.stdAddChar (a * t) ≠ 1) : completeKloosterman q a d = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_power_vanish (p k : ℕ) [Fact (Nat.Prime p)] (a d : ℤ) (ha : ¬↑p ∣ a) (hd : ↑p ∣ d) : completeKloosterman (p * p ^ (k + 1)) (↑a) d = 0

For exponent at least two, unequal frequency valuations give zero after common-factor descent. No odd-prime hypothesis is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_power_vanish_left (p k : ℕ) [Fact (Nat.Prime p)] (a d : ℤ) (ha : ↑p ∣ a) (hd : ¬↑p ∣ d) : completeKloosterman (p * p ^ (k + 1)) (↑a) d = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_zero_frequency (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) (ha : a ≠ 0) : completeKloosterman p a 0 = -1

At exponent one, a single zero frequency gives -1, not zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_zero_left (p : ℕ) [Fact (Nat.Prime p)] (d : ℤ) (hd : ¬↑p ∣ d) : completeKloosterman p 0 d = -1