hex-lll-mathlib

Part of hex, a computer algebra library for Lean 4.

hex-lll-mathlib relates the executable integer lattice operations from hex-lll to Mathlib submodules and Euclidean norms. Its principal theorem says that the first row returned by Hex.lll is short relative to every nonzero vector of the input lattice.

Quickstart

[[require]]
name = "hex-lll-mathlib"
git = "https://github.com/leanprover/hex-lll-mathlib.git"
rev = "main"

import HexLLLMathlib

open HexLLLMathlib

#check @lll_first_row_norm_sq_le
#check @lllNative_first_row_norm_sq_le
#check @latticeSubmodule
#check @lll_mem_latticeSubmodule_iff

Functionality

latticeSubmodule b is the ℤ-submodule generated by the rows of the executable matrix b. The membership theorems identify it with Hex.Matrix.memLattice.

intRowToEuclidean and intVectorToEuclidean map integer coordinates into EuclideanSpace ℝ (Fin m). Their norm theorems convert the executable squared norm to Mathlib's norm.

The package also proves soundness of lllReduced, lllReducedInterval, lllReducedCheck, and certCheck.

Verification

For an independent basis and 121/400 < δ ≤ 1, lll_first_row_norm_sq_le bounds the squared norm of the first reduced row by

(1 / (δ - 121/400))^(n - 1)

times the squared norm of any nonzero lattice vector. The corresponding theorem for lllNative uses the tighter classical denominator δ - 1/4. The lattice-preservation theorems state that both returned bases generate exactly the input submodule.

See the SPEC for the theorem map and precise hypotheses.

Contributing

Development happens in the hex-dev monorepo, not in this published mirror. Contributions are welcome as pull requests to the SPEC/ directory: describe the behavior you want and leave the implementation to the maintainer.