16.1. Introduction🔗

Released as hex-gram-schmidt, with the Mathlib correspondence in hex-gram-schmidt-mathlib.

HexGramSchmidt orthogonalizes the rows of a matrix by Gram-Schmidt: from each row it subtracts the projection onto the earlier rows, and returns the orthogonal basis together with the lower-unitriangular matrix of projection coefficients that reconstructs the input. Everything is phrased over Hex.Matrix: operations take and return whole matrices (basis b : Matrix Rat n m, coeffs b : Matrix Rat n n), and rows are addressed by Nat indices with explicit bounds rather than Fin.

The library has two namespaces. Hex.GramSchmidt.Rat orthogonalizes a rational matrix directly. Hex.GramSchmidt.Int works on an integer matrix, and its computable operations — the leading Gram determinants and the integer scaled coefficient matrix — stay entirely in exact integer arithmetic. That is the whole point of the integer namespace: lattice code reads the exact Hex.GramSchmidt.Int.gramDet and Hex.GramSchmidt.Int.scaledCoeffs values and never leaves Int. The orthogonal basis and rational coefficients themselves involve division, which is usually a performance bottleneck, so Hex.GramSchmidt.Rat.basis and Hex.GramSchmidt.Rat.coeffs are noncomputable. The computable determinant operations (Hex.GramSchmidt.Int.gramDet, Hex.GramSchmidt.Int.scaledCoeffs) drive the worked examples below.

HexGramSchmidt is Mathlib-free and depends only on HexMatrix. HexLLL uses it for orthogonalization and the exact-update formulas. See Cross-references.