6.1. Introduction🔗

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

HexLLL reduces an integer lattice basis. Given the rows of a Hex.Matrix over Int, it produces a new basis for the same lattice made of short, nearly orthogonal vectors (the LLL guarantee). Its first row is a provably short lattice vector, which is what the downstream factorization path consumes: the BHKS van Hoeij recombination step in hex-berlekamp-zassenhaus reconstructs true factors from short vectors of a knapsack lattice.

On adversarial worst-case input the reducers diverge sharply in cost. These are the five benchmarked reducers on fplll's Ajtai-style gen_trg bases, whose steeply decreasing profile forces a Θ(d² log B) swap count:

The exact integer reducers (Lean's lllNative and the verified Isabelle extraction) blow up ~d⁷. The certified path (an fpLLL candidate checked by a verified Lean checker) stays cheap, near raw floating-point speed. The performance comparison below describes every curve and all six input families.

The library splits computation from proof. The public reducer can accelerate through an optional external fpLLL provider (fast, untrusted numerics), but no proof depends on those numerics being correct. Every external candidate is fed through a verified integer checker. Only a basis the checker accepts is returned, and the checker's soundness theorem (proved on the Mathlib side) turns that acceptance into the mathematical guarantee. When no external candidate certifies, the exact all-integer reducer lllNative runs directly, and its guarantee is proved outright.

HexLLL is Mathlib-free. It takes the Gram-Schmidt machinery underlying both the predicates and the checkers from HexGramSchmidt, which computes the leading integer Gram determinants by fraction-free (Bareiss) elimination and so rests in turn on HexBareiss, HexDeterminant, and HexRowReduce.