Linearity-of-source helpers for subtractProjection and reduceAgainstBasis. These let later proofs pull the reconstruction sum across the reduction.

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.