class HilbertBilinearField (F : Type u_1) [Field F] extends CharZero F : Prop

A characteristic-zero field on which the Hilbert symbol is bilinear and nondegenerate. The two structural axioms encode: (i) if both $(a,c)_F$ and $(b,c)_F$ equal $-1$ then $(ab,c)_F = 1$ (used to derive bilinearity); (ii) for every non-square unit $c$ there exists $b$ with $(b,c)_F = -1$ (nondegeneracy of the Hilbert pairing).

• cast_injective : Function.Injective Nat.cast
• isSolvable_mul_of_both_neg (a b c : Fˣ) : hilbertSymbol F a c = -1 → hilbertSymbol F b c = -1 → hilbertSymbol F (a * b) c = 1
• nondegenerate (c : Fˣ) : ¬IsSquare ↑c → ∃ (b : Fˣ), hilbertSymbol F b c = -1

theorem legendreSym_val_local {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ZMod p) : legendreSym p ↑a.val = (quadraticChar (ZMod p)) a

Local variant: the Legendre symbol applied to ZMod.val a agrees with the quadratic character of ZMod p evaluated at a.

theorem padicUnitLegendre_mul_local {p : ℕ} [hp : Fact (Nat.Prime p)] (u₁ u₂ : ℤ_[p]ˣ) : padicUnitLegendre (u₁ * u₂) = padicUnitLegendre u₁ * padicUnitLegendre u₂

Multiplicativity of padicUnitLegendre: $\left(\frac{u_1 u_2}{p}\right) = \left(\frac{u_1}{p}\right)\left(\frac{u_2}{p}\right)$.

theorem padicUnitLegendre_eq_one_or_neg_one_local {p : ℕ} [hp : Fact (Nat.Prime p)] (v : ℤ_[p]ˣ) : padicUnitLegendre v = 1 ∨ padicUnitLegendre v = -1

padicUnitLegendre always takes values in $\{\pm 1\}$ for an odd prime, since the quadratic character of a nonzero element of $\mathbb{F}_p$ is $\pm 1$.

theorem padic_unit_decomp {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℚ_[p]ˣ) : ∃ (α : ℤ) (u : ℤ_[p]ˣ), a = padicPowerUnitZ p α u

Every nonzero $p$-adic number can be written as $p^\alpha u$ with $\alpha \in \mathbb{Z}$ and $u \in \mathbb{Z}_p^\times$, i.e. $a = $ padicPowerUnitZ p α u.

theorem natAbs_add_mod_two (α₁ α₂ : ℤ) : (α₁ + α₂).natAbs % 2 = (α₁.natAbs + α₂.natAbs) % 2

The parity of $|\alpha_1 + \alpha_2|$ equals the parity of $|\alpha_1| + |\alpha_2|$.

theorem formula_bilinear_natAbs {m : ℕ} (α₁ α₂ γ Lu₁ Lu₂ Lw : ℤ) (_hLu₁ : Lu₁ ^ 2 = 1) (_hLu₂ : Lu₂ ^ 2 = 1) (hLw : Lw ^ 2 = 1) : (-1) ^ ((α₁ + α₂).natAbs * γ.natAbs * m) * (Lu₁ * Lu₂) ^ γ.natAbs * Lw ^ (α₁ + α₂).natAbs = (-1) ^ (α₁.natAbs * γ.natAbs * m) * Lu₁ ^ γ.natAbs * Lw ^ α₁.natAbs * ((-1) ^ (α₂.natAbs * γ.natAbs * m) * Lu₂ ^ γ.natAbs * Lw ^ α₂.natAbs)

Algebraic identity expressing bilinearity of the closed-form Hilbert formula in the first argument, with all exponents written as natural-number absolute values and using the square-equal-to-one hypotheses on the Legendre values.

theorem padic_unit_square_of_legendre_one {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (v : ℤ_[p]ˣ) (hv : padicUnitLegendre v = 1) : IsSquare ↑v

For an odd prime $p$, a $p$-adic unit $v$ whose Legendre symbol is $1$ is a square in $\mathbb{Z}_p$ (Hensel lifting from a square root mod $p$).

theorem padicPowerUnitZ_isSquare_of_unit_sq_even_val {p : ℕ} [hp : Fact (Nat.Prime p)] {γ : ℤ} (v : ℤ_[p]ˣ) (hv_sq : IsSquare ↑v) (k : ℕ) (hk : γ.natAbs = k + k) : IsSquare ↑(padicPowerUnitZ p γ v)

If $v$ is a square in $\mathbb{Z}_p$ and $\gamma$ has even absolute value, then $p^\gamma v$ is a square in $\mathbb{Q}_p$.

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

Bridge: existence of a primitive mod-$8$ solution for $z^2 = ux^2 + vy^2$ over $\mathbb{Z}_2$ is equivalent to the decidable predicate on the mod-$8$ reductions.

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

Bridge: existence of a primitive mod-$8$ solution for $z^2 = 2u x^2 + v y^2$ over $\mathbb{Z}_2$ is equivalent to the decidable predicate on the mod-$8$ reductions.

theorem hilbert_eq_formula_of_iff_local {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

Glue lemma: given that the Hilbert symbol equals $1$ iff there is a primitive solution, that primitive solvability is equivalent to a decidable mod-$8$ predicate, and the formula is $\pm 1$ matching the predicate, conclude that the Hilbert symbol equals the formula.

theorem thm_10_9_one_one_local (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 $(\alpha,\beta) = (0,0)$: the $2$-adic Hilbert symbol on unit inputs $(u, v)$ equals the closed-form formula at $(0,0)$.

theorem thm_10_9_two_one_local (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 $(\alpha,\beta) = (1,0)$: $(2u, v)_{\mathbb{Q}_2}$ equals the closed-form formula at $(1, 0)$.

theorem hilbertSymbol_symm_local (a b : ℚ_[2]ˣ) : hilbertSymbol ℚ_[2] a b = hilbertSymbol ℚ_[2] b a

Symmetry of the Hilbert symbol over $\mathbb{Q}_2$: $(a, b)_{\mathbb{Q}_2} = (b, a)_{\mathbb{Q}_2}$ (local instance of the general symmetry, swapping $(x,y)$).

theorem thm_10_9_one_two_local (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 $(\alpha,\beta) = (0,1)$: $(u, 2v)_{\mathbb{Q}_2}$ equals the closed-form formula at $(0, 1)$, obtained from the $(1,0)$ case by symmetry.

theorem toZModPow_unit_mul (u v : ℤ_[2]ˣ) : toZModPow_unit 3 (u * v) = toZModPow_unit 3 u * toZModPow_unit 3 v

Multiplicativity of the mod-$8$ reduction on units: toZModPow_unit 3 (u * v) = toZModPow_unit 3 u * toZModPow_unit 3 v.

theorem padic_hilbert_bilinear_p2_two_two_case (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 $(\alpha,\beta) = (1,1)$: $(2u, 2v)_{\mathbb{Q}_2}$ equals the closed-form formula at $(1, 1)$. This is the remaining case completing Theorem 10.9.

theorem thm_10_9_two_two_local (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 $(\alpha,\beta) = (1,1)$: wrapper around padic_hilbert_bilinear_p2_two_two_case matching the naming convention of the other cases.

theorem hilbert_formula_2adic_fin2 (α β : Fin 2) (u v : ℤ_[2]ˣ) : padicHilbertSymbol 2 (padicPowerUnit 2 α u) (padicPowerUnit 2 β v) = hilbert2Adic_formula (toZModPow_unit 3 u) (toZModPow_unit 3 v) ↑α ↑β

Theorem 10.9 in unified form: for $\alpha, \beta \in \{0,1\}$ and units $u, v \in \mathbb{Z}_2^\times$, the $2$-adic Hilbert symbol $(2^\alpha u, 2^\beta v)_{\mathbb{Q}_2}$ equals the closed-form formula at $(\alpha, \beta)$.

theorem hilbert_formula_2adic_general (α β : ℤ) (u v : ℤ_[2]ˣ) : padicHilbertSymbol 2 (padicPowerUnitZ 2 α u) (padicPowerUnitZ 2 β v) = hilbert2Adic_formula (toZModPow_unit 3 u) (toZModPow_unit 3 v) (α % 2).toNat (β % 2).toNat

Theorem 10.9 in fully general form: for $\alpha, \beta \in \mathbb{Z}$ and units $u, v \in \mathbb{Z}_2^\times$, $(2^\alpha u, 2^\beta v)_{\mathbb{Q}_2}$ equals the closed-form formula at $(\alpha \bmod 2, \beta \bmod 2)$, using that the symbol is unchanged by even shifts in the valuation.

theorem padic_isSolvable_mul_of_both_neg_p2 [hp : Fact (Nat.Prime 2)] (a b c : ℚ_[2]ˣ) : hilbertSymbol ℚ_[2] a c = -1 → hilbertSymbol ℚ_[2] b c = -1 → hilbertSymbol ℚ_[2] (a * b) c = 1

Half of bilinearity over $\mathbb{Q}_2$: if $(a, c)_{\mathbb{Q}_2} = (b, c)_{\mathbb{Q}_2} = -1$, then $(ab, c)_{\mathbb{Q}_2} = 1$. Reduced via the $p$-adic decomposition and the closed-form formula to the verified bilinearity lemma formula_mul_left_core.

theorem padic_isSolvable_mul_of_both_neg_ax (p : ℕ) [Fact (Nat.Prime p)] (a b c : ℚ_[p]ˣ) : hilbertSymbol ℚ_[p] a c = -1 → hilbertSymbol ℚ_[p] b c = -1 → hilbertSymbol ℚ_[p] (a * b) c = 1

Half of bilinearity over $\mathbb{Q}_p$ for arbitrary primes $p$: if $(a,c)_{\mathbb{Q}_p} = (b,c)_{\mathbb{Q}_p} = -1$ then $(ab,c)_{\mathbb{Q}_p} = 1$. The case $p = 2$ is padic_isSolvable_mul_of_both_neg_p2; the odd case uses the closed-form formula together with multiplicativity of the Legendre symbol.

@[reducible]

def hasPrimSolMod8_one_loc (u₀ v₀ : (ZMod (2 ^ 3))ˣ) : Prop

Local copy (within this Nondeg2Adic_Computational section, with classical decidability disabled) of the decidable predicate for primitive mod-$8$ solvability of $z^2 = u_0 x^2 + v_0 y^2$.

@[reducible]

def hasPrimSolMod8_two_loc (u₀ v₀ : (ZMod (2 ^ 3))ˣ) : Prop

Local copy (within Nondeg2Adic_Computational) of the decidable predicate for primitive mod-$8$ solvability of $z^2 = 2 u_0 x^2 + v_0 y^2$.

@[implicit_reducible]

instance instDecidableHasPrimSolMod8_one_loc (u₀ v₀ : (ZMod (2 ^ 3))ˣ) : Decidable (hasPrimSolMod8_one_loc u₀ v₀)

Decidability of hasPrimSolMod8_one_loc via finite search over ZMod 8.

@[implicit_reducible]

instance instDecidableHasPrimSolMod8_two_loc (u₀ v₀ : (ZMod (2 ^ 3))ˣ) : Decidable (hasPrimSolMod8_two_loc u₀ v₀)

Decidability of hasPrimSolMod8_two_loc via finite search over ZMod 8.

@[reducible]

def nondeg_unit_combined (w₀ : (ZMod (2 ^ 3))ˣ) : Prop

Decidable witness predicate for $2$-adic nondegeneracy: a unit $w_0 \in (\mathbb{Z}/8)^\times$ has either a unit $v_0$ with $z^2 = v_0 x^2 + w_0 y^2$ insolvable mod $8$, or a unit $v_0$ with $z^2 = 2v_0 x^2 + w_0 y^2$ insolvable mod $8$.

@[implicit_reducible]

instance instDecidableNondeg_unit_combined (w₀ : (ZMod (2 ^ 3))ˣ) : Decidable (nondeg_unit_combined w₀)

Decidability of nondeg_unit_combined from decidability of each disjunct.

theorem nondeg_mod8_unit_witness (w₀ : (ZMod (2 ^ 3))ˣ) : w₀ ≠ 1 → nondeg_unit_combined w₀

Brute-force verification: every non-identity unit $w_0 \in (\mathbb{Z}/8)^\times$ admits a witness of nondegeneracy in the nondeg_unit_combined sense, used in the $p = 2$ case of the nondegeneracy axiom.

@[reducible]

def nondeg_two_prop (w₀ : (ZMod (2 ^ 3))ˣ) : Prop

Decidable predicate: a unit $w_0 \in (\mathbb{Z}/8)^\times$ admits some unit $v_0$ for which $z^2 = 2 w_0 x^2 + v_0 y^2$ is insolvable mod $8$. Used for nondegeneracy when the valuation of $c$ is odd.

@[implicit_reducible]

instance instDecidableNondeg_two_prop (w₀ : (ZMod (2 ^ 3))ˣ) : Decidable (nondeg_two_prop w₀)

Decidability of nondeg_two_prop via finite search over $(\mathbb{Z}/8)^\times$.

theorem nondeg_mod8_two_witness (w₀ : (ZMod (2 ^ 3))ˣ) : nondeg_two_prop w₀

Brute-force verification: every unit $w_0 \in (\mathbb{Z}/8)^\times$ satisfies nondeg_two_prop. Used for nondegeneracy when $c = 2^{\text{odd}} w$.

noncomputable def toZMod8Unit (w : ℤ_[2]ˣ) : (ZMod (2 ^ 3))ˣ

Reduction modulo $8$ of a $2$-adic unit, producing a unit of $\mathbb{Z}/8$.

theorem toZMod8Unit_val (w : ℤ_[2]ˣ) : ↑(toZMod8Unit w) = (PadicInt.toZModPow 3) ↑w

The underlying element of toZMod8Unit w is PadicInt.toZModPow 3 (↑w).

theorem hasPrimSolMod8_one_iff (u v : ℤ_[2]ˣ) : HasPrimitiveSolutionMod8_one u v ↔ hasPrimSolMod8_one_loc (toZMod8Unit u) (toZMod8Unit v)

Bridge: primitive mod-$8$ solvability of $z^2 = ux^2 + vy^2$ over $\mathbb{Z}_2$ is equivalent to the local decidable predicate on toZMod8Unit u and toZMod8Unit v.

theorem hasPrimSolMod8_two_iff (u v : ℤ_[2]ˣ) : HasPrimitiveSolutionMod8_two u v ↔ hasPrimSolMod8_two_loc (toZMod8Unit u) (toZMod8Unit v)

Bridge: primitive mod-$8$ solvability of $z^2 = 2u x^2 + v y^2$ over $\mathbb{Z}_2$ is equivalent to the local decidable predicate on toZMod8Unit u and toZMod8Unit v.

theorem toZMod8Unit_surj (u₀ : (ZMod (2 ^ 3))ˣ) : ∃ (u : ℤ_[2]ˣ), toZMod8Unit u = u₀

Surjectivity of toZMod8Unit: every unit in $\mathbb{Z}/8$ lifts to some unit in $\mathbb{Z}_2$.

theorem padicUnit_one_eq_unitZpToQp (w : ℤ_[2]ˣ) : ↑(padicUnit_one w) = ↑(HilbertSymbol.unitZpToQp w)

The underlying $\mathbb{Q}_2$-value of padicUnit_one w equals the image of $w$ under unitZpToQp, i.e. the embedding $\mathbb{Z}_2^\times \hookrightarrow \mathbb{Q}_2^\times$.

theorem padicUnit_one_eq_unitZpToQp' (w : ℤ_[2]ˣ) : padicUnit_one w = HilbertSymbol.unitZpToQp w

Unit-level version of padicUnit_one_eq_unitZpToQp: equality in $\mathbb{Q}_2^\times$.

theorem padicUnit_two_eq_qpPrime_mul (w : ℤ_[2]ˣ) : ↑(padicUnit_two w) = ↑(qpPrime 2) * ↑(HilbertSymbol.unitZpToQp w)

The underlying $\mathbb{Q}_2$-value of padicUnit_two w factors as $2 \cdot w$.

theorem padicUnit_two_eq_qpPrime_mul' (w : ℤ_[2]ˣ) : padicUnit_two w = qpPrime 2 * HilbertSymbol.unitZpToQp w

Unit-level version of padicUnit_two_eq_qpPrime_mul: equality in $\mathbb{Q}_2^\times$.

theorem padic_nondegenerate_p2 [hp : Fact (Nat.Prime 2)] (c : ℚ_[2]ˣ) : ¬IsSquare ↑c → ∃ (b : ℚ_[2]ˣ), hilbertSymbol ℚ_[2] b c = -1

Nondegeneracy of the $2$-adic Hilbert pairing: for every non-square unit $c \in \mathbb{Q}_2^\times$ there exists $b \in \mathbb{Q}_2^\times$ with $(b, c)_{\mathbb{Q}_2} = -1$. Proven by lifting an obstruction from the mod-$8$ witnesses nondeg_mod8_unit_witness/nondeg_mod8_two_witness.

theorem padic_nondegenerate_ax (p : ℕ) [Fact (Nat.Prime p)] (c : ℚ_[p]ˣ) : ¬IsSquare ↑c → ∃ (b : ℚ_[p]ˣ), hilbertSymbol ℚ_[p] b c = -1

Nondegeneracy of the $p$-adic Hilbert pairing for every prime $p$. For odd $p$, uses a quadratic non-residue $u_{\text{nr}}$ and the closed-form formula; for $p = 2$ uses padic_nondegenerate_p2.

instance instHilbertBilinearFieldPadic (p : ℕ) [Fact (Nat.Prime p)] : HilbertBilinearField ℚ_[p]

The $p$-adic field $\mathbb{Q}_p$ is a HilbertBilinearField: the Hilbert symbol $(-,-)_{\mathbb{Q}_p}$ is bilinear and nondegenerate.

theorem real_unit_not_square_neg (c : ℝˣ) (hc : ¬IsSquare ↑c) : ↑c < 0

A nonzero real number that is not a square must be negative (since nonnegative reals admit square roots).

theorem real_pos_isSolvable (a : ℝˣ) (ha : 0 < ↑a) (b : ℝˣ) : HilbertSymbol.IsSolvable ℝ a b

If $a > 0$ is real, then $z^2 = a x^2 + b y^2$ is solvable with $(x, y, z) = (1/\sqrt{a}, 0, 1)$, so the real Hilbert symbol $(a, b)_{\mathbb{R}} = 1$ for any $b$.

theorem real_hilbert_neg_one_imp_neg_left (a c : ℝˣ) (h : hilbertSymbol ℝ a c = -1) : ↑a < 0

If $(a, c)_{\mathbb{R}} = -1$ then $a < 0$ (contrapositive of real_pos_isSolvable).

theorem real_hilbert_neg_one_imp_neg_right (a c : ℝˣ) (h : hilbertSymbol ℝ a c = -1) : ↑c < 0

If $(a, c)_{\mathbb{R}} = -1$ then $c < 0$ (symmetric counterpart of the previous lemma).

instance instHilbertBilinearFieldReal : HilbertBilinearField ℝ

The real field $\mathbb{R}$ is a HilbertBilinearField: bilinearity holds because two negative reals multiply to a positive one, and nondegeneracy holds because $-1$ pairs nontrivially with itself.

theorem hilbertSymbol.isSolvable_mul_of_both_neg {F : Type u_1} [Field F] [HilbertBilinearField F] (a b c : Fˣ) (ha : hilbertSymbol F a c = -1) (hb : hilbertSymbol F b c = -1) : hilbertSymbol F (a * b) c = 1

Wrapper exposing HilbertBilinearField.isSolvable_mul_of_both_neg in the hilbertSymbol namespace.

theorem hilbertSymbol.symm {F : Type u_1} [Field F] (a b : Fˣ) : hilbertSymbol F a b = hilbertSymbol F b a

Symmetry of the Hilbert symbol over any field: $(a, b)_F = (b, a)_F$ (swap $(x, y)$ in the defining equation $z^2 = a x^2 + b y^2$).

theorem hilbertSymbol.mul_left {F : Type u_1} [Field F] [HilbertBilinearField F] (a b c : Fˣ) : hilbertSymbol F (a * b) c = hilbertSymbol F a c * hilbertSymbol F b c

Bilinearity in the left argument: $(ab, c)_F = (a, c)_F \cdot (b, c)_F$ for any HilbertBilinearField $F$.

theorem hilbertSymbol.mul_right {F : Type u_1} [Field F] [HilbertBilinearField F] (a b c : Fˣ) : hilbertSymbol F a (b * c) = hilbertSymbol F a b * hilbertSymbol F a c

Bilinearity in the right argument: $(a, bc)_F = (a, b)_F \cdot (a, c)_F$, derived from symmetry and mul_left.

theorem hilbertSymbol.nondegenerate {F : Type u_1} [Field F] [HilbertBilinearField F] (c : Fˣ) (hc : ¬IsSquare ↑c) : ∃ (b : Fˣ), hilbertSymbol F b c = -1

Nondegeneracy axiom of HilbertBilinearField, exposed in the hilbertSymbol namespace: every non-square unit pairs to $-1$ with some element.