Primitive Kloosterman estimates at powers of two

The square-zero layer localizes the sum to unit quadratic roots modulo the smaller half-power. Four roots and the exact size of the reduction fibers suffice: the factor k+1 absorbs the elementary stationary-phase constant. No odd-characteristic Gauss-sum identity is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_two_power_primitive_weil (k : ℕ) (a d : ℤ) (hprimitive : ¬2 ∣ a ∨ ¬2 ∣ d) : ‖completeKloosterman (2 ^ k) (↑a) d‖ ≤ ↑(k + 1) * √(2 ^ k)

Primitive Weil-type bound at every power of two, including modulus one. The elementary stationary bound is absorbed by the divisor factor k+1.