5.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 casts an integer matrix to Rat first, and adds computable integer data (the leading Gram determinants and the integer scaled coefficient matrix) that lattice code uses to stay in exact arithmetic. The orthogonal basis and rational coefficients involve division, so Hex.GramSchmidt.Rat.basis and Hex.GramSchmidt.Rat.coeffs are noncomputable. The determinant operations (Hex.GramSchmidt.Int.gramDet, Hex.GramSchmidt.Int.scaledCoeffs) are computable and 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.