Mathlib-side determinantal theory for the integer Gram-Schmidt surface of hex-gram-schmidt.

This module relates the executable leading integer Gram determinant gramDet to products of squared norms of the orthogonal Gram-Schmidt basis rows. Its spine is a rational column-operation reduction from leadingGramMatrixInt (via the interpolating progressMatrix, the triangular auxMatrix, and the Int → Rat cast law det_intCast) to the diagonal norm-squared matrix, giving gramDet_succ_rat and leadingGramMatrixInt_det_nonneg. Along the way it builds the Cramer machinery (scaledCoeffMatrix solved through the chosen originalProjectionCoords) that the sibling module uses to read off the Gram-Schmidt coefficients coeffs.

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.

Helpers for gramDet_eq_prod_normSq_core

The remaining theorems below build the rational column-operation reduction from the leading Gram matrix to the diagonal Gram-Schmidt norm-squared matrix, plus the integer→rational cast law for det.

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

The k-leading Gram determinant equals, as a rational, the product of the squared Gram-Schmidt norms of the first k basis vectors (gramSchmidtNormProduct b k). Public wrapper over gramDet_eq_prod_normSq_core.

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

For an independent integer matrix b, every nonempty leading Gram determinant is strictly positive (0 < k ≤ n). Public wrapper over gramDet_pos_core.

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 basis vector is the ratio of consecutive leading Gram determinants d_{k+1} / d_k, the standard telescoping identity. Public wrapper over basis_normSq_core.

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]).