Unconditional square-root cancellation at prime-square moduli

The stationary-phase identity is evaluated using equal-sized reduction fibers and the two-root bound in a field. This proves the primitive prime-square case, including p=2; the prime-modulus Weil theorem is not used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.zmod_reduction_fiber_card (q r : ℕ) [NeZero q] [NeZero r] (v : ZMod q) : {u : ZMod (q * r) | (ZMod.castHom ⋯ (ZMod q)) u = v}.card = r

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.zmod_reduction_preimage_card (q r : ℕ) [NeZero q] [NeZero r] (s : Finset (ZMod q)) : {u : ZMod (q * r) | (ZMod.castHom ⋯ (ZMod q)) u ∈ s}.card = s.card * r

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_square_modulus_norm_le_roots (m : ℕ) [NeZero m] (a d : ℤ) : ‖completeKloosterman (m * m) (↑a) d‖ ≤ ↑m * ↑{v : ZMod m | ↑a * v ^ 2 = ↑d}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.prime_quadratic_root_card_le_two (p : ℕ) [Fact (Nat.Prime p)] (a d : ZMod p) (ha : a ≠ 0) : {v : ZMod p | a * v ^ 2 = d}.card ≤ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_prime_square_norm_le (p : ℕ) [Fact (Nat.Prime p)] (a d : ℤ) (hprimitive : ¬↑p ∣ a ∨ ¬↑p ∣ d) : ‖completeKloosterman (p * p) (↑a) d‖ ≤ 2 * ↑p

A genuine square-root estimate, uniform in both frequencies, for primitive prime-square pairs. This includes the prime two.