theorem Hex.GramSchmidt.Int.leadingGramMatrixInt_det_nonneg {n m : ℕ} (b : Matrix ℤ n m) (t : ℕ) (ht : t ≤ n) : 0 ≤ (leadingGramMatrixInt b t ht).det

Leading integer Gram determinants are nonnegative.

theorem Hex.GramSchmidt.Int.gramDet_pos {n m : ℕ} (b : Matrix ℤ n m) (hli : independent b) (k : ℕ) (hk : k ≤ n) (hk' : 0 < k) : 0 < gramDet b k hk

Every nonempty leading Gram determinant of an independent integer matrix is strictly positive.

theorem Hex.GramSchmidt.Int.dot_add_right_rat {m' : ℕ} (u v w : Vector ℚ m') : u.dotProduct (v + w) = u.dotProduct v + u.dotProduct w

Right-side dot product distributes over vector addition.

theorem Hex.GramSchmidt.Int.dot_smul_right_rat {m' : ℕ} (s : ℚ) (u v : Vector ℚ m') : u.dotProduct (s • v) = s * u.dotProduct v

Right-side dot product distributes over scalar multiplication.

theorem Hex.GramSchmidt.Int.gramDet_eq_prod_normSq {n m : ℕ} (b : Matrix ℤ n m) (hli : independent b) (k : ℕ) (hk : k ≤ n) : ↑(gramDet b k hk) = gramSchmidtNormProduct b k hk

For an independent integer matrix, each leading Gram determinant, cast to Rat, equals the product of the squared norms of its Gram-Schmidt basis rows.

theorem Hex.GramSchmidt.Int.gramSchmidtNormProduct_succ {n m : ℕ} (b : Matrix ℤ n m) (k : ℕ) (hk : k + 1 ≤ n) : gramSchmidtNormProduct b (k + 1) hk = gramSchmidtNormProduct b k ⋯ * ((basis b).row ⟨k, ⋯⟩).normSq

One-step extension of gramSchmidtNormProduct: appending the k-th factor multiplies the k-fold product by ((basis b).row ⟨k, _⟩)..normSq This is a Fin.foldl cancellation lemma; positivity of the leading Gram determinant is handled separately by gramDet_pos.

theorem Hex.GramSchmidt.Int.basis_normSq {n m : ℕ} (b : Matrix ℤ n m) (hli : independent b) (k : ℕ) (hk : k < n) : ((basis b).row ⟨k, hk⟩).normSq = ↑(gramDet b (k + 1) ⋯) / ↑(gramDet b k ⋯)

The squared norm of the k-th Gram-Schmidt vector is the ratio of consecutive leading Gram determinants.

theorem Hex.GramSchmidt.Int.gramDet_succ_rat {n m : ℕ} (b : Matrix ℤ n m) (j : ℕ) (hjsuc : j + 1 ≤ n) : ↑(gramDet b (j + 1) hjsuc) = gramSchmidtNormProduct b j ⋯ * ((basis b).row ⟨j, ⋯⟩).normSq

The Gram-determinant succession: (gramDet (j+1) : Rat) factors as (gramSchmidtNormProduct j) * normSq(basis[j]).