Assembly of the Hasse–Minkowski principle over ℚ (WP6)

This file assembles the local–global principle for quadratic forms over ℚ from the rank-by-rank inputs proved in the earlier layers:

• isotropic_of_rank_one / isotropic_of_rank_two (RankTwo.lean),
• isotropic_of_rank_three' (Legendre.lean),
• rankFourDiagonalHM (RankFour.lean, the diagonal rank-four case),
• RankFiveLeDiagonalHM (HighRank.lean, diagonal rank ≥ 5).

The two diagonal ingredients RankFourDiagonalHM (RankFour.lean) and RankFiveLeDiagonalHM (the WP5.3 induction, HighRank.lean) enter as explicit hypotheses of the conditional hasseMinkowski_of and meyer_of; the unconditional hasseMinkowski and meyer below specialise them with rankFourDiagonalHM and rankFiveLeDiagonalHM rankFourDiagonalHM.

Main results

• isotropic_of_radical_ne_bot (WP6.1): a form with nonzero radical is isotropic, because a radical vector x has associated Q x x = 0 and associated Q x x = 2 * Q x.
• hasseMinkowski_of (WP6.2): Isotropic Q ↔ EverywhereLocallyIsotropic Q.
• meyer_of (WP6.3): an indefinite form of rank ≥ 5 over ℚ is isotropic.

WP6.1 — a degenerate form is isotropic

In characteristic different from 2 a nonzero vector of the radical satisfies Q x = 0 (it is orthogonal to itself, and associated Q x x = 2 * Q x). This is the "degenerate Q" case of the Hasse–Minkowski principle.

theorem HasseMinkowski.isotropic_of_radical_ne_bot {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (h : QuadraticMap.radical Q ≠ ⊥) : Isotropic Q

WP6.2 — the rank-by-rank dispatch on the diagonalized form

A nondegenerate form is equivalent to a weighted sum of squares ⟨w₀, …, w_{n-1}⟩ with nonzero rational weights. The local hypotheses of h4 and h5 are exactly the isotropy of this diagonal form at every place, so we dispatch on n = finrank ℚ V: ranks 0, 1, 2, 3 are the proved layer results, rank 4 is h4, and rank ≥ 5 is h5.

theorem HasseMinkowski.hasseMinkowski_of (h4 : RankFourDiagonalHM) (h5 : RankFiveLeDiagonalHM) {V : Type u_2} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (Q : QuadraticForm ℚ V) : Isotropic Q ↔ EverywhereLocallyIsotropic Q

WP6.3 — Meyer's theorem

An indefinite real form of rank ≥ 5 is isotropic over ℝ; over each ℚ_[p] every form in at least five variables is isotropic (isotropic_weightedSumSquares_of_five_le), and these local data feed WP6.2.

theorem HasseMinkowski.meyer_of (h4 : RankFourDiagonalHM) (h5 : RankFiveLeDiagonalHM) {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (Q : QuadraticForm ℚ V) (hrank : 5 ≤ Module.finrank ℚ V) (hind : Indefinite (QuadraticForm.baseChange ℝ Q)) : Isotropic Q

The unconditional theorems

With RankFourDiagonalHM proved in RankFour.lean and its rank-≥ 5 counterpart in HighRank.lean, the conditional theorems above specialise to the targets:

theorem HasseMinkowski.hasseMinkowski {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (Q : QuadraticForm ℚ V) : Isotropic Q ↔ EverywhereLocallyIsotropic Q

theorem HasseMinkowski.meyer {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (Q : QuadraticForm ℚ V) (h : 5 ≤ Module.finrank ℚ V) (hind : Indefinite (QuadraticForm.baseChange ℝ Q)) : Isotropic Q