The HexLLLMathlib library identifies the executable HexLLL lattice surface with Mathlib's linear-algebra API.

This library exposes a Submodule ℤ model of the integer row lattice generated by an executable Hex.Matrix, together with the equivalence between Mathlib-side submodule membership and the executable Hex.Matrix.memLattice predicate used by hex-lll, and the Euclidean short-vector guarantee for Hex.lll.