WP5 toolkit: diagonal Hasse–Minkowski for rank ≥ 5

This file collects the two "one-step" tools of the rank-n ≥ 5 induction of Serre IV.2 (see Plan-v3.md §WP5). The final rank ≥ 5 theorem is proved elsewhere; here we supply

• WP5.1 — over an odd prime, a ternary diagonal form whose three weights are p-adic units is isotropic, and hence so is any diagonal form with at least three unit weights;
• WP5.2 — the openness of the nonzero square classes of ℝ and ℚ_[p] (a number close enough to a nonzero a₀ has a / a₀ a square), and the vector form of weak approximation for ℚ (a rational vector can be found close to prescribed local vectors).

The rank-three criterion of RankCriteria.lean together with hilbertSym_padicInt_units turns the local isotropy into the vanishing of a Hilbert symbol of two p-adic units.

WP5.1 — three unit weights over an odd prime

theorem HasseMinkowski.isotropic_weightedSumSquares_three_units (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (u : Fin 3 → ℤ_[p]ˣ) : (QuadraticMap.weightedSumSquares ℚ_[p] fun (i : Fin 3) => ↑↑(u i)).Isotropic

theorem HasseMinkowski.isotropic_of_three_units (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) {ι : Type u_1} [Fintype ι] {w : ι → ℚ_[p]} (u : Fin 3 ↪ ι) (hu : ∀ (j : Fin 3), ∃ (v : ℤ_[p]ˣ), ↑↑v = w (u j)) : (QuadraticMap.weightedSumSquares ℚ_[p] w).Isotropic

theorem HasseMinkowski.isotropic_of_three_units_int (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) {ι : Type u_1} [Fintype ι] {w : ι → ℤ_[p]} (u : Fin 3 ↪ ι) (hu : ∀ (j : Fin 3), IsUnit (w (u j))) : (QuadraticMap.weightedSumSquares ℚ_[p] fun (i : ι) => ↑(w i)).Isotropic

WP5.2 — openness of square classes and vector approximation

theorem HasseMinkowski.isSquare_div_of_close_real {a₀ a : ℝ} (h₀ : a₀ ≠ 0) (h : ‖a - a₀‖ < ‖a₀‖) : IsSquare (a / a₀)

theorem HasseMinkowski.isSquare_div_of_close_padic (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) {a₀ a : ℚ_[p]} (h₀ : a₀ ≠ 0) (h : ‖a - a₀‖ < ‖a₀‖) : IsSquare (a / a₀)

theorem HasseMinkowski.isSquare_div_of_close_padic_two {a₀ a : ℚ_[2]} (h₀ : a₀ ≠ 0) (h : ‖a - a₀‖ < 2 ^ (-2) * ‖a₀‖) : IsSquare (a / a₀)

theorem HasseMinkowski.factPrimeOfPrimesHighRank (p : Nat.Primes) : Fact (Nat.Prime ↑p)

theorem HasseMinkowski.exists_rat_close_vec {S : Finset Nat.Primes} (x : (p : ↥S) → Fin 2 → ℚ_[↑↑p]) : ∃ (q : Fin 2 → ℚ), ∀ (p : ↥S), ‖x p 0 - ↑(q 0)‖ < 1 ∧ ‖x p 1 - ↑(q 1)‖ < 1

The rank-four input of the high-rank induction

The rank-n ≥ 5 induction of Serre IV.2 bottoms out at rank 4, so HighRank.lean is stated relative to the following Prop, which is exactly the diagonal rank-four Hasse–Minkowski theorem that RankFour.lean (WP4.2) proves. Keeping it as an explicit hypothesis lets the high-rank induction be developed and checked independently of the rank-four proof.

def HasseMinkowski.RankFourDiagonalHM : Prop

Diagonal rank-four Hasse–Minkowski over ℚ: a diagonal rank-four form with nonzero rational weights that is isotropic over every p-adic completion and over ℝ is isotropic over ℚ. This is the WP4.2 statement, recorded as a Prop so that the rank-≥ 5 induction can be stated against it.

Equations

• One or more equations did not get rendered due to their size.

WP5.3 — algebraic splitting of a weighted sum of squares

The induction writes ⟨w₀, …, w_{n-1}⟩ as ⟨w₀, w₁⟩ ⊥ (w₂, …, w_{n-1}). These lemmas realise that split on the level of vectors, so that local isotropy of the big form can be read off by prod_isotropic_iff.

theorem HasseMinkowski.sum_fin_add_two {α : Type u_1} [AddCommMonoid α] (m : ℕ) (f : Fin (m + 2) → α) : ∑ i : Fin (m + 2), f i = f 0 + f 1 + ∑ j : Fin m, f j.succ.succ

theorem HasseMinkowski.wss_add_two_val {K : Type u_1} [CommSemiring K] (m : ℕ) (w v : Fin (m + 2) → K) : (QuadraticMap.weightedSumSquares K w) v = (QuadraticMap.weightedSumSquares K ![w 0, w 1]) ![v 0, v 1] + (QuadraticMap.weightedSumSquares K fun (j : Fin m) => w j.succ.succ) fun (j : Fin m) => v j.succ.succ

theorem HasseMinkowski.prod_isotropic_of_wss {K : Type u_1} [CommSemiring K] (m : ℕ) (w : Fin (m + 2) → K) (hiso : (QuadraticMap.weightedSumSquares K w).Isotropic) : ((QuadraticMap.weightedSumSquares K ![w 0, w 1]).prod (QuadraticMap.weightedSumSquares K fun (j : Fin m) => w j.succ.succ)).Isotropic

theorem HasseMinkowski.wss_tail_isotropic {K : Type u_1} [CommSemiring K] (m : ℕ) (w : Fin (m + 2) → K) (hiso : (QuadraticMap.weightedSumSquares K fun (j : Fin m) => w j.succ.succ).Isotropic) : (QuadraticMap.weightedSumSquares K w).Isotropic

theorem HasseMinkowski.nondegenerate_wss_of_ne {K : Type u_1} [Field K] [Invertible 2] {ι : Type u_2} [Fintype ι] {w : ι → K} (hw : ∀ (i : ι), w i ≠ 0) : QuadraticMap.Nondegenerate

theorem HasseMinkowski.exists_local_common_value {K : Type u_1} [Field K] [Invertible 2] {m : ℕ} [NeZero m] {w : Fin (m + 2) → K} (hw : ∀ (i : Fin (m + 2)), w i ≠ 0) (hiso : (QuadraticMap.weightedSumSquares K w).Isotropic) : ∃ (a : K), a ≠ 0 ∧ (QuadraticMap.weightedSumSquares K ![w 0, w 1]).represents a ∧ (QuadraticMap.weightedSumSquares K fun (j : Fin m) => w j.succ.succ).represents (-a)

theorem HasseMinkowski.exists_rat_close_vec' {S : Finset Nat.Primes} {ε : ℝ} (hε : 0 < ε) (xr : Fin 2 → ℝ) (x : (p : ↥S) → Fin 2 → ℚ_[↑↑p]) : ∃ (q : Fin 2 → ℚ), (∀ (i : Fin 2), ‖xr i - ↑(q i)‖ < ε) ∧ ∀ (p : ↥S) (i : Fin 2), ‖x p i - ↑(q i)‖ < ε

theorem HasseMinkowski.exists_padicUnit_of_norm_eq_one {p : ℕ} [Fact (Nat.Prime p)] {x : ℚ_[p]} (h : ‖x‖ = 1) : ∃ (u : ℤ_[p]ˣ), ↑↑u = x

WP5.3 — the quantitative closeness bound

theorem HasseMinkowski.wss_pair_close {K : Type u_1} [NormedField K] {w x q : Fin 2 → K} {ε B : ℝ} (h2 : ‖2‖ ≤ 2) (hq : ∀ (i : Fin 2), ‖q i - x i‖ ≤ ε) (hx : ∀ (i : Fin 2), ‖x i‖ ≤ B) : ‖(QuadraticMap.weightedSumSquares K w) q - (QuadraticMap.weightedSumSquares K w) x‖ ≤ (‖w 0‖ + ‖w 1‖) * (ε * (ε + 2 * B))

WP5.3 — the finite set of bad primes

noncomputable def HasseMinkowski.smallPrimes {ι : Type u_1} [Fintype ι] (w : ι → ℚ) : Finset Nat.Primes

The finite set of primes dividing the numerator or denominator of some weight, together with 2. Off this set every weight is a p-adic unit.

Equations

• One or more equations did not get rendered due to their size.

theorem HasseMinkowski.notMem_smallPrimes {ι : Type u_1} [Fintype ι] {w : ι → ℚ} (hw : ∀ (i : ι), w i ≠ 0) {p : Nat.Primes} (hp : p ∉ smallPrimes w) (i : ι) : ¬↑p ∣ (w i).num.natAbs ∧ ¬↑p ∣ (w i).den

theorem HasseMinkowski.norm_eq_one_of_notMem_smallPrimes {ι : Type u_1} [Fintype ι] {w : ι → ℚ} (hw : ∀ (i : ι), w i ≠ 0) {p : Nat.Primes} (hp : p ∉ smallPrimes w) (i : ι) : ‖↑(w i)‖ = 1

WP5.3 — base change and the rank-lowering assembly

theorem HasseMinkowski.wss_cast_val {K : Type u_1} [CommSemiring K] [Algebra ℚ K] (v z : Fin 2 → ℚ) : (algebraMap ℚ K) ((QuadraticMap.weightedSumSquares ℚ v) z) = (QuadraticMap.weightedSumSquares K fun (i : Fin 2) => (algebraMap ℚ K) (v i)) fun (i : Fin 2) => (algebraMap ℚ K) (z i)

theorem HasseMinkowski.isotropic_wss_neg {K : Type u_1} [Field K] {m : ℕ} {w : Fin m → K} (h : (QuadraticMap.weightedSumSquares K w).Isotropic) : (QuadraticMap.weightedSumSquares K fun (j : Fin m) => -w j).Isotropic

theorem HasseMinkowski.represents_neg_of_represents_neg_of_square {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {av A : K} (hA : A ≠ 0) (hav : av ≠ 0) (h : QuadraticMap.represents Q (-av)) (hs : IsSquare (A / av)) : QuadraticMap.represents Q (-A)

theorem HasseMinkowski.wss_cons_neg_isotropic_of_represents {K : Type u_1} [Field K] {m : ℕ} (c : K) {w : Fin m → K} (h : (QuadraticMap.weightedSumSquares K w).represents (-c)) : (QuadraticMap.weightedSumSquares K (Fin.cons (-c) fun (j : Fin m) => -w j)).Isotropic

theorem HasseMinkowski.wss_cons_neg_isotropic_of_tail {K : Type u_1} [Field K] {m : ℕ} (c : K) {w : Fin m → K} (h : (QuadraticMap.weightedSumSquares K fun (j : Fin m) => -w j).Isotropic) : (QuadraticMap.weightedSumSquares K (Fin.cons (-c) fun (j : Fin m) => -w j)).Isotropic

theorem HasseMinkowski.wss_cons_neg_isotropic_of_represents_rat {K : Type u_1} [Field K] {m : ℕ} (A : ℚ) {v : Fin m → ℚ} (h : (QuadraticMap.weightedSumSquares K fun (j : Fin m) => ↑(v j)).represents (-↑A)) : (QuadraticMap.weightedSumSquares K fun (i : Fin (m + 1)) => ↑(Fin.cons (-A) (fun (j : Fin m) => -v j) i)).Isotropic

theorem HasseMinkowski.wss_cons_neg_isotropic_of_tail_rat {K : Type u_1} [Field K] {m : ℕ} (A : ℚ) {v : Fin m → ℚ} (h : (QuadraticMap.weightedSumSquares K fun (j : Fin m) => -↑(v j)).Isotropic) : (QuadraticMap.weightedSumSquares K fun (i : Fin (m + 1)) => ↑(Fin.cons (-A) (fun (j : Fin m) => -v j) i)).Isotropic

theorem HasseMinkowski.isSquare_div_of_close_padic' (p : ℕ) [Fact (Nat.Prime p)] {a₀ a : ℚ_[p]} (h₀ : a₀ ≠ 0) (h : ‖a - a₀‖ < (if p = 2 then 2 ^ (-2) else 1) * ‖a₀‖) : IsSquare (a / a₀)

theorem HasseMinkowski.exists_rat_value_close {m : ℕ} (w : Fin (m + 2) → ℚ) {S : Finset Nat.Primes} (xp : (p : ↥S) → Fin 2 → ℚ_[↑↑p]) (av : (p : ↥S) → ℚ_[↑↑p]) (hav : ∀ (p : ↥S), av p ≠ 0) (hxpa : ∀ (p : ↥S), (QuadraticMap.weightedSumSquares ℚ_[↑↑p] ![w 0, w 1]) (xp p) = av p) (xr : Fin 2 → ℝ) (ar : ℝ) (har : ar ≠ 0) (hxra : (QuadraticMap.weightedSumSquares ℝ ![w 0, w 1]) xr = ar) : ∃ (q : Fin 2 → ℚ), (QuadraticMap.weightedSumSquares ℚ ![w 0, w 1]) q ≠ 0 ∧ IsSquare (↑((QuadraticMap.weightedSumSquares ℚ ![w 0, w 1]) q) / ar) ∧ ∀ (p : ↥S), IsSquare (↑((QuadraticMap.weightedSumSquares ℚ ![w 0, w 1]) q) / av p)

theorem HasseMinkowski.norm_two_padic_le_two (p : ℕ) [Fact (Nat.Prime p)] : ‖2‖ ≤ 2

The high-rank diagonal input

def HasseMinkowski.RankFiveLeDiagonalHM : Prop

Diagonal Hasse–Minkowski over ℚ in rank n ≥ 5: a diagonal form with nonzero rational weights that is isotropic over every p-adic completion and over ℝ is isotropic over ℚ. This is the WP5.3 statement, recorded as a Prop so that the assembly of hasseMinkowski (WP6.2) can be developed against it while the induction is proved.

Equations

• One or more equations did not get rendered due to their size.

WP5.3 — the rank-lowering induction

theorem HasseMinkowski.diagonal_hm_ge_four (h4 : RankFourDiagonalHM) (k : ℕ) : 4 ≤ k → ∀ (w : Fin k → ℚ), (∀ (i : Fin k), w i ≠ 0) → (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], (QuadraticMap.weightedSumSquares ℚ_[p] fun (i : Fin k) => ↑(w i)).Isotropic) → (QuadraticMap.weightedSumSquares ℝ fun (i : Fin k) => ↑(w i)).Isotropic → (QuadraticMap.weightedSumSquares ℚ w).Isotropic

theorem HasseMinkowski.diagonal_hm_five_le (h4 : RankFourDiagonalHM) {n : ℕ} : 5 ≤ n → ∀ (w : Fin n → ℚ), (∀ (i : Fin n), w i ≠ 0) → (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], (QuadraticMap.weightedSumSquares ℚ_[p] fun (i : Fin n) => ↑(w i)).Isotropic) → (QuadraticMap.weightedSumSquares ℝ fun (i : Fin n) => ↑(w i)).Isotropic → (QuadraticMap.weightedSumSquares ℚ w).Isotropic

theorem HasseMinkowski.rankFiveLeDiagonalHM (h4 : RankFourDiagonalHM) : RankFiveLeDiagonalHM