WP1 1.1 — norm transfer for the Hilbert symbol

The Hilbert symbol (a, b)_k depends on b only through its class in kˣ / kˣ², but in the form used later (the descent in the proof of quadratic reciprocity) the input is not a square multiple of b but a norm from k(√a): we are handed t with t ^ 2 - a = b * b'.

Geometrically, t + √a has norm t ^ 2 - a = b * b' in k(√a), so if b is a norm then so is b' (divide the norm identity by b), and conversely. Since a nonzero nonsquare a satisfies (b, a)_k = 1 exactly when b is a norm from k(√a), the two symbols agree.

theorem HasseMinkowski.hilbertSym_eq_of_sq_sub_eq_mul {k : Type u_1} [Field k] {a b b' t : k} (hb : b ≠ 0) (hb' : b' ≠ 0) (h : t ^ 2 - a = b * b') : hilbertSym a b = hilbertSym a b'

If t ^ 2 - a = b * b' with b and b' nonzero, then (a, b)_k = (a, b')_k: the two second arguments differ by the norm of t + √a in k(√a), and being a norm from k(√a) is invariant under multiplication by a square class, in particular under b ↦ (t² - a) / b.

WP1 1.4 — the squarefree normal form

Every nonzero integer is a squarefree integer times a nonzero square, and the same holds for every nonzero rational after clearing denominators.

theorem HasseMinkowski.exists_squarefree_mul_sq_int (n : ℤ) (hn : n ≠ 0) : ∃ (m : ℤ) (u : ℤ), Squarefree m ∧ u ≠ 0 ∧ n = m * u ^ 2

Every nonzero integer is a squarefree integer times a nonzero square.

theorem HasseMinkowski.exists_squarefree_mul_sq (A : ℚ) (hA : A ≠ 0) : ∃ (a : ℤ), Squarefree a ∧ ∃ (s : ℚ), s ≠ 0 ∧ A = ↑a * s ^ 2

Every nonzero rational is a squarefree integer times a nonzero square.

WP1 1.3 — combining the local congruences by CRT

If t ^ 2 ≡ a (mod p) is solvable for every prime p ∣ b with b squarefree, then it is solvable modulo b, and the solution can be chosen in the balanced range 2 |t| ≤ |b|. The balanced representative is Int.bmod, which preserves the congruence and satisfies the bound.

theorem HasseMinkowski.exists_sq_mod_squarefree (a b : ℤ) (hb : Squarefree b) (h : ∀ (p : ℕ), Nat.Prime p → ↑p ∣ b → ∃ (t : ℤ), ↑p ∣ t ^ 2 - a) : ∃ (t : ℤ), b ∣ t ^ 2 - a ∧ 2 * |t| ≤ |b|

CRT plus a size bound. For squarefree b, if t ^ 2 - a is divisible by every prime factor of b, then some residue class t satisfies b ∣ t ^ 2 - a and 2 * |t| ≤ |b|.

WP1 1.2 — the local symbol being 1 forces a square residue

If (a, b)_p = 1, b is squarefree and p ∣ b, then a is a square modulo p. The case p ∣ a is trivial (t = 0), and p = 2 follows from a ^ 2 ≡ a (mod 2) (t = a). For odd p with p ∤ a, the integer b has p-adic valuation 1 (squarefree plus p ∣ b), so its norm is p⁻¹, while p ∤ a makes a a unit of ℤ_[p]. Serre's case 10 formula then reads (a, b)_p = (a / p), the quadratic character of a; being 1 it says a is a square mod p, and that square lifts back to an integer t with p ∣ t ^ 2 - a.

theorem HasseMinkowski.exists_sq_mod_of_hilbertSym (a b : ℤ) (hb : Squarefree b) (p : ℕ) [Fact (Nat.Prime p)] (hpb : ↑p ∣ b) (h : hilbertSym ↑a ↑b = 1) : ∃ (t : ℤ), ↑p ∣ t ^ 2 - a

Local square residue. If the local Hilbert symbol (a, b)_p equals 1 for a squarefree b divisible by p, then a ≡ t ^ 2 (mod p) for some integer t.

WP1 1.5 — the integral descent (Legendre's theorem)

The local–global principle for the Hilbert symbol at the integral place (Serre, Cours d'arithmétique, IV §3.2, Theorem 8): for squarefree integers a, b, if (a, b)_v = 1 at every place v — every prime and the real place — then (a, b)_ℚ = 1. The argument is an elementary descent on |a| + |b|: by symmetry assume |a| ≤ |b|; for |b| ≤ 1 all cases are immediate, while for |b| ≥ 2 CRT (exists_sq_mod_squarefree) produces t with t ^ 2 ≡ a (mod b), the size bound 2|t| ≤ |b| makes b' = (t ^ 2 - a) / b strictly smaller than b, the norm-transfer lemma hilbertSym_eq_of_sq_sub_eq_mul moves every local hypothesis from b to b', and stripping the square class of b' (exists_squarefree_mul_sq_int) lets the induction hypothesis finish.

theorem HasseMinkowski.legendre_int (a b : ℤ) (ha : Squarefree a) (hb : Squarefree b) (hp : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], hilbertSym ↑a ↑b = 1) (hr : hilbertSym ↑a ↑b = 1) : hilbertSym ↑a ↑b = 1

Integral descent. If the Hilbert symbol (a, b)_v equals 1 at every finite place and at the real place, for squarefree integers a, b, then (a, b)_ℚ = 1.

WP1 1.6 — the rank-three local–global principle

With legendre_int in hand we can discharge the hypothesis that RankThree.lean isolated: a global Hilbert symbol (A, B)_ℚ is 1 as soon as all its localizations are. The reduction from arbitrary nonzero A, B to squarefree integers is the square-class normal form 1.4, and the local hypotheses are moved along the same square factors by hilbertSym_mul_square_eq.

theorem HasseMinkowski.hilbertSymLocalGlobal : HilbertSymLocalGlobal

Legendre's theorem / Hasse norm theorem for ℚ(√B). If (A, B)_v = 1 at every place v of ℚ (every prime p and v = ∞), then (A, B)_ℚ = 1.

theorem HasseMinkowski.isotropic_of_rank_three' {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (Q : QuadraticForm ℚ V) (hr : Module.finrank ℚ V = 3) (hQ : QuadraticMap.Nondegenerate) (hQ' : EverywhereLocallyIsotropic Q) : Isotropic Q

Rank-three local–global principle (unconditional). A nondegenerate quadratic form of rank three over ℚ that is isotropic over every completion is isotropic over ℚ.