The dyadic square criterion #

Groundwork for the in-repo proof of B7′ (hilbertSymbol_dyadic). This file is the 2-adic square-lifting input, independent of the Hilbert symbol and reusable (it is the k = ℚ₂ germ of the B13/B11b unit-filtration square-class computations).

ℤ₂ˣ squares are exactly the units ≡ 1 (mod 8):

isSquare_of_toZModPow_eq_one — w ≡ 1 (mod 8) ⟹ w is a square (Hensel's lemma at X² − w, base point 1: ‖1 − w‖ ≤ 2⁻³ < 2⁻² = ‖2‖²);
toZModPow_sq_eq_one — the converse for units (an odd square is ≡ 1 (mod 8));
exists_unit_sq_eq — two units with equal image mod 8 differ by a unit square.

All std-3 (2-adic Hensel + a finite decide over ZMod 8).

source

theorem GQ2.DyadicSquares.isSquare_of_toZModPow_eq_one {w : ℤ_[2]} (hw : (PadicInt.toZModPow 3) w = 1) :

IsSquare w

A 2-adic integer ≡ 1 (mod 8) is a square. Hensel's lemma applied to F = X² − w at the approximate root a = 1: ‖F 1‖ = ‖1 − w‖ ≤ 2⁻³ < 2⁻² = ‖2‖² = ‖F′ 1‖².

source

theorem GQ2.DyadicSquares.toZModPow_sq_eq_one {t : ℤ_[2]} (ht : IsUnit t) :

(PadicInt.toZModPow 3) (t ^ 2) = 1

The converse for units. An odd 2-adic integer squares to ≡ 1 (mod 8).

source

theorem GQ2.DyadicSquares.exists_unit_sq_of_toZModPow_eq_one {m : ℤ_[2]ˣ} (hm : (PadicInt.toZModPow 3) ↑m = 1) :

∃ (w : ℤ_[2]ˣ), m = w ^ 2

A unit that is ≡ 1 (mod 8) is a unit square.

source

theorem GQ2.DyadicSquares.exists_unit_sq_eq {u v : ℤ_[2]ˣ} (h : (PadicInt.toZModPow 3) ↑u = (PadicInt.toZModPow 3) ↑v) :

∃ (w : ℤ_[2]ˣ), u = v * w ^ 2

Two units equal mod 8 differ by a unit square. The square-class reduction driving the Hilbert-symbol parity/residue dispatch (B7′-2).