Unit squares modulo powers of two

Every element of the form 1 + 8a is the square of a unit modulo 2^{k+1}. The square root has the form 1 + 4t: the bijection t ↦ 2t² + t supplies t. In particular, an integer congruent to one modulo eight gives a unit square at every positive dyadic exponent. The variant 5 - 4r, for a unit r, provides the rotation coefficient for pairs of odd cyclic dyadic forms.

For any modulus divisible by sixteen, the kernel of reduction to half the modulus consists of squares (ZMod.isSquare_of_cast_half_eq_one). This also applies when the modulus has odd factors and gives the dyadic conductor bound for quadratic characters.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §93.
• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, Proposition 1.8.2(c).

theorem ZMod.isSquare_of_cast_half_eq_one {N : ℕ} (x : ZMod N) (hN : 16 ∣ N) (hx : x.cast = 1) : IsSquare x

If sixteen divides the modulus, every residue that becomes one modulo half the modulus is a square. The modulus may be zero, in which case the hypothesis forces x = 1.

theorem ZMod.exists_unit_sq_eq_one_add_eight_mul {k : ℕ} (a : ZMod (2 ^ (k + 1))) : ∃ (u : (ZMod (2 ^ (k + 1)))ˣ), ↑u ^ 2 = 1 + 8 * a

Every residue 1 + 8a modulo 2^{k+1} is the square of a unit.

theorem ZMod.exists_unit_sq_eq_five_sub_four_mul {k : ℕ} {r : ZMod (2 ^ (k + 1))} (hr : IsUnit r) : ∃ (u : (ZMod (2 ^ (k + 1)))ˣ), ↑u ^ 2 = 5 - 4 * r

The residue 5 - 4r is a unit square whenever r is a unit modulo 2^{k+1}.

theorem ZMod.exists_unit_sq_mul_intCast_eq_of_modEq_eight (k : ℕ) {θ η : ℤ} (hη : Odd η) (h : θ ≡ η [ZMOD 8]) : ∃ (u : (ZMod (2 ^ (k + 1)))ˣ), ↑η * ↑u ^ 2 = ↑θ

Odd integer coefficients congruent modulo eight differ by a unit square modulo any positive power of two. The square multiplies the second coefficient to the first.