Rank criteria for the Hasse–Minkowski invariant

This file ports the local representability criteria of HassePrinciple's QuadraticForm/HasseMinkowskiInvariant.lean, connecting the discriminant of a quadratic form with the Hasse–Minkowski invariant:

• over a rank-two space, a nondegenerate form Q represents a exactly when (a, -discr Q) = ε(Q);
• over a rank-three space, a nondegenerate form Q is isotropic exactly when (-1, -discr Q) = ε(Q).

The proofs rest on the rank-three isotropy criterion weightedSumSquares_isotropic_iff_hilbertSym_eq_one and the Hilbert-symbol square-class computation hilbertSym_mul_mul, both of which are proved unconditionally here.

The well-definedness of hasseMinkowskiInv (that equivalent diagonal forms have the same invariant) is not available in this project, so no theorem at the level of that form-level invariant is stated. The invariant-free (diagonal) forms of the criteria are stated and proved with hasseMinkowskiInvAux and need no such hypothesis.

Provenance

This file is a derived work. It is based on QuadraticForm/HasseMinkowskiInvariant.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.

theorem QuadraticMap.Equivalent.isotropic_iff {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (h : Q₁.Equivalent Q₂) : HasseMinkowski.Isotropic Q₁ ↔ HasseMinkowski.Isotropic Q₂

Hilbert-symbol helpers

theorem HasseMinkowski.hilbertSym_eq_one_iff {k : Type u_1} [Field k] {a b : k} (ha : a ≠ 0) (hb : b ≠ 0) : hilbertSym a b = 1 ↔ ∃ (z : k) (x : k) (y : k), (z, x, y) ≠ (0, 0, 0) ∧ z ^ 2 - a * x ^ 2 - b * y ^ 2 = 0

theorem HasseMinkowski.hilbertSym_right_neg_self {k : Type u_1} [Field k] {a : k} (ha : a ≠ 0) : hilbertSym a (-a) = 1

theorem HasseMinkowski.hilbertSym_neg_one_mul_self {k : Type u_1} [Field k] {a : k} (ha : a ≠ 0) : hilbertSym (-1) a * hilbertSym (-1) a = 1

theorem HasseMinkowski.hilbertSym_self {k : Type u_1} [Field k] [HasBilinHilbertSym k] {a : k} : hilbertSym a a = hilbertSym a (-1)

theorem HasseMinkowski.hilbertSym_self_eq_left_neg_one {k : Type u_1} [Field k] [HasBilinHilbertSym k] {a : k} : hilbertSym a a = hilbertSym (-1) a

theorem HasseMinkowski.hilbertSym_left_neg_mul {k : Type u_1} [Field k] [HasBilinHilbertSym k] {a b : k} : hilbertSym (-(a * b)) b = hilbertSym a b

theorem HasseMinkowski.hilbertSym_mul_mul {k : Type u_1} [Field k] [HasBilinHilbertSym k] {a b c : k} : hilbertSym (c * a) (c * b) = hilbertSym c (-(a * b)) * hilbertSym a b

The rank-three isotropy criterion

theorem HasseMinkowski.weightedSumSquares_isotropic_iff_hilbertSym_eq_one {k : Type u_1} [Field k] (a b c : k) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : (QuadraticMap.weightedSumSquares k ![a, b, c]).Isotropic ↔ hilbertSym (-c * a) (-c * b) = 1

theorem HasseMinkowski.weightedSumSquares_isotropic_iff_hilbertSym_eq_one' {k : Type u_1} [Field k] (a b : k) (ha : a ≠ 0) (hb : b ≠ 0) : (QuadraticMap.weightedSumSquares k ![a, b, 1]).Isotropic ↔ hilbertSym (-a) (-b) = 1

theorem HasseMinkowski.weightedSumSquares_units_coe {k : Type u_1} [Field k] {ι : Type u_2} [Fintype ι] (w : ι → kˣ) : QuadraticMap.weightedSumSquares k w = QuadraticMap.weightedSumSquares k fun (i : ι) => ↑(w i)

The rank-three criterion for the Hasse–Minkowski invariant

theorem HasseMinkowski.hilbertSym_mul_mul_neg {k : Type u_1} [Field k] [HasBilinHilbertSym k] (a b c : k) : hilbertSym (-c * a) (-c * b) = hilbertSym (-1) (-(a * b * c)) * (hilbertSym a b * hilbertSym a c * hilbertSym b c)

theorem HasseMinkowski.mul_eq_one_iff_eq_of_signs {x y : ℤ} (hx : x = 1 ∨ x = -1) (hy : y = 1 ∨ y = -1) : x * y = 1 ↔ x = y

theorem HasseMinkowski.represents_zero_iff_of_rank_three_diag {k : Type u_1} [Field k] [HasBilinHilbertSym k] (a b c : kˣ) : (QuadraticMap.weightedSumSquares k ![a, b, c]).Isotropic ↔ hilbertSym (-1) (-(↑a * ↑b * ↑c)) = hasseMinkowskiInvAux ![a, b, c]