Exact stationary-phase localization at square moduli

This is a finite cancellation identity, not a bound assumed on a remainder. Translation by a square-zero layer removes every nonstationary residue. The square-modulus specialization works for all positive moduli, including powers of two, and leaves only the actual quadratic congruence.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_square_zero_localization (q : ℕ) [NeZero q] (a t : ZMod q) (d : ℤ) (ht : t ^ 2 = 0) : completeKloosterman q a d = ∑ u : ZMod q, if IsUnit u ∧ t * (a * u ^ 2 - ↑d) = 0 then ZMod.stdAddChar (a * u + ↑d * u⁻¹) else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.zmod_mul_modulus_eq_zero_iff (q r : ℕ) [NeZero q] [NeZero r] (z : ZMod (q * r)) : ↑r * z = 0 ↔ (ZMod.castHom ⋯ (ZMod q)) z = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_square_modulus_localization (m : ℕ) [NeZero m] (a d : ℤ) : completeKloosterman (m * m) (↑a) d = ∑ u : ZMod (m * m), if IsUnit u ∧ ↑a * (ZMod.castHom ⋯ (ZMod m)) u ^ 2 = ↑d then ZMod.stdAddChar (↑a * u + ↑d * u⁻¹) else 0

The remaining stationary condition is the actual quadratic congruence a u^2 = d (mod m). No primality, oddness, or unit-frequency assumption.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_square_modulus_norm_le (m : ℕ) [NeZero m] (a d : ℤ) : ‖completeKloosterman (m * m) (↑a) d‖ ≤ ↑{u : ZMod (m * m) | IsUnit u ∧ ↑a * (ZMod.castHom ⋯ (ZMod m)) u ^ 2 = ↑d}.card