Hilbert-symbol existence theorem

Given prescribed local Hilbert-symbol values (x, aᵢ)_v = e_{i,v} at all places v of ℚ, one asks whether there is a single rational x realising all of them. The answer is given by the classical necessary-and-sufficient conditions (Serre, Cours d'arithmétique, Ch. III):

1. for each i, almost all the e_{i,v} are 1;
2. for each i, the product of the e_{i,v} is 1 (the product formula);
3. the prescription is locally realisable at every place.

This file ports the constructive core of the HassePrinciple proof. Writing S for the finite set of prime numbers dividing some aᵢ (together with 2) and T for the finite set of primes at which some e_{i,p} equals -1, the construction produces x = A · q with A = ∏_{t ∈ T} t and q a prime chosen by Dirichlet's theorem so that q ≡ A (mod 4·∏_{s ∈ S} s). This x is a square at every prime of S, has p-adic valuation 1 at every prime of T and valuation 0 at the remaining primes — exactly the three facts on which the place-by-place verification rests.

Status

This file provides the Dirichlet/CRT construction of S, T, A, M, the squareness/valuation lemmas at each place, the disjoint case of the existence theorem (exists_disjoint, WP3.1 of Plan-v3.md), and the general existence theorem (exists_rat_hilbertSym, WP3.2, Serre III Thm 4), which reduces to the disjoint case. No sorry is introduced.

Provenance

This file is a derived work. It is based on HilbertSymbol/ExistenceTheorem.lean of the HassePrinciple project (https://github.com/mariainesdff/HassePrinciple, Apache-2.0, Copyright (c) 2026 Nirvana Coppola, María Inés de Frutos-Fernández), a Women in Numbers 7 collaboration. It has been modified: the statements and proofs were rewritten for Lean 4.33 / Mathlib without upstream's module system, and the development is extended beyond what upstream proves. Upstream declaration names are kept so that the two developments can be compared side by side. See the repository NOTICE file.

noncomputable def HasseMinkowski.Existence.S {I : Type u_1} [Finite I] (a : I → ℤ) : Finset Nat.Primes

S is the finite set of primes dividing the numerator or the denominator of some a i, together with 2. (In Serre, S also contains ∞.)

Equations

• HasseMinkowski.Existence.S a = ((Finset.univ.biUnion fun (i : I) => (a i).natAbs.primeFactors) ∪ {2}).preimage Subtype.val ⋯

theorem HasseMinkowski.Existence.two_in_S {I : Type u_1} [Finite I] (a : I → ℤ) : ⟨2, Nat.prime_two⟩ ∈ S a

theorem HasseMinkowski.Existence.Tfin {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) : (⋃ (i : I), {p : Nat.Primes | ep i p = -1}).Finite

noncomputable def HasseMinkowski.Existence.T {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) : Finset Nat.Primes

T is the finite set of primes such that at least one of the e_{i,v} is -1.

Equations

• HasseMinkowski.Existence.T hep h1 = ⋯.toFinset

theorem HasseMinkowski.Existence.ep_eq_one_of_not_mem_T {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {p : Nat.Primes} (hpT : p ∉ T hep h1) (i : I) : ep i p = 1

theorem HasseMinkowski.Existence.ep_eq_one_iff_not_mem_T {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (p : Nat.Primes) : p ∉ T hep h1 ↔ ∀ (i : I), ep i p = 1

theorem HasseMinkowski.Existence.ep_eq_one_of_mem_S_disjoint {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (a : I → ℤ) (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (disjoint_ST : Disjoint (S a) (T hep h1)) {p : Nat.Primes} (hpS : p ∈ S a) (i : I) : ep i p = 1

theorem HasseMinkowski.Existence.is_unit_ai_of_p_notMem_S {I : Type u_1} [Finite I] (a : I → ℤ) (ha : ∀ (i : I), a i ≠ 0) {p : Nat.Primes} (hpS : p ∉ S a) (i : I) : padicValInt (↑p) (a i) = 0

noncomputable def HasseMinkowski.Existence.A {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) : ℕ

A is the product of all primes of T.

Equations

• HasseMinkowski.Existence.A hep h1 = ∏ t ∈ HasseMinkowski.Existence.T hep h1, ↑t

theorem HasseMinkowski.Existence.A_ne_zero {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) : A hep h1 ≠ 0

theorem HasseMinkowski.Existence.A_pos {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hep : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) : 0 < A hep h1

noncomputable def HasseMinkowski.Existence.M {I : Type u_1} [Finite I] (a : I → ℤ) : ℕ

M = 4 · ∏_{s ∈ S} s, the modulus used in the congruence defining q.

Equations

• HasseMinkowski.Existence.M a = 4 * ∏ s ∈ HasseMinkowski.Existence.S a, ↑s

theorem HasseMinkowski.Existence.M_ne_zero {I : Type u_1} [Finite I] (a : I → ℤ) : M a ≠ 0

WP3.1 sub-lemmas: the auxiliary prime ℓ

The construction x = A · ℓ needs ℓ to be a prime larger than every prime of S ∪ T and congruent to A modulo M. These lemmas record the elementary consequences of those two hypotheses: ℓ ∉ T (hence ε_{i,ℓ} = 1), the congruence M ∣ ℓ - A, and the divisibility of A by exactly the primes of T.

theorem HasseMinkowski.Existence.prime_notMem_T_of_lt {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓgt : ∀ s ∈ S a ∪ T hε h1, ↑s < ℓ) : ⟨ℓ, hℓ⟩ ∉ T hε h1

theorem HasseMinkowski.Existence.ep_eq_one_prime_of_lt {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓgt : ∀ s ∈ S a ∪ T hε h1, ↑s < ℓ) (i : I) : ep i ⟨ℓ, hℓ⟩ = 1

theorem HasseMinkowski.Existence.M_dvd_int {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {ℓ : ℕ} (hℓA : ℓ ≡ A hε h1 [MOD M a]) : ↑(M a) ∣ ↑ℓ - ↑(A hε h1)

theorem HasseMinkowski.Existence.dvd_A_of_mem_T {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {p : Nat.Primes} (hp : p ∈ T hε h1) : ↑p ∣ A hε h1

theorem HasseMinkowski.Existence.not_dvd_A_of_notMem_T {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {p : Nat.Primes} (hp : p ∉ T hε h1) : ¬↑p ∣ A hε h1

theorem HasseMinkowski.Existence.two_notMem_T_of_disjoint {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (hdisj : Disjoint (S a) (T hε h1)) : ⟨2, Nat.prime_two⟩ ∉ T hε h1

theorem HasseMinkowski.Existence.not_two_dvd_A {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (hdisj : Disjoint (S a) (T hε h1)) : ¬2 ∣ A hε h1

theorem HasseMinkowski.Existence.padicValNat_A_of_mem_T {I : Type u_1} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {p : Nat.Primes} (hp : p ∈ T hε h1) : padicValNat (↑p) (A hε h1) = 1

theorem HasseMinkowski.Existence.eight_dvd_M {I : Type u_1} [Finite I] (a : I → ℤ) : 8 ∣ M a

theorem HasseMinkowski.Existence.dvd_M_of_mem_S {I : Type u_1} [Finite I] (a : I → ℤ) {p : Nat.Primes} (hpS : p ∈ S a) : ↑p ∣ M a

theorem HasseMinkowski.Existence.prime_not_dvd_of_lt {p : Nat.Primes} {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hlt : ↑p < ℓ) : ¬↑p ∣ ℓ

theorem HasseMinkowski.Existence.prime_not_dvd_of_ne {p : Nat.Primes} {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hne : ↑p ≠ ℓ) : ¬↑p ∣ ℓ

theorem HasseMinkowski.Existence.isSquare_A_mul_ell_of_mem_S {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (hdisj : Disjoint (S a) (T hε h1)) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓA : ℓ ≡ A hε h1 [MOD M a]) (hℓgt : ∀ s ∈ S a ∪ T hε h1, ↑s < ℓ) {p : Nat.Primes} (hpS : p ∈ S a) : IsSquare ↑(A hε h1 * ℓ)

theorem HasseMinkowski.Existence.hilbertSym_A_mul_ell_eq_one_of_mem_S {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (ha : ∀ (i : I), a i ≠ 0) (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (hdisj : Disjoint (S a) (T hε h1)) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓA : ℓ ≡ A hε h1 [MOD M a]) (hℓgt : ∀ s ∈ S a ∪ T hε h1, ↑s < ℓ) {p : Nat.Primes} (hpS : p ∈ S a) (i : I) : hilbertSym ↑(a i) ↑(A hε h1 * ℓ) = 1

The symbol at a p-adic unit against an arbitrary element

For odd p, if the first argument is a unit then only the parity of the valuation of the second argument matters: (u,b)_p = χ(u) for odd valuation and = 1 for even valuation.

theorem HasseMinkowski.Existence.hilbertSym_A_mul_ell_eq_of_mem_T {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (ha : ∀ (i : I), a i ≠ 0) (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) (hdisj : Disjoint (S a) (T hε h1)) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓgt : ∀ s ∈ S a ∪ T hε h1, ↑s < ℓ) (h3 : ∀ (p : Nat.Primes), ∃ (x : ℚ_[↑p]), x ≠ 0 ∧ ∀ (i : I), hilbertSym (↑(a i)) x = ep i p) {p : Nat.Primes} (hpT : p ∈ T hε h1) (i : I) : hilbertSym ↑(a i) ↑(A hε h1 * ℓ) = ep i p

theorem HasseMinkowski.Existence.hilbertSym_A_mul_ell_eq_one_of_notMem {I : Type u_1} {a : I → ℤ} {ep : I → Nat.Primes → ℤ} [Finite I] (ha : ∀ (i : I), a i ≠ 0) (hε : ∀ (i : I) (p : Nat.Primes), ep i p = 1 ∨ ep i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, ep i p = 1) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) {p : Nat.Primes} (hpS : p ∉ S a) (hpT : p ∉ T hε h1) (hpℓ : ↑p ≠ ℓ) (i : I) : hilbertSym ↑(a i) ↑(A hε h1 * ℓ) = 1

The product-formula obstruction

The hypotheses of exists_disjoint force the construction x = A · ℓ, but they do not constrain the product of the prescribed values ep i p. The lemma below shows this is a genuine obstruction: if a > 0 and a nonzero rational x realises the sign pattern that is -1 at a single prime p₀ and 1 at every other finite place, then Hilbert reciprocity (whose archimedean factor is 1 because a > 0) is violated. Thus no version of exists_disjoint without a hypothesis ∏ᶠ p, ep i p = 1 can be true.

theorem HasseMinkowski.Existence.not_realizable_of_single_neg {a : ℚ} (ha : 0 < a) {p₀ : Nat.Primes} {x : ℚ} (hx : x ≠ 0) (hother : ∀ (p : Nat.Primes), p ≠ p₀ → hilbertSym ↑a ↑x = 1) (hp₀ : hilbertSym ↑a ↑x = -1) : False

The ℓ-place and the assembly

At the new prime ℓ we use Hilbert reciprocity. Since x = A·ℓ > 0, the archimedean factor is 1, so the product of all finite symbols is 1; all finite places other than ℓ have symbol ep i p (cases S, T, and the unit place), and the product of the ep i p is 1 by h2. Hence the symbol at ℓ is 1, matching ep i ℓ = 1.

theorem HasseMinkowski.Existence.exists_disjoint {I : Type u_2} [Finite I] (a : I → ℤ) (ha : ∀ (i : I), a i ≠ 0) (εp : I → Nat.Primes → ℤ) (hε : ∀ (i : I) (p : Nat.Primes), εp i p = 1 ∨ εp i p = -1) (h1 : ∀ (i : I), ∀ᶠ (p : Nat.Primes) in Filter.cofinite, εp i p = 1) (h2 : ∀ (i : I), ∏ᶠ (p : Nat.Primes), εp i p = 1) (h3 : ∀ (p : Nat.Primes), ∃ (x : ℚ_[↑p]), x ≠ 0 ∧ ∀ (i : I), hilbertSym (↑(a i)) x = εp i p) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓA : ℓ ≡ A hε h1 [MOD M a]) (hℓgt : ∀ s ∈ S a ∪ T hε h1, ↑s < ℓ) : ∃ (x : ℚ), x ≠ 0 ∧ ∀ (i : I) (p : Nat.Primes), hilbertSym ↑(a i) ↑x = εp i p

WP3.2: the general existence theorem

We now drop the disjointness assumption. The proof reduces a to squarefree integers, approximates the local realisations by a rational x' whose quotients are local squares, shifts the prescription by (α i, x'), and applies the disjoint-case exists_disjoint to the shifted prescription.

theorem HasseMinkowski.Existence.hilbertSym_eq_one_or_neg_one {k : Type u_2} [Field k] {a b : k} (ha : a ≠ 0) (hb : b ≠ 0) : hilbertSym a b = 1 ∨ hilbertSym a b = -1

theorem HasseMinkowski.Existence.hilbertSym_mul_sq_left {k : Type u_2} [Field k] {a s b : k} (hs : s ≠ 0) : hilbertSym (a * s ^ 2) b = hilbertSym a b

theorem HasseMinkowski.Existence.exists_rat_local_squares (S : Finset Nat.Primes) (hS : S.Nonempty) (x : (p : ↥S) → ℚ_[↑↑p]) (hx : ∀ (p : ↥S), x p ≠ 0) {r : ℝ} (hr : r ≠ 0) : ∃ (x' : ℚ), x' ≠ 0 ∧ (0 < r ↔ 0 < ↑x') ∧ ∀ (p : Nat.Primes) (hp : p ∈ S), IsSquare (↑x' / x ⟨p, hp⟩)

theorem HasseMinkowski.Existence.hilbertSym_cast_eq {k : Type u_2} [Field k] (n : ℤ) (q : ℚ) : hilbertSym ↑↑n ↑q = hilbertSym ↑n ↑q

theorem HasseMinkowski.Existence.exists_rat_hilbertSym {I : Type u_2} [Finite I] (a : I → ℚ) (ha : ∀ (i : I), a i ≠ 0) (ε : I → Nat.Primes → ℤ) (εR : I → ℤ) (h1 : ∀ (i : I), {p : Nat.Primes | ε i p ≠ 1}.Finite) (h2 : ∀ (i : I), (∏ᶠ (p : Nat.Primes), ε i p) * εR i = 1) (h3 : ∀ (p : Nat.Primes), ∃ (x : ℚ_[↑p]), x ≠ 0 ∧ ∀ (i : I), hilbertSym (↑(a i)) x = ε i p) (h3R : ∃ (x : ℝ), x ≠ 0 ∧ ∀ (i : I), hilbertSym (↑(a i)) x = εR i) : ∃ (x : ℚ), x ≠ 0 ∧ (∀ (i : I) (p : Nat.Primes), hilbertSym ↑(a i) ↑x = ε i p) ∧ ∀ (i : I), hilbertSym ↑(a i) ↑x = εR i