6.2. Lattices and reducedness🔗

A lattice is the set of integer combinations of the basis rows. Membership and independence are the two structural predicates. Both are propositions about the exact integer data, never about the numerics.

def

Hex.Matrix.memLattice {n m : Nat} (b : Hex.Matrix Int n m)
  (v : Vector Int m) : Prop
Hex.Matrix.memLattice {n m : Nat}
  (b : Hex.Matrix Int n m)
  (v : Vector Int m) : Prop

v lies in the integer lattice generated by the rows of b.

def

Hex.Matrix.independent {n m : Nat} (b : Hex.Matrix Int n m) : Prop
Hex.Matrix.independent {n m : Nat}
  (b : Hex.Matrix Int n m) : Prop

The rows of b are linearly independent, witnessed by positivity of each executable leading Gram determinant.

The central specification is the (δ, η)-reducedness predicate. It is the classical LLL definition phrased over the exact rational Gram-Schmidt coefficients of the integer GramSchmidt.Int representation: a size-reduction bound η on every below-diagonal coefficient, together with the Lovász condition at each adjacent pair, controlled by the parameter δ.

def

Hex.isLLLReduced {n m : Nat} (b : Hex.Matrix Int n m) (δ η : Rat) : Prop
Hex.isLLLReduced {n m : Nat}
  (b : Hex.Matrix Int n m) (δ η : Rat) :
  Prop

A basis is (δ, η)-LLL-reduced when it is size-reduced with bound η (|μ| ≤ η for every below-diagonal entry of the Gram-Schmidt coefficient matrix) and satisfies the Lovasz condition at every adjacent pair. The size-reduction clause is stored in squared form μ² ≤ η², which is equivalent to |μ| ≤ η exactly when η ≥ 0; every consumer supplies 1/2 ≤ η.

Reducedness in this squared-coefficient form relaxes monotonically as the size bound η grows.

theorem

Hex.Internal.isLLLReduced.mono_η {n m : Nat} (b : Hex.Matrix Int n m)
  {δ η₁ η₂ : Rat} (hη₁ : 0 ≤ η₁) (hle : η₁ ≤ η₂)
  (hred : Hex.isLLLReduced b δ η₁) : Hex.isLLLReduced b δ η₂
Hex.Internal.isLLLReduced.mono_η
  {n m : Nat} (b : Hex.Matrix Int n m)
  {δ η₁ η₂ : Rat} (hη₁ : 0 ≤ η₁)
  (hle : η₁ ≤ η₂)
  (hred : Hex.isLLLReduced b δ η₁) :
  Hex.isLLLReduced b δ η₂

Monotonicity of the size-reduction bound: a (δ, η₁)-LLL-reduced basis is also (δ, η₂)-LLL-reduced for any η₂ ≥ η₁ ≥ 0. The Lovász side is unchanged; the size-reduced side relaxes since |μ| ≤ η₁ ≤ η₂ (in squared form, μ² ≤ η₁² ≤ η₂²).

The key theorem is the short-vector bound: in a reduced basis the first row is within an explicit δ/η-dependent factor of the shortest nonzero lattice vector. This is the property downstream callers actually rely on.

theorem

Hex.short_vector_bound_of_size_bound {n m : Nat}
  (b : Hex.Matrix Int n m) {δ η : Rat} (hli : b.independent)
  (hred : Hex.isLLLReduced b δ η) (hη : 1 / 2 ≤ η) (hδη : η * η < δ)
  (hδ' : δ ≤ 1) (hn : 1 ≤ n) {v : Vector Int m} (hv : b.memLattice v)
  (hv' : v ≠ 0) :
  ↑(b.row ⟨0, ⋯⟩).normSq ≤ (1 / (δ - η * η)) ^ (n - 1) * ↑v.normSq
Hex.short_vector_bound_of_size_bound
  {n m : Nat} (b : Hex.Matrix Int n m)
  {δ η : Rat} (hli : b.independent)
  (hred : Hex.isLLLReduced b δ η)
  (hη : 1 / 2 ≤ η) (hδη : η * η < δ)
  (hδ' : δ ≤ 1) (hn : 1 ≤ n)
  {v : Vector Int m} (hv : b.memLattice v)
  (hv' : v ≠ 0) :
  ↑(b.row ⟨0, ⋯⟩).normSq ≤
    (1 / (δ - η * η)) ^ (n - 1) *
      ↑v.normSq

LLL short-vector core inequality, parameterized by the size-reduction bound η. For a (δ, η)-LLL-reduced basis with 1/2 ≤ η, η² < δ ≤ 1, the squared norm of the first row is at most (1 / (δ - η²)) ^ (n - 1) times the squared norm of any nonzero lattice vector. Combines LLLCore.teleBound with the lower bound on the smallest Gram-Schmidt vector contained in the lattice.