The (δ, η)-reducedness predicate isLLLReduced and the short-vector bound short_vector_bound_of_size_bound: a reduced independent basis has a first row no longer than (1 / (δ - η²)) ^ (n - 1) (squared) times any nonzero lattice vector.

def Hex.Internal.LLLCore.basisNormSq {n m : Nat} (basis : Matrix Rat n m) (i : Fin n) : Rat

Recover the squared norm of a Gram-Schmidt basis vector.

Equations

• Hex.Internal.LLLCore.basisNormSq basis i = (basis.row i).normSq

def Hex.isLLLReduced {n m : Nat} (b : 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 ≤ η.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Internal.LLLCore.basisNormSq_nonneg {n m : Nat} (basis : Matrix Rat n m) (i : Fin n) : 0 ≤ basisNormSq basis i

The squared norm of any basis row is nonnegative, being a sum of squares of its rational entries.

theorem Hex.Internal.LLLCore.stepBound {n m : Nat} (b : Matrix Int n m) {δ η : Rat} (hred : isLLLReduced b δ η) (_hδη : η * η < δ) (i : Nat) (hi : i + 1 < n) : (δ - η * η) * basisNormSq (GramSchmidt.Int.basis b) ⟨i, ⋯⟩ ≤ basisNormSq (GramSchmidt.Int.basis b) ⟨i + 1, hi⟩

Adjacent Gram-Schmidt norm bound from size reduction and Lovasz.

theorem Hex.Internal.LLLCore.stepAlpha {n m : Nat} (b : Matrix Int n m) {δ η : Rat} (hred : isLLLReduced b δ η) (hδη : η * η < δ) (i : Nat) (hi : i + 1 < n) : basisNormSq (GramSchmidt.Int.basis b) ⟨i, ⋯⟩ ≤ 1 / (δ - η * η) * basisNormSq (GramSchmidt.Int.basis b) ⟨i + 1, hi⟩

Adjacent Gram-Schmidt norm bound in reciprocal form.

theorem Hex.Internal.LLLCore.teleBound {n m : Nat} (b : Matrix Int n m) {δ η : Rat} (hred : isLLLReduced b δ η) (hδη : η * η < δ) (i : Nat) (hi : i < n) : basisNormSq (GramSchmidt.Int.basis b) ⟨0, ⋯⟩ ≤ (1 / (δ - η * η)) ^ i * basisNormSq (GramSchmidt.Int.basis b) ⟨i, hi⟩

Telescoped Gram-Schmidt norm bound from the first vector to index i.

theorem Hex.Internal.LLLCore.basisNormSq_zero {n m : Nat} (b : Matrix Int n m) (hn : 0 < n) : basisNormSq (GramSchmidt.Int.basis b) ⟨0, hn⟩ = ↑(b.row ⟨0, hn⟩).normSq

First Gram-Schmidt basis vector identity: the 0-th Gram-Schmidt vector coincides with the 0-th input row, so their squared norms agree.

theorem Hex.short_vector_bound_of_size_bound {n m : Nat} (b : Matrix Int n m) {δ η : Rat} (hli : b.independent) (hred : 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.

theorem Hex.Internal.isLLLReduced.mono_η {n m : Nat} (b : Matrix Int n m) {δ η₁ η₂ : Rat} (hη₁ : 0 ≤ η₁) (hle : η₁ ≤ η₂) (hred : isLLLReduced b δ η₁) : 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, μ² ≤ η₁² ≤ η₂²).