theorem Hex.GramSchmidt.normSq_vecMul_of_orthogonal {n m : Nat} (rows : Matrix Rat n m) (coeffs : Vector Rat n) (horth : ∀ (i j : Fin n), i ≠ j → (rows.row i).dotProduct (rows.row j) = 0) : (Matrix.vecMul coeffs rows).normSq = Fin.foldl n (fun (total : Rat) (i : Fin n) => total + coeffs[i] * coeffs[i] * (rows.row i).normSq) 0

The squared norm of a linear combination of pairwise orthogonal rows is the sum of the coefficient squares times the row squared norms.

theorem Hex.GramSchmidt.vecMul_normSq_ge_of_orthogonal_coeff_sq_ge_one {n m : Nat} (rows : Matrix Rat n m) (coeffs : Vector Rat n) (k : Fin n) (horth : ∀ (i j : Fin n), i ≠ j → (rows.row i).dotProduct (rows.row j) = 0) (hcoeff : 1 ≤ coeffs[k] * coeffs[k]) : (rows.row k).normSq ≤ (Matrix.vecMul coeffs rows).normSq

Orthogonal row-combination lower bound. If the rows of rows are pairwise orthogonal and the coefficient at k has square at least 1, then the squared norm of the whole row combination is at least the squared norm of row k.

theorem Hex.GramSchmidt.one_le_intCast_mul_self_of_ne_zero (z : Int) (hz : z ≠ 0) : 1 ≤ ↑z * ↑z

A nonzero integer coefficient has rational square at least 1.