6.8. Cross-references🔗

HexLLL's substantive dependency is HexGramSchmidt, with its correctness proofs in HexLLLMathlib:

• HexGramSchmidt supplies the integer Gram-Schmidt representation (Hex.GramSchmidt.Int.independent, the scaled coefficients, and the leading Gram determinants) on which both the reducedness predicates and the integer checkers are defined. Through it, HexLLL rests transitively on the fraction-free integer determinant libraries HexBareiss, HexDeterminant, and HexRowReduce.

• HexLLLMathlib carries the soundness theorems. lllReducedInt_sound and lllReducedCheck_sound relate the integer checkers to Hex.isLLLReduced, and certCheck_sound combines those with Hex.Matrix.sameLatticeCert_sound into the property triple (same lattice, independence, reducedness) that the certified-dispatch path of Hex.lll relies on. HexLLL itself is Mathlib-free.