theorem Hex.GramSchmidt.Int.gramDetVecEntry_eq_gramDet {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (k : Nat) (hk : k ≤ n) : gramDetVecEntry b.gramMatrix.bareissNoPivotData ⟨k, ⋯⟩ = gramDet b k hk

The no-pivot Bareiss pass over the full Gram matrix records the same leading-prefix determinant as the public gramDet API at every vector slot.

@[simp]

theorem Hex.GramSchmidt.Int.gramDet_zero {n m : Nat} (b : Matrix Int n m) : gramDet b 0 ⋯ = 1

The empty leading Gram determinant is 1: the determinant of the 0 × 0 principal Gram minor. This is the base case anchoring the gramDetVec diagonal recurrence (gramDetVec_eq_gramDet at k = 0).

theorem Hex.GramSchmidt.Int.scaledCoeffs_upper {n m : Nat} (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i < j) : entry (scaledCoeffs b) ⟨i, hi⟩ ⟨j, hj⟩ = 0

The integral scaled Gram-Schmidt coefficient matrix is lower triangular: every strict-upper-triangle entry (i < j) is zero. Callers treating scaledCoeffs as a triangular factor use this to discard above-diagonal terms. Tagged @[grind =] (keyed on the entry (scaledCoeffs b) i j term) so the strict-upper hypothesis i < j is discharged by grind's arithmetic when the vanishing fact is needed.

theorem Hex.GramSchmidt.Int.vecMul_coeffs_apply_eq_of_zero_above {n m : Nat} (b : Matrix Int n m) (c : Vector Int n) (k : Fin n) (hzero_above : ∀ (j : Fin n), ↑k < ↑j → c[j] = 0) : (Matrix.vecMul (Vector.map (fun (x : Int) => ↑x) c) (coeffs b))[k] = ↑c[k]

The k-th entry of the row combination of the Gram-Schmidt coefficient matrix with a cast integer coefficient vector, when all later integer coefficients vanish, equals the cast k-th coefficient.

This is the top Gram-Schmidt coordinate specialization consumed by the lattice norm lower bound: rows below k contribute zero by upper-triangularity, row k contributes one by the diagonal lemma, and rows above k contribute zero because the corresponding integer coefficient vanishes.