noncomputable def epsilon_padic (u : ℤ_[2]ˣ) : ZMod 2

The function $\varepsilon(u) = (u - 1) / 2 \pmod{2}$ applied to a $2$-adic unit $u$, computed via its image in $(\mathbb{Z}/8\mathbb{Z})^\times$.

noncomputable def omega_padic (u : ℤ_[2]ˣ) : ZMod 2

The function $\omega(u) = (u^2 - 1) / 8 \pmod{2}$ applied to a $2$-adic unit $u$, computed via its image in $(\mathbb{Z}/8\mathbb{Z})^\times$.

theorem hasPrimSolMod8_one_eq (u v : ℤ_[2]ˣ) : HasPrimitiveSolutionMod8_one u v ↔ hasPrimSolMod8_one_dec (toZModPow_unit 3 u) (toZModPow_unit 3 v)

The mod-$8$ primitive solution condition for type-one ($u x^2 + v y^2 \equiv z^2$) can be checked using a decidable version on the images in $(\mathbb{Z}/8\mathbb{Z})^\times$.

theorem hasPrimSolMod8_two_eq (u v : ℤ_[2]ˣ) : HasPrimitiveSolutionMod8_two u v ↔ hasPrimSolMod8_two_dec (toZModPow_unit 3 u) (toZModPow_unit 3 v)

The mod-$8$ primitive solution condition for type-two (involving the factor $2$) can be checked using a decidable version on the images in $(\mathbb{Z}/8\mathbb{Z})^\times$.

theorem hilbert_eq_formula_of_iff {a b : ℚ_[2]ˣ} (h_iff : padicHilbertSymbol 2 a b = 1 ↔ HilbertSymbol.HasPrimitiveSolution a b) {solMod : Prop} [Decidable solMod] (h_lift : HilbertSymbol.HasPrimitiveSolution a b ↔ solMod) {f : ℤ} (hf : f = 1 ∨ f = -1) (h_formula : solMod ↔ f = 1) : padicHilbertSymbol 2 a b = f

Bridge between the abstract Hilbert symbol and a concrete formula $f \in \{1, -1\}$: if the Hilbert symbol equals $1$ iff the form has a primitive solution, and the latter is equivalent to a decidable mod-$8$ condition expressed by $f = 1$, then the Hilbert symbol equals $f$.

noncomputable def twoQp : ℚ_[2]ˣ

The element $2 \in \mathbb{Q}_2^\times$, viewed as a unit.

theorem twoQp_val : ↑twoQp = 2

The underlying value of the unit twoQp is $2$.

theorem padicUnit_two_eq_mul (v : ℤ_[2]ˣ) : padicUnit_two v = twoQp * padicUnit_one v

Decomposition of a "type-two" $2$-adic unit (of the form $2 \cdot v$) as the product $2 \cdot v$.

theorem padicUnit_two_eq_mul' (u : ℤ_[2]ˣ) : padicUnit_two u = padicUnit_one u * twoQp

Decomposition of a "type-two" $2$-adic unit as $u \cdot 2$ (commuted form).

theorem twoQp_eq_padicUnit_two_one : twoQp = padicUnit_two 1

The unit $2 \in \mathbb{Q}_2^\times$ equals the type-two unit with multiplier $1$.

theorem neg_one_eq_padicUnit_one : -1 = padicUnit_one (-1)

The element $-1 \in \mathbb{Q}_2^\times$ equals the type-one unit coming from $-1 \in \mathbb{Z}_2^\times$.

theorem toZModPow_unit_one : toZModPow_unit 3 1 = 1

The image of $1 \in \mathbb{Z}_2^\times$ under reduction to $(\mathbb{Z}/8\mathbb{Z})^\times$ is $1$.

theorem toZModPow_unit_neg_one : toZModPow_unit 3 (-1) = -1

The image of $-1 \in \mathbb{Z}_2^\times$ under reduction to $(\mathbb{Z}/8\mathbb{Z})^\times$ is $-1$.

theorem thm_10_9_one_one (u v : ℤ_[2]ˣ) : padicHilbertSymbol 2 (padicUnit_one u) (padicUnit_one v) = hilbert2Adic_formula (toZModPow_unit 3 u) (toZModPow_unit 3 v) 0 0

Theorem 10.9 (case unit-unit). For $2$-adic units $u, v$, the Hilbert symbol $(u, v)_2$ equals the explicit formula $(-1)^{\varepsilon(u)\varepsilon(v)}$.

theorem thm_10_9_two_one (u v : ℤ_[2]ˣ) : padicHilbertSymbol 2 (padicUnit_two u) (padicUnit_one v) = hilbert2Adic_formula (toZModPow_unit 3 u) (toZModPow_unit 3 v) 1 0

Theorem 10.9 (case $2u$-unit). Hilbert symbol formula for $(2u, v)_2$ with $u, v \in \mathbb{Z}_2^\times$.

theorem thm_10_9_one_two (u v : ℤ_[2]ˣ) : padicHilbertSymbol 2 (padicUnit_one u) (padicUnit_two v) = hilbert2Adic_formula (toZModPow_unit 3 u) (toZModPow_unit 3 v) 0 1

Theorem 10.9 (case unit-$2v$). Hilbert symbol formula for $(u, 2v)_2$ with $u, v \in \mathbb{Z}_2^\times$, obtained from thm_10_9_two_one by symmetry.

theorem thm_10_9_two_two (u v : ℤ_[2]ˣ) : padicHilbertSymbol 2 (padicUnit_two u) (padicUnit_two v) = hilbert2Adic_formula (toZModPow_unit 3 u) (toZModPow_unit 3 v) 1 1

Theorem 10.9 (case $2u$-$2v$). Hilbert symbol formula for $(2u, 2v)_2$ with $u, v \in \mathbb{Z}_2^\times$, obtained by bilinearity from the unit-unit and mixed cases.