26.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 : ℕ} (b : Hex.Matrix ℤ n m)
  (v : Vector ℤ m) : Prop
Hex.Matrix.memLattice {n m : ℕ}
  (b : Hex.Matrix ℤ n m)
  (v : Vector ℤ m) : Prop

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

def

Hex.Matrix.independent {n m : ℕ} (b : Hex.Matrix ℤ n m) : Prop
Hex.Matrix.independent {n m : ℕ}
  (b : Hex.Matrix ℤ 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 : ℕ} (b : Hex.Matrix ℤ n m) (δ η : ℚ) : Prop
Hex.isLLLReduced {n m : ℕ}
  (b : Hex.Matrix ℤ n m) (δ η : ℚ) : 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 : ℕ} (b : Hex.Matrix ℤ n m)
  {δ η₁ η₂ : ℚ} (hη₁ : 0 ≤ η₁) (hle : η₁ ≤ η₂)
  (hred : Hex.isLLLReduced b δ η₁) : Hex.isLLLReduced b δ η₂
Hex.Internal.isLLLReduced.mono_η {n m : ℕ}
  (b : Hex.Matrix ℤ n m) {δ η₁ η₂ : ℚ}
  (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 : ℕ} (b : Hex.Matrix ℤ n m)
  {δ η : ℚ} (hli : b.independent) (hred : Hex.isLLLReduced b δ η)
  (hη : 1 / 2 ≤ η) (hδη : η * η < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n)
  {v : Vector ℤ 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 : ℕ} (b : Hex.Matrix ℤ n m)
  {δ η : ℚ} (hli : b.independent)
  (hred : Hex.isLLLReduced b δ η)
  (hη : 1 / 2 ≤ η) (hδη : η * η < δ)
  (hδ' : δ ≤ 1) (hn : 1 ≤ n)
  {v : Vector ℤ m} (hv : b.memLattice v)
  (hv' : v ≠ 0) :
  ↑(b.row ⟨0, ⋯⟩).normSq ≤
    (1 / (δ - η * η)) ^ (n - 1) *
      ↑v.normSq

LLL short-vector 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. The proof combines the telescoping Gram-Schmidt inequality with the lower bound on the smallest Gram-Schmidt vector contained in the lattice.