hex

6.4. The reduction entry points🔗

The reducer state is the proof-facing Hex.Internal.LLLState, which holds the exact integer basis together with the scaled Gram-Schmidt data, and a separate Hex.Internal.LLLState.Valid predicate relates that data to the GramSchmidt.Int representation, keeping the state updates computational while letting the Mathlib side reason about them.

🔗structure
Hex.Internal.LLLState (n m : Nat) : Type
Hex.Internal.LLLState (n m : Nat) : Type

Integer-only state for later LLL reduction steps. The proof-facing fields connect the stored Gram determinants and scaled coefficients to the executable Gram-Schmidt integer data for b.

Constructor

Hex.Internal.LLLState.mk

Fields

b : Hex.Matrix Int n m

The current integer basis, as a matrix of row vectors.

ν : Hex.Matrix Int n n

The integer scaled Gram-Schmidt coefficients of b.

d : Vector Nat (n + 1)

The leading Gram determinants of b (d[k] for k ≤ n).

🔗structure
Hex.Internal.LLLState.Valid {n m : Nat}
  (s : Hex.Internal.LLLState n m) : Prop
Hex.Internal.LLLState.Valid {n m : Nat}
  (s : Hex.Internal.LLLState n m) : Prop

Correctness predicate for the proof-facing interpretation of an executable LLLState. Keeping this separate lets core state updates remain purely computational; Mathlib-side modules can prove preservation when they need the Gram-Schmidt interpretation.

Constructor

Hex.Internal.LLLState.Valid.mk

Fields

ν_eq : ∀ (i j : Nat) (hi : i < n) (hj : j < n),
  j < i → (s.ν.getRow ⟨i, hi⟩).get ⟨j, hj⟩ = ((Hex.GramSchmidt.Int.scaledCoeffs s.b).getRow ⟨i, hi⟩).get ⟨j, hj⟩

Each below-diagonal ν entry equals the executable scaled Gram-Schmidt coefficient of s.b.

d_eq : ∀ (i : Nat) (hi : i < n + 1), s.d.get ⟨i, hi⟩ = Hex.GramSchmidt.Int.gramDet s.b i ⋯

Each d entry equals the corresponding leading Gram determinant of s.b.

The exact all-integer reducer Hex.lllNative drives the standard LLL outer loop (integer size-reduction and adjacent Lovász swaps) from that exact d/ν data alone. Its size-reduction step produces exact |μ| ≤ 1/2, so it satisfies the classical η = 1/2 bound and is the direct 1/4 < δ entry point.

🔗def
Hex.lllNative {n m : Nat} (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) : Hex.Matrix Int n m
Hex.lllNative {n m : Nat}
  (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1)
  (hn : 1 ≤ n) : Hex.Matrix Int n m

Native (non-dispatched) executable LLL entry point. Builds the canonical integer state via LLLState.ofBasisUnchecked and dispatches to lllAux. This is the body the public lll runs by default; its output achieves the classical size-reduction bound |μ| ≤ 1/2 (η = 1/2), so its short-vector guarantee uses α = 1/(δ − 1/4) with the classical precondition 1/4 < δ.

The public entry point hides all of this behind one signature. Given a basis with independent rows and δ in the classical range, it returns a reduced basis generating the same lattice. The short-vector and same-lattice post-conditions are identical on every internal path, so callers and proofs never see the dispatch.

🔗def
Hex.lll {n m : Nat} (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n)
  (_hind : b.independent) : Hex.Matrix Int n m
Hex.lll {n m : Nat}
  (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1)
  (hn : 1 ≤ n) (_hind : b.independent) :
  Hex.Matrix Int n m

Top-level LLL entry point. Dispatches first to the certified-external path: if LLLProvider.providerAvailable () is true and the candidate passes certCheck B B' U V δ (11/20), the certified B' is returned; otherwise the exact lllNative runs. Both paths satisfy the identical post-condition (isLLLReduced (lll …) δ (11/20), same lattice, the public short-vector bound), so dispatch is invisible to callers and to proofs.

Two functions return the short vectors of the reduced basis. Hex.lll.firstShortVector is the single short vector used by recombination. Hex.lll.shortVectors returns the whole reduced basis as an ordered candidate list. Each has a proof-free Unchecked variant that drops the independence hypothesis for quick experimentation.

🔗def
Hex.lll.firstShortVector {n m : Nat} (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n)
  (hind : b.independent) : Vector Int m
Hex.lll.firstShortVector {n m : Nat}
  (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1)
  (hn : 1 ≤ n) (hind : b.independent) :
  Vector Int m

The first row of the reduced basis: a provably short vector, bounded by the LLL approximation factor relative to any nonzero lattice vector (see lll_first_row_norm_sq_le_unconditional), not necessarily the shortest lattice vector. Canonical short-vector entry point for downstream callers such as hex-berlekamp-zassenhaus recombination.

🔗def
Hex.lll.shortVectors {n m : Nat} (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n)
  (hind : b.independent) : Array (Vector Int m)
Hex.lll.shortVectors {n m : Nat}
  (b : Hex.Matrix Int n m) (δ : Rat)
  (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1)
  (hn : 1 ≤ n) (hind : b.independent) :
  Array (Vector Int m)

The full reduced basis viewed as an ordered array of candidate short vectors.