hex

25.6. Cross-references🔗

HexGramSchmidt builds on the matrix, row-reduction, determinant, and Bareiss libraries and underpins HexLLL:

  • HexMatrix supplies the Hex.Matrix representation and the row operations (Hex.Matrix.rowAdd, Hex.Matrix.rowSwap) that the update formulas reason about. The orthogonalization here is built entirely on that representation.

  • HexRowReduce supplies Hex.Matrix.IsRowReduced and its row-echelon contracts, used by the integer Bareiss-Gram invariant, while HexDeterminant and HexBareiss supply the determinant and fraction-free elimination layers used by the integer data.

  • HexGramSchmidtMathlib re-expresses this executable theory as theorems about Mathlib's InnerProductSpace.gramSchmidt on EuclideanSpace and Mathlib's _root_.Matrix determinants. HexGramSchmidt itself is Mathlib-free.

  • HexLLL consumes the integer data (the Gram determinants and scaled coefficients) and the exact update formulas to drive lattice reduction in integer arithmetic.