Four-root bound over powers of two

If two unit roots have equal squares modulo 2^(n+1), their reductions modulo 2^n agree up to sign. Each of these two reduction fibers has size two. The proof uses only divisibility of the difference of squares.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.two_power_unit_quadratic_root_card_le_four (n : ℕ) (a d : ℤ) (ha : ¬2 ∣ a) : {v : ZMod (2 ^ n * 2) | IsUnit v ∧ ↑a * v ^ 2 = ↑d}.card ≤ 4

A unit quadratic congruence with odd leading coefficient has at most four roots modulo any positive power of two.